Under maximal semantics, the occurrence of an event a in a concurrent run of an occurrence net may imply the occurrence of other events, not causally related to a, in the same run. In recent works, we have formalized this phenomenon as the reveals relation, and used it to obtain a contraction of sets of events called facets in the context of occurrence nets. Here, we extend this idea to propose a canonical contraction of general safe Petri nets into pieces of partial-order behaviour which can be seen as “macro-transitions” since all their events must occur together in maximal semantics. On occurrence nets, our construction coincides with the facets abstraction. Our contraction preserves the maximal semantics in the sense that the maximal processes of the contracted net are in bijection with those of the original net.
The properties of the long-run, maximal behaviour of discrete event systems
contains also correlations between occurrences, i.e. relations of the type “if a
fires, then b will fire sooner or later – unless it already has”. This could be
exploited in predicting (in the sense e.g. of failure prognosis, see [
It is known that structural transformations can facilitate verification of some
system properties, as witnessed by e.g. Berthelot [
h g 3 c e 4 f 0• 2 a 1 b d ef ab
d hiω cgf 0• 2 (a) (A Petri net representation of) an automaton (b) Its contraction it represents. Note that the infinite word hiω is obtained via a single macrotransition without post-place, since the word has no last transition. Of course, not all temporal properties of the system are preserved, since not all finite words survive the contraction: abcg is a word produced by a run in Figure 1(a), but not in Figure 1(b) which has no intermediate word between (ab) and (ab)(cgf ). However, one sees quickly that the maximal words – which coincide with the infinite words – of the original system of Figure 1(a) are in bijection with the infinite words of the contracted system in Figure 1(b). This contraction represents a reduction of the original system onto its essential behavior.
When concurrent behavior in partial order semantics is considered, the
language of words is replaced by a collection of partial orders representing the
non-sequential runs. Best and Randell [
The paper is organized as follows: We begin by recalling the basic definitions
on unfoldings, and results from [
Reveals Relation and Facets in Occurrence Nets Petri Nets, Occurrence Nets and Unfoldings. This part collects several basic definitions used below. In this paper, only safe Petri nets are considered. Definition 1 (Petri Net). A Petri net (PN), or simply net, is a tuple (P, T, F, M 0) where P and T are sets of places and transitions respectively, F ⊆ (P × T ) ∪ (T × P ) is a flow relation , and M 0 ⊆ P is an initial marking. For any node x ∈ P ∪ T , we call pre-set of x the set •x = {y ∈ P ∪ T | (y, x) ∈ F } and post-set of x the set x• = {y ∈ P ∪ T | (x, y) ∈ F }. A marking of a net is a subset M of P . A transition t is enabled at M iff •t ⊆ M . Then t can fire , t leading to M 0 = (M \ •t) ∪ t•. In that case, we write M −→ M 0. A marking M is reachable if M 0 −→∗ M , where −→ d=ef St∈T −→t. A PN is safe iff for each reachable marking M , for each transition t enabled at M , (t• ∩ M ) ⊆ •t. As usual, in figures, transitions are represented as rectangles and places as circles. If p ∈ M , a black token is drawn in p (see Figure 2(a)).
Partial-order Semantics. Occurrence nets are used to represent the partialorder behaviour of Petri nets. We need a few definitions to introduce them. Denote by l the direct causality relation defined as: for any transitions s and t, s l t ⇔def s• ∩ •t 6= ∅. We write < for its transitive closure and ≤ for its reflexive transitive closure, called causality. For any transition t, the set dte d=ef {s | s ≤ t} is the causal past of t, and for T 0 ⊆ T , the causal past of T 0 is defined as dT 0e d=ef St∈T 0 dte. Two distinct transitions s and t are in direct conflict , denoted by s #d t, iff •s ∩ •t 6= ∅. Two transitions s and t are in conflict , denoted by s # t, iff ∃s0 ∈ dse, t0 ∈ dte : s0 #d t0, and the conflict set of t is defined as #[t] d=ef {s | s # t}. Finally, two transitions s and t are concurrent, denoted by s co t, iff ¬(s # t) ∧ ¬(s ≤ t) ∧ ¬(t ≤ s).
Definition 2 (Occurrence net). An occurrence net (ON) is a Petri net (B, E, F, C0) where elements of B and E are called conditions and events, respectively, and such that: 1. ∀b ∈ C0 •b = ∅, 2. ∀b ∈ B \ C0 |•b| = 1 (no backward branching), 3. ∀e ∈ E ¬(e < e) (≤ is a partial order), 4. ∀e ∈ E ¬(e # e) (no self-conflict), 5. ∀e ∈ E |dee| < ∞ (finite cones). Definition 3 (Configurations and Maximal Configurations). A configuration of an ON is a conflict-free and causally closed set of events, i.e. ω ⊆ E is a configuration iff ∀e ∈ ω, (#[e]∩ω = ∅)∧(dee ⊆ ω). A configuration is maximal iff it is maximal w.r.t. ⊆. We write Ωgen for the set of all configurations and Ωmax for the set of maximal configurations.
Executions of safe Petri nets will be represented as non-branching processes, using occurrence nets related to the original Petri net by a net homomorphism. Definition 4 (Net homomorphism). A net homomorphism from N = (P, T, F, M 0) to N 0 = (P 0, T 0, F 0, M 00) is a pair of maps π = (πP , πT ), where πP : P → P 0 and πT : T → T 0, such that: – for all t ∈ T , πP |•t (the restriction of πP to •t) is a bijection between •t and •πT (t), and πP |t• is a bijection between t• and πT (t)•; – and πP |M0 maps injectively M 0 to (a subset of ) M 00.
We will often write simply π instead of πP or πT .
Net homomorphisms preserve the semantics of nets in the sense that they map every firing sequence of N to a firing sequence of N 0, and πP |M0 needs not be a bijection for that. If a place p0 of N 0 is not the image of any place of N , it simply means that the images in N 0 of the firing sequences of N do not use the token initially in p0. We need this subtlety to define macro-transitions later. Definition 5 (Branching process). Let N = (P, T, F, M 0) be a PN. A branching process of N is a pair (O, π), where O = (B, E, F 0, C0) is an ON and π is a homomorphism from (B, E, F 0, C0) to (P, T, F, M 0) such that for all t, t0 ∈ E, •t = •t0 ∧ π(t) = π(t0) ⇒ t = t0. . . .
t0 t2 2 t2 2 2 2 t5 t5 . . .
Definition 6 (Run). A run of a safe Petri net N = (P, T, F, M 0) is a branching process (O, π) of N with O = (B, E, F 0, C0) such that E is a configuration and π(C0) = M 0.
Definition 7 (Prefix). For Π1, Π2 two branching processes, Π1 is a prefix of Π2, written Π1 v Π2, if there exists an injective homomorphism h from ON1 into ON2, such that the composition π2 ◦ h coincides with π1.
Definition 8 (Maximal run). A run ρ is maximal if it is not a proper prefix of any run, i.e. for every run ρ0, if ρ is a prefix of ρ0, then ρ and ρ0 are isomorphic. We define a function μ which allows us to construct the run μ(ω) corresponding to a configuration ω of an ON.
Definition 9 ( μ). Let O = (B, E, F, C0) be an occurrence net. Every
conflictfree set of events E0 ⊆ E defines a run μ(E0) of the Petri net (B, E, F, •E0\E0•)1.
The occurrence net μ(E0) has E0 as events, their pre- and post-sets as conditions,
and •E0 \ E0• as initial conditions. The arcs are the restriction of F to these
events and conditions, and the folding homomorphism π is the identity.
Definition 10 (Unfolding). Let N be a PN. By Theorem 23 of [
Remark. Occurrence nets are linked to safe Petri nets in the sense that the partial
order unfolding semantics of such Petri nets yields occurrence nets, as defined
above. The converse is true for occurrence nets corresponding to regular trace
languages: Following Zielonka [
Reveals Relation and Facets Abstraction. The structure of an ON defines three relations over its events: causality, conflict and concurrency. But these structural relations do not express all logical dependencies between the occurrence of events in maximal configurations. A central fact is that concurrency is not always a logical independency: it is possible that the occurrence of an event implies, under the perspective of maximal runs, the occurrence of another one, which is structurally concurrent. This happens with events t1 and t01 in Figure 3(a): we observe that t1 is in conflict with t0 and that any maximal configuration contains either t0 or t01. Therefore, if t1 occurs in a maximal configuration, then t0 does not occur and eventually t01 necessarily occurs. Yet t1 and t01 are concurrent.
Another case is illustrated by events labeled t3 and t4 on the left of the same
figure: because t3 is a causal predecessor of t4, the occurrence of t4 implies the
occurrence of t3; but in any maximal configuration, the occurrence of t3 also
implies the occurrence of t4, because t4 is the only possible continuation to t3
and nothing can prevent it. Then t3 and t4 are actually made logically equivalent
by the maximal progress assumption.
1 Notice that (B, E, F, •E0 \ E0•) is not an occurrence net in general: it satisfies items
3, 4 and 5 of Definition 2, but items 1 and 2 may not hold.
Definition 11 (Reveals relation [
Definition 12 (Facets Abstraction in Occurrence Nets[
In Figure 3(a), the facets are highlighted in grey. If ψ is a facet, then for any maximal configuration ω ∈ Ωmax and for any event e such that e ∈ ψ, e ∈ ω iff ψ ⊆ ω. In this sense, facets can be seen as atomic sets of events (under the maximal semantics). Denote the set of O’s facets as Ψ (O).
For any facet and for any configuration, either all events in the facet are in the configuration or no event in the facet is in the configuration. Therefore, facets can be seen as events.
Definition 13 (Reduced occurrence net).
(B, E, F, C0) such that ∀e1, e2 ∈ e,
As shown in [
(b, ψ) : b ∈ B ∧ ∃ e ∈ ψ : (b, e) ∈ F
∪ (ψ, b) : b ∈ B ∧ ∃ e ∈ ψ : (e, b) ∈ F
(1)
(2)
Preliminaries. We propose to identify pieces of partial-order behaviour of a
safe Petri net, under the form of macro-transitions which group events that
always occur together when at least one of them occur in any maximal run of
the original net. There will be a fundamental difference in the approach here
with respect to the work in [
Definition 15 (Macro-transition). Let N = (P, T, F, M 0) be a PN. A macrotransition of N is a run φ = (O, π) of (P, T, F, π(C0)) (the net N initialized with the image of the initial conditions C0 of O) such that for any reachable marking M of N with π(C0) ⊆ M and for any maximal run ρ of (P, T, F, M ) (the net N starting at M ), if there exists a nonempty prefix φ0 of φ which is also a prefix of ρ, then the entire φ is a prefix of ρ. 0• t1 1 (a) φ1 0• t1 1 00• 1• t2 2 2 2 t5 t5 (c) φ3 5• 5 5
– φ1 is trivially a macro-transition. – In φ2 we have two events: an occurrence of t1 and one of t01. The initial conditions of φ2 are mapped to places 0 and 00 of N . The only reachable marking of N which contains {0, 00} is {0, 00} itself; in {0, 00}, if one of the two transitions fire, the other one will necessarily fire in any maximal run. – Consider now φ3: again the only reachable marking of N which contains {1, 5} is {1, 5} itself. From it, if t2 fires, it is necessarily followed by an infinite sequence of firings of t5. φ3 is exactly a prefix of it.
We also find counter-examples here: – φ4 is not a macro-transition as it is not a run: t0 and t1 are in conflict. – φ5 is not a macro-transition because an occurrence of t1 is not necessarily followed by an occurrence of t2. – Concerning φ6, it is exactly a prefix of every maximal run from {1, 00} starting by an occurrence of t2, but not of every run starting by an occurrence of t01 (because t02 can fire instead of t2).
The two following properties are immediate consequences of the definition. Property 1. Any single transition t ∈ T induces a macro-transition defined as the (unique, up to isomorphism) non-branching process which contains a single event mapped to t and whose initial conditions are mapped to •t. For example, the facet induced by t1 in the net of Figure 2(a) is the one depicted in Figure 4(a). Property 2. Let φ be a macro-transition of a Petri net N . Then any prefix of φ with the same initial conditions as φ is also a macro-transition of N . Definition 16 ( Φ-contracted net). Given a set Φ of macro-transitions of a Petri net N = (P, T, F, M 0), we construct the Φ-contracted net N/Φ by replacing 0• t1 1
t0 (a) φ4 00• 0• t1 1 t2 2 (b) φ5 00• 4 1• t2 2 (c) φ6 the transitions of N by new transitions which summarize the macro-transitions. The contracted net is formally defined as the net N/Φ = (P, Φ, FΦ, M 0) where the macro-transitions are interpreted as transitions and with the flow relation FΦ defined such that, for every φ = (O, π) ∈ Φ, •φ is the image by π of the initial conditions of O, and φ• is the image by π of the conditions of O that are not consumed by any event of O.
To express the soundness of this contraction, we define a function χ which maps any branching process (O, π) of the contracted net N/Φ to a branching process of N . Intuitively, χ simply expands every event e of O into a set of events corresponding to the content of the macro-transition π(e). For example, the reduced unfolding of Figure 3(b), viewed as a branching process of the contraction of the unfolding U of Figure 3(a), is mapped by χ to U .
Definition 17 ( χ). Let N = (P, T, F, M 0) be a Petri net, Φ a set of macrotransitions of N and ρ = (O, π) a branching process of the contracted net N/Φ, with O = (B, E, F, C0). We define the branching process χ(ρ) of N as χ(ρ) = (O0, π0) with O0 = (C0 ∪ χcond (E), χevents (E), χcond (E), χarcs (E), C0) where χevents , χcond and χarcs associate to every event e ∈ E a set of events χevents (e), a set of conditions χcond (e) and a set of arcs χarcs (e), all specified below. Remember that e is an occurrence of transition π(e) of N/Φ, which is also a macro-transition of N and thus has the form (Oe, πe) with Oe an occurrence net and πe a net homomorphism from Oe to (P, T, F, π(Ce0)), where Ce0 are the initial conditions of Oe.
The set χevents (e) is defined as the set of pairs (e, f ) with f an event of Oe; it represents an occurrence of each of the events that were grouped inside the macro-transition π(e) of the contracted net N/Φ.
The set χconds (e) is defined as the set of pairs (e, b) with b a condition created by an event of Oe; it represents all conditions created by events in χevents (e). The initial conditions of π(e) are not reproduced since they will be merged with the final conditions of the occurrence of the macro-transition that created them.
Now the arcs in χarcs (e) connect naturally every event (e, f ) to the conditions (e, b) with b ∈ f •, and every condition (e, b) with b ∈ •f to the event (e, f ).
It remains the case of the initial conditions of Oe: for every initial condition b of Oe, there exists a unique condition b0 ∈ •e such that π(b0) = πe(b) ∈ P . Either this b0 is an initial condition of O or it is created by an event e0 ∈ E. In the first case, b0 is also an initial condition of O0 and an arc is added in χarcs (e) to connect it to any event (e, f ) ∈ χevents (e) representing an event f of Oe which consumes b. In the second case b0 comes from a final condition of π(e0), which appears in χcond (e0) and serves as the origin of the arcs.
Finally, we define the homomorphism π0 from O0 to N . It maps simply every event (e, f ) to the transition πe(f ) ∈ T , and every condition (e, b) to πe(b) ∈ P . On the set C0 of initial conditions, π0 coincides with π : π|C0 ≡ π|0C0 . Lemma 1 (Soundness). Let N be a Petri net and Φ a set of macro-transitions of N . The function χ maps any branching process (O, π) of the contracted net N/Φ to a branching process of N .
Proof. By construction of χ. tu Definition 18 (Completeness). A set Φ of macro-transitions of a Petri net N = (P, T, F, M 0) is complete if for every reachable marking M of the contracted net N/Φ = (P, Φ, F 0, M 0) and every transition t ∈ T firable from M , the run of (P, T, F, M ) composed of all the events revealed by the initial occurrence of t in the unfolding of (P, T, F, M ), is the image by χ of a run of (P, Φ, F 0, M ). Lemma 2. Let N be a Petri net and Φ a complete set of macro-transitions of N . Then every maximal run ρ of N is (isomorphic to) the image by χ of a maximal run ρ0 of N/Φ.
Proof. To construct the ρ0, start from the process with no events and initial conditions corresponding to the initial marking of N (which is also the initial marking of N/Φ). Then, as long as there are events in ρ which are not in χ(ρ0), take one which is minimal w.r.t. causality and call it e. (Among the possible choices, e should be of minimal depth2 so that every event of ρ is eventually in χ(ρ0).) The transition t of N which is the image of e by the homomorphism of ρ, can fire from the marking M reached after ρ0 (which is also the marking reached after χ(ρ0)). By the completeness hypothesis, there exists a run of (P, Φ, F 0, M ) whose image by χ yields all the events revealed by the firing of t from M . Then ρ0 can be augmented by this run. Our e of ρ is now one of the new events in χ(ρ0); and the other new events are also in ρ because they are revealed by the occurrence of t from M and ρ is maximal.
Notice that at each step, χ(ρ0) is a prefix of ρ. The iteration may not terminate but, since ρ0 always grows, we consider its limit (containing all the events that are eventually added). By construction this limit is the desired process. 2 The depth of an event e is the size of the longest path from an initial condition to e. 3 By “φ starts by t”, we mean that there exists an event in φ which is mapped to t and consumes only initial conditions of φ. Theorem 1 (Facets as Macro-Transitions). Let O = (B, E, F, C0) be an occurrence net and ψ ⊆ E a facet of O. Then μ(ψ) is a macro-transition of O. Moreover the image by μ of all the facets of O is a complete non-redundant set of macro-transitions of O.
Proof. Consider a reachable set of conditions C ⊇ •ψ, and let ω be a maximal run of (B, E, F, C) starting by a nonempty prefix of μ(ψ). Then ω starts by μ({e}) with e an initial event of ψ. By Definition 12, e reveals all the events in ψ. This implies that ω starts by the entire μ(ψ).
For completeness, remark that for every run ρ of the contracted ON, the events in χ(ρ) are a union of facets of O. After such a run, every maximal run is again a union of facets.
Non-redundancy holds because the facets are a partition of the events. tu 4
Before defining our canonical contraction, we study the markings that are reachable after a run of a contracted net.
For every configuration O, we call cut of O the set of conditions which are created and not consumed along O. When O is the support of a finite run (O, π) of a net N , the homomorphism π maps the cut of O to a reachable marking of N . And conversely every reachable marking of N is the image of the final conditions of a finite run.
But in this paper we focus on maximal runs, which are in general infinite. And the image of a cut of an infinite run may be only a subset of a reachable marking of N . An example is the maximal run of the net of Figure 1(a) containing an occurrence of h and an infinite chain of i’s. All the conditions are consumed, and the cut is empty. Yet the empty marking is not reachable after any finite run.
Then we call asymptotically reachable (or a-reachable for short) in N any marking that is the image of the cut of a (possibly infinite) run of N . Lemma 3 (A-Reachability in a Contracted Net). Let N be a Petri net and Φ a set of macro-transitions of N . Any marking a-reachable in N/Φ is also a-reachable in N .
Proof. This is an immediate consequence of Lemma 1. tu
Notice however that in general not every marking a-reachable in N is areachable in N/Φ. And this is actually what allows us to skip some intermediate markings and give a more compact representation of the behaviour of the net.
In this sense we can say that a complete contracted net N/Φ is more compact than another N/Φ0 if all markings a-reachable in N/Φ are also a-reachable in N/Φ0 . We will show now that there exists a complete non-redundant contracted net which is optimal w.r.t. this criterion: i.e. all markings a-reachable in this contracted net are a-reachable in any complete non-redundant contracted net. Definition 20 ( MN and RN ). We define inductively a set of M and a set RN of runs as the smallest sets satisfying: MN of markings – M 0 ∈ MN ; – for every M ∈ MN , for every transition t firable from M , μ(E) ∈ RN , where
E is the set of events revealed by the initial occurrence of t in U ((P, T, F, M )); – for every M ∈ MN , for every ρ ∈ RN such that •ρ ⊆ M , the marking (M \ •ρ) ∪ ρ• reached after firing ρ from M , belongs to MN ; – for every ρ1, ρ2 ∈ RN , the largest common prefix of ρ1 and ρ2 is in RN . Theorem 2. Let N = (P, T, F, M 0) be a Petri net and Φ a non-redundant complete set of macro-transitions. All markings of MN are a-reachable in N/Φ. Proof. Let NΦ = (P, Φ, F 0, M 0). The theorem is a direct consequence of the following lemma: for every marking M a-reachable in N every run ρ ∈ RN firable from M satisfies the property that ρ is the image by χ a run ρ0 of (P, Φ, F 0, M ). This lemma is proved by induction, following the construction of RN : at each step of the construction, we prove that if all the runs in the current RN satisfy the property, then the new runs added to RN also satisfy it. Initialization of the induction is trivial since RN is initially empty.
By completeness of Φ, the property is satisfied by all the runs of the form μ(E) with E the set of events revealed by the initial occurrence of a transition t in U ((P, T, F, M )). For every run ρ constructed as the largest common prefix of two runs ρ1 and ρ2 already in RN , assume that ρ1 and ρ2 satisfy our property and call ρ01 and ρ02 the corresponding runs of the contracted net. By non-redundancy of Φ, ρ01 and ρ02 must coincide on the largest common prefix ρ of ρ1 and ρ2. Then ρ is the image by χ of the largest common prefix of ρ01 and ρ02. tu Definition 21 (Canonical contraction N ). We define the canonical contraction of a safe Petri net N as the contracted net N d=ef NΦN where ΦN is the set of nonempty runs of RN which are minimal w.r.t. the prefix relation. Theorem 3. For every safe Petri net N , the set ΦN of macro-transitions in N is complete and non-redundant, and the set of states a-reachable in N is precisely MN . Moreover |ΦN | ≤ |T |.
Proof. Completeness is ensured by the insertion in RN of all the runs of the form μ(E) with E the set of events revealed by the initial occurrence of a transition t in U ((P, T, F, M )). For redundancy, assume two runs ρ1 and ρ2 of RN both start by an occurrence of t. Then their common prefix ρ is nonempty and is in RN . Then ρ1 and ρ2 are not minimal in RN w.r.t. the prefix relation, and they are not in ΦN . By construction all the states a-reachable in N are in MN . Finally the inequality |ΦN | ≤ |T | is a direct consequence of the non-redundancy of ΦN . tu Illustration. Let us construct the canonical contraction of the net N of Figure 2(a). MN contains the initial marking {0, 00}. From this marking t0, t1 and t01 are firable. Since t1 and t01 reveal each other, RN contains the runs t0 and t1t01, and MN contains the reached markings {} and {1, 4}. From {1, 4}, t2 and t02 can fire; they reveal nothing, so they are added as such to RN . The marking {2, 4} is now reachable; it is added to MN . From {2, 4}, t3 and t03 can fire, and in both cases an occurrence of t4 necessarily follows. Hence t3t4 and t03t4 are added to RN . We can now reach {1, 5} and fire t2 or t02 again. But, from {1, 5} firing t2 (or t02) reveals an infinite sequence of occurrences of t5. For this t2t5ω and t02t5ω are added to RN . But, since t2 and t02 already appear “alone” – i.e. as singleton transitions – in RN , marking {2, 5} obtained after firing them from {1, 5} must also be added to MN . And from it, t5ω can fire and is added to RN . Now, ΦN is constructed by extracting the runs of RN that are minimal w.r.t. the prefix relation. Here we get all of them, except t2t5ω and t02t5ω. The resulting contracted net is shown in Figure 2(b).
Contraction and Automata. It is clear that applying our contraction to the Petri net representation N of an automaton (i.e. a Petri where every transition has exactly one input- and one output-place) removes the deterministic states (or places), i.e. those from which there is no choice. Concretely, these places will not appear in the set MN . The macro-transitions are the paths between non-deterministic states with only deterministic intermediate states. 5
When concurrent behavior in partial order semantics is considered, our
contraction is related to the facets reduction [
Theorem 4 (Reduction as contraction of ONs). For every occurrence net O, the canonical contraction of O is isomorphic to its facet reduction. Proof. By Definition 20, all runs in RO correspond to unions of facets of O. Now, let ρ ∈ RO be a run containing more than one facet. By definition of facets, the reveals relation on facets is antisymmetric. Then one of O0s initial facets, say ψ1, does not reveal the other, say ψ2. Take an initial event e of ψ1 and a marking M ∈ MO from which ρ can fire; e is firable from M in O. Therefore RO contains the run ρ0 containing the events revealed by e from M . This run contains ψ1 but not ψ2. By definition, RO contains the largest common prefix of ρ and ρ0. Hence ρ is not minimal in RO w.r.t. the prefix relation, and is not in ΦO. tu
As illustrated in Figure 6, the operation of reduction does not entirely commute with unfolding. That is, in general, the unfolding U (N ) of reduced Petri net N is coarser, as an occurrence net, than the reduction U (N ) of the original net N ’s unfolding. In the example of Figure 6, the facets labeled t2t5ω and t02t5ω in U (N ) are both split into two events of U (N ).
However, one retrieves the reduction of U (N ) from U (N ) as follows. Theorem 5. For every net N , applying the occurrence net facet reduction to U (N ) yields U (N ) up to isomorphism.
t0 t2 2 t3t4
t03t4 t0 t2 2 0• 1 t1t01 t0 2 2 00•
4 t3t4 t03t4 t3t4
t03t4 (a) The unfolding of the contracted Petri net of Figure 2(b). Remark that the unfolding is not reduced: the last occurrence of t2 and the following t5ω are in the same facet (similarly for t02 and the following t5ω).
contraction contraction (or reduction)
Proof. By definition of macro-transitions, for every event e of U (N ), all the events of U (N ) which are in χevents (e), reveal each other. Then χevents (e) is included in a facet ψ of U (N ). And for two events e1 and e2 of U (N ), an event in χevents (e1) reveals (in U (N )) an event in χevents (e2) iff e1 reveals e2 in U (N ). Therefore the facets reduction of U (N ) regroups e1 and e2 into the same facet iff the events in χevents (e1) and those in χevents (e2) are in the same facet. tu
We have presented a method for identifying and contracting macro-transitions in
safe Petri nets. The procedure includes and justifies our previous work in [