We assume that the reader is familiar with definitions and notations of Petri nets, as well as Coloured Petri Nets (CPNs, CP-nets) in particular, such as, marking, enabling, reachability, preset, postset, initial marking, binding elements, token elements, multi-sets etc. We will use the definitions and notations of Petri nets as described in [1]. For the definitions and notations of Coloured Petri Nets we will rely on [5–7]. In the following we will introduce McMillan’s unfolding technique.
2.1 McMillan’s Unfolding
McMillan’s unfolding approach is based on partial order semantics for Petri nets, i.e., the states of a system are represented implicitly, using branching processes, which are in fact labelled acyclic Petri nets (occurrence nets).
The idea of McMillan’s unfolding algorithm [15], roughly described bellow, is very simple: for each token in the initial marking of a given Petri net, make a copyb of the placepon which it resides and label it withp, and then carry out the following steps:
– Choose a transitiontfrom the given Petri net.
– For each placepconnected tot(those with arcs directed tot) find a copyb, labelled withp, and mark it with a token. If no such a copy can be found, then go to the first step. Note: for a givent, do not choose the same subset of places twice.
– If, for any two placesa andb of the marked places, there is a path leading from one place to the other or there exists a place c containing different paths leading to a and b, while exiting c by different arcs, go to the first step.
– Make a copy e of t and label it with t. From each of the marked copies b draw an arc toe. Erase the tokens.
– For each place p, that t has an arc pointing to it, make a copyb, label it withpand draw an arc from eto b.
Following these steps one can easily unfold the Petri net presented in Fig.2(a). Its unfoldings are shown in Fig.2(b) and (c), i.e., unfoldings can have different sizes, depending on how long we proceed with it. And, depending on the behaviour of Petri nets, an unfolding can get infinitely long and as such not very useful for analysis.
Let us briefly introduce in the following the unfoldings of low-level Petri nets more formally and finally define the algorithm for generating the finite complete prefix, which can be used for verification.
The relations between any two distinct nodes of a Petri net,x, y∈P∪T (with P representing the set of places and T the set of transitions), are defined as follows:
– xandy are incausal-relation, if there exist a path in the net with at least one arc leading from x to y or from y to x, denoted y < x and x < y, respectively.
– xand yare in conflict-relation, denotedx#y, if
∃t1, t2∈T, t1=t2 ∧•t1∩•t21=∅ : (t1< x∧t2< y), i.e., there exists a place containing different paths leading toxandy.
– xand yare in concurrency-relation, denotedxcoy, if
¬(x < y)∧ ¬(y < x)∧ ¬(x#y) = true, i.e.,xandy are neither in causal-relation nor in conflict-causal-relation.
1•xrepresents the preset ofxandx•represents the postset ofx.
Let us consider the branching process in Fig.2(b) regarding the relations de-scribed above, one can easily get some information about the behaviour of the original Petri net (Fig.2(a)), e.g., the nodesb1ande5 are in causal-relation, i.e., the action t1 occurs after the state th1. e3 and e4 are in conflict-relation, i.e., the actionst2andt4 cannot take place in parallel.b1 andb4are in concurrency-relation, i.e., the states th1andth2 do not influence each other.
Having introduced the relations above, we can now define the occurrence nets and the branching processes for low-level Petri nets.
Anoccurrence netis an acyclic Petri netO= (B, E, F), whereB is the set of conditions (places),E is the set ofevents (transitions) andF is a flow relation, satisfying the following:
– ∀b∈B,|•b| ≤1, i.e., a condition has only one or none event in its preset, – ∀x∈(B∪E) :|{y∈(B∪E)|y < x}|<∞, i.e., each node has a finite set
of nodes being in casual-relation with, and
– ∀y∈B∪E,¬(y#y), i.e., the nodes are not in self-conflict, thus, no two (or more) disjunctive paths starting at a condition are allowed to merge into a single node.
Definition 1. A branching process of a Petri net systemΣ = (P, T, F, M0) is the pairβ = (O, p), whereO is an occurrence net andpa labelling function satisfying the following properties:
(i) p(B)⊆P andp(E)⊆T, i.e., conditions are mapped to places and events to transitions.
(ii) ∀e∈E, the restriction of pto•e is a bijection between•e(in Σ) and •p(e) (inβ), similarly fore•andp(e)•, i.e., transition environments are preserved.
(iii) the restriction ofpto the set of conditions that have an empty preset, denoted Min(O), is a bijection between Min(O)andM0, i.e.,β starts atM0. (iv) ∀ e1, e2 ∈E : (•e1 = •e2∧p(e1) = p(e2))⇒ (e1 =e2), i.e., there is no
redundancy.
prepresents thehomomorphism fromO toΣ.
As mentioned, depending on how long we unfold, we get different sizes of branch-ing processes, i.e., a branchbranch-ing process can be a prefix of some other branchbranch-ing process. For example, the branching process in Fig.2(c) is a prefix of the branch-ing process in Fig.2(b).
A branching process β = (O, p) is a prefix of another branching process β = (O, p), denotedβ β, ifO is a subnet ofOsatisfying:
– Min(O)belongs toO, i.e., bothβ andβstart at the same set of conditions, – if a conditionbbelongs toO, then its input evente∈•b inO also belongs
toO (if it exists), and
– if an eventebelongs toO, then its input and output conditions,•e∧e•, in Oalso belong toO.
There exists a unique, up to isomorphism, maximal (w.r.t.) branching process βmaxfor any given Petri net systemΣ, called theunfolding ofΣ(see [1, 11–13]).
The unfolding of the Petri net in Fig.2(a) is infinite.
In order be able to define the finite complete prefix of an unfolding, we will introduce in the following some more definitions. These will also contribute on building a stronger connection between branching processes and their original Petri nets.
A set of eventsC⊆E is called aconfigurationif the following is satisfied:
– ∀e, e∈C : ¬(e#e), i.e.,C is conflict-free, and – ∀e∈C : e≤e⇒e∈C, i.e.,C is causally-closed.
Thelocal configuration of an event eof a branching process, denoted[e], repre-sents the set of eventsE, such thate ≤e,∀e ∈E.
The set of events{e1, e3, e5, e6} is a configuration, as well as the local configu-ration ofe6. The setsC={e1, e2, e4}andC={e1, e3, e6}are not.C satisfies the second configuration-property but not the first, i.e., e1 is in conflict with both other events.Csatisfies the first property but not the second, because the evente5 is missing.
Further, a set of conditionsB⊆Bis called aco-set, iff for allb, b∈B : ¬(b <
b∨b < b∨b#b), i.e., b and b are neither reachable from each other nor are they in conflict with each other. A maximal co-setB ⊆B is called acut.
The set of conditionsB ={b1, b2, b3}is a co-set, and addingb4toB,B∪ {b4}, we get a cut, i.e., there is no other condition that can be added toB without destroying the co-set property, thus,B is maximal.
For a given finite configurationC the co-setCut(C) = (Min(O)∪C•)\•C is a cut. In addition, the set of placesMark(C) =p(Cut(C))is a reachable marking in the original Petri net. Thus, a cut represents a reachable marking.
LetC ={e1, e3, e5, e6} be a configuration of the branching process in Fig.2(b) andMin(O) ={b1, b2, b3, b4}represent the set of conditions with an empty pre-set, we get the cut Cut(C) = (Min(O)∪C•)\•C = {b4, b14, b15, b16}, which represents the reachable markingMark(C) =p(Cut(C)) ={th1, th2, f1, f2}.
One can conclude that, a marking M of a Petri net system Σ is represented in a branching processβ of Σ iffβ contains a finite configurationC such that Mark(C) =M. Further, every reachable marking of a Petri net system is rep-resented in its unfolding, and every marking reprep-resented in a branching process is reachable in the original Petri net system, see [1, 11–13].
There are certain rules, during unfolding, that one has to follow, in order to find extensions of already built branching processes. These extensions that come into consideration are called possible extensions and are defined as follows:
Definition 2. A possible extension of a branching process β of a Petri net systemΣ is a pair (t, X)2 such that:
(i) p(X) =•t, and
(ii) (t, X) is not a part ofβ.
2X is a co-set of conditions ofβ, andta transition ofΣ
Finite Prefix Algorithm:
input:Σ= (N, M0)3 — ann-safe net system output: a finite complete prefixF inofΣ Fin :={(s1,∅), . . . ,(sn,∅)}
pe := P E(F in) cut-off :=∅ whilepe=∅do
choose an evente= (t, X)inpesuch that [e] is minimal w.r.t. ≺ if[e]∩cut-off =∅then
add toFin eand a condition(s, e)for every output placestot pe := P E(F in)
ifeis a cut-off event ofFin then cut-off := cut-off ∪ {e}
pe := pe− {e}
Fig. 1.The finite complete prefix algorithm.
The set of all possible extensions of β is denotedP E(β).
A possible extension of the branching process in Fig.2(c) would be the pair (t1,{b7, b8, b9}), which is already represented in Fig.2(b).
When dealing with Petri nets that have an infinite unfolding, e.g., like the one in Fig.2(a), the number of possible extensions is infinite as well. However, our aim is the construction of a finite complete prefix of an unfolding. In order to achieve this, we will introduce in the following two other core components of the prefix generation process, namely the adequate order and cut-off event.
A partial order ≺on the finite configurations of the unfolding of a net system is anadequate order if:
– ≺is well-founded, – C1⊂C2⇒C1≺C2, and
– ≺ is preserved by finite extensions, i.e., if C1 ≺ C2 and Mark(C1) = Mark(C2), then the isomorphism I4 satisfies C1⊕E ≺ C2⊕I(E) for all finite extensionsC1⊕E ofC1.
Let ≺ be an adequate order on the configurations of the unfolding of a net system, and letβ be a prefix of the unfolding containing an evente. The event e is a cut-off event of β (w.r.t.≺) if β contains a local configuration [e] such that:
– Mark([e]) =Mark([e]), and – [e]≺[e].
4 I is a mapping from the finite extensions ofC1 onto the finite extensions ofC2. A configurationCand a set of eventsEis called anextensionofC, denotedC⊕E, if C∪E is a configuration such thatC∩E=∅.
(a)
Fig. 2.A Petri net(a), one of its branching process(b)and its prefix(c).
The conditionse3 ande4build the cut-off events set of the net in Fig.2(a). The dashed line through the eventse3ande4in Fig.2(b)represents thecut-off-point of these events, i.e., further construction is stopped, and the already constructed part (up to the dashed line) represents the finite complete prefix. It is easy to see that the part after these two events repeats itself, and thus the prefix contains all the necessary information about the reachable states. A branching process β = (O, p) of a Petri net system Σ = (P, T, F, M0) is complete iff for every reachable marking M in Σ there exists a configuration C in β, not containing any cut-off event, such that:
– Mark(C) =M, indicating thatM is represented inβ, and
– ∀t∈T enabled inM there exists a configurationC∪ {e}:e /∈C∧p(e) =t.
Further, the number of events in the complete prefix can never exceed the number of reachable states of a Petri net, see [1, 11–13]. Thus, the size of the prefix is never larger than the corresponding state space graph.
Now we can put all these definitions together and define the finite complete prefix algorithm, which is shown in Fig.1. The correctness of the algorithm,Fin is finite andFin is complete, is proved in [1], and thus omitted.