Nested Petri nets (NP-nets) is an extension of the Petri nets formalism within the nets-within-nets approach, allowing to model systems of interacting dynamic agents in a natural way. One of the main problems in verifying of such systems is the State Explosion Problem. To tackle this problem for highly concurrent systems the unfolding method has proved to be very helpful. In this paper we continue our research on applying unfoldings for NP-nets verication and compare unfolding of NP-net translated into classical Petri net with direct component-wise unfolding.
Multi-agent systems have been studied explicitly for the last decades and can be regarded as one of the most advanced research and development area in computer science today. They are used in various practical elds and areas, such as articial intelligence, cloud services, grid systems, augmented reality systems with interactive environment objects, information gathering, mobile agent cooperation, sensor information and communication.
Petri nets have been proved to be one of the best formalisms for modeling and
analysis of distributed systems. However, due to the at structure of classical
Petri nets, they are not so good for modeling complex multi-agent systems. For
such systems a special extension of Petri nets, called nested Petri nets [
To check nested Petri net model properties one of the most popular verication method, model checking, could be used. The basic idea of model checking is to build a reachability (transition) graph and check properties on this graph. However, there is a crucial problem for verication of highly concurrent systems using model checking approach a large number of interleavings of concurrent processes. This leads to the so-called state-space explosion problem.
To tackle this problem unfolding theory [
However, safe conservative nested Petri nets are bounded. So, for such net
it is possible to construct a P/T net with equivalent behavior, for which the
standard unfolding techniques can be applied. Then the question is whether
direct unfolding proposed in [
In this paper we study this question. For that we develop an algorithm for translating a safe conservative NP-net into a behaviorally equivalent P/T net. We prove that the reachability graphs of a source NP-net and the obtained P/T net are isomorphic, and hence both unfolding methods give the same (up to isomorphism) result. From general considerations translating an NP-net into a P/T net and then constructing unfoldings will be more time consuming, than constructing unfoldings directly. To check whether this time gap reveals itself in practice we implement all the algorithms and compare both methods experimentally.
Related Work Nested Petri nets (NP-nets) are widely used in modeling of
distributed systems [
Several methods for NP-nets behavioral analysis were proposed in the
literature, among them compositional methods for checking boundedness and liveness
for nested Petri nets [
Unfolding approach and state-space explosion problem are explicitly studied
in the literature. The original development in unfoldings (of P/T-nets) is due
to [
The original McMillan’s algorithm was used to solve the executability problem
to check whether a given transition can re in the net. This algorithm can be
used also for checking deadlock-freedom and for solving some other problems.
Later, numerous improvements to the algorithm have been proposed ([
The general method for truncating unfoldings, which abstracts from the
information one wants to preserve in the nite prex of the unfolding, was proposed
in [
The paper is organized as follows. In Section 2 we present the basic notions of Petri nets, nested Petri nets, and classical unfoldings. In Section 3 an algorithm for nested Petri nets into P/T nets translation is described. In Section 4 direct unfoldings for safe conservative NP-nets are dened and compared with constructing unfoldings via into P/T nets translation. The last section gives some conclusions. 2
Multisets. Let S be a nite set. A multiset m over a set S is a function m : S Nat, where Nat is the set of natural numbers (including zero), in other words, a multiset may contain several copies of the same element.
For two multisets m, m1 we write m m1 i @s P S : mpsq ⁄ m1psq (the inclusion relation). The sum and the union of two multisets m and m1 are dened as usual: @s P S : pm m1qpsq mpsq m1psq, pm Y m1qpsq maxpmpsq, m1psqq. 2.1
P/T-nets Let P and T be two nite disjoint sets of places and transitions and let F pP T q Y pT P q be a ow relation . Then N p P, T, F q is called a P/T-net.
A marking in a P/T-net N p P, T, F q is a multiset over the set of places P . By MpN q we denote a set of all markings in N . A marked P/T-net pN, M0q is a P/T-net together with its initial marking M0.
Pictorially, P -elements are represented by circles, T -elements by boxes, and the ow relation F by directed arcs. Places may carry tokens represented by lled circles. A current marking m is designated by putting mppq tokens into each place p P P .
For a transition t P T , an arc px, tq is called an input arc, and an arc pt, xq an output arc. For each node x P P Y T , we dene the pre-set as x t y | py, xq P F u and the post-set as x t y | px, yq P F u.
We say that a transition t in a P/T-net N p P, T, F q is enabled at a marking M i t M . An enabled transition may re , yielding a new marking M 1 M t t (denoted M t M 1). A marking M is called reachable if there exists a (possibly empty) sequence of rings M0 t1 M1 t2 M2 M from the initial marking to M . By RMpN, M0q we denote the set of all reachable markings in pN, M0q.
A marking M is called safe i for all places p P P we have M ppq ⁄ 1. A marked P/T-net N is called safe i every reachable marking M P RMpN, M0q is safe. A reachability graph of a P/T-net pN, M0q presents detailed information about the net behavior. It is a labeled directed graph, where vertices are reachable markings in pN, M0q, and an arc labeled by a transition t leads from a vertex v, corresponding to a marking M , to a vertex v1, corresponding to a marking M 1 i M t M 1 in N . 2.2
Classical Petri Nets Unfoldings
Branching processes and unfoldings of P/T-nets. Unfoldings are used to dene
non-sequential (true concurrent) semantics of P/T-nets, and complete prexes
of unfoldings are used for verication. Here we give necessary basic notions and
denitions, connected with unfoldings. Further details can be found in [
Let N p P, T, F q be a P/T-net. The following relations are dened on the set P Y T of nodes in N : 1. the causality relation, denoted as , is the transitive closure of F , and ⁄ is the reexive closure of ; if x y, we say that y causally depends on x. 2. the conict relation, denoted as #: nodes x, y P P Y T are in conict i
Dt, t1 P T, t t1 ^ t X t1 H ^ t ⁄ x ^ t1 ⁄ y; 3. the concurrency relation, denoted as co : two nodes are concurrent if they are not in conict and neither of them causally depends on the other. For a set B of nodes we write co pBq i all nodes in B are pairwise concurrent.
An occurrence net is a safe P/T-net ON p B, E, Gq s.t. 1. ON is acyclic; 2. @p P B : | p| ⁄ 1; 3. @x P B Y E the set ty | y xu is nite, i.e., each node in ON has a nite set of predecessors; 4. @x P B Y E : px#xq, i.e., no node is in self-conict.
In occurrence nets, elements from B are usually called conditions and elements from E are called events.
A conguration C in an occurrence net ON p B, E, Gq is a non-conicting subset of nodes, which is downwards-closed under , i.e., @x, y P C : px#yq, and px yq ^ y P C implies x P C. For each x P B Y E we dene a local conguration of x to be rxs t y | y P B Y E, y xu. The denition of a local conguration can be straightforwardly generalized to any non-conicting set of nodes X B Y E, namely rXs t y | y P B Y E, x P X, y xu.
We dene the set of branching processes of a given marked P/T-net N pP, T, F, M0q using the so-called canonical representation .
The set C of canonical names for N is dened recursively to be the smallest set s.t. if x P P Y T and A is a nite subset of C, then pA, xq P C.
A C-Petri net is an occurrence net pB, E, Gq such that: B Y E C; @pA, xq P B Y E, pA, xq A.
The initial marking of a C-Petri net is a subset of nodes tpH, xq | pH, xq P Bu. For each C-Petri net CN , the morphism h maps the nodes of CN to the nodes of N : hppA, xqq x. If hpyq z, we say that y is labeled by z.
Let S be a (nite or innite) set of C-Petri nets. The union of S is dened component-wise, i.e.,
S p
pP,T,F,MqPS P, pP,T,F,MqPS T, pP,T,F,MqPS F, pP,T,F,MqPS M q.
The set of branching processes of a marked P/T-net N p P, T, F, M0q is dened as the smallest set of C-Petri nets satisfying the following conditions: 1. The C-Petri net pI, H, Hq, where I tpH , pq | p P M0u (consisting of conditions I and having no events), is a branching process. 2. LMet1 B1 be a branching process and M be a reachable marking of B1, and
M , such that hpM 1q t for some t in T . Let B2 be a net obtained by adding an event pM 1, tq and conditions tptpM 1, tqu, pq | p P t u to B1. Then B2 is a branching process. 3. Let BB be a (nite, or innite) set of branching processes. The union BB is a branching process.
An example of a P/T-net and its branching process is shown in Figs. 1 and 2. The P/T-net P N 1 has the initial marking tp1u and is shown in Fig. 1. One of its possible branching processes is shown in Fig. 2, where the labeling function h is indicated by labels on nodes.
p1 t1 p2 t2 t3 t4 t5 t6 p3 p4 p5 p6 p1 t1 p2 t2 t3 p3 p4 p5 t4 t5 p6 p6 t6 t6 p1 p1
The fundamental property of P/T-nets unfoldings [
t 2. if there is a step M such that hptU q
t ^ hpM U1 q M 1. t
M 1 of N , M U1 in U pN q,
In other words, the fundamental property of unfoldings states that the reachability graph of the unfolding is isomorphic to the reachability graph of the P/T-net. This property is crucial for the use of unfoldings in semantic study and verication.
Unfoldings were dened and studied for dierent classes of Petri nets, namely
for high-level Petri nets [
Nested Petri Nets
In this paper we deal with nested Petri nets (NP-nets) in particular, a proper
subclass of NP-nets called strictly conservative NP-nets. The basic denition
of nested Petri nets can be found in [
In nested Petri nets (NP-nets) , tokens may be Petri nets themselves. An NP-net consists of a system net and element nets. We call these nets the NPnet components. Marked element nets are net tokens. Net tokens, as well as usual black dot tokens, may reside in places of the system net. Some transitions in NP-net components may be labeled with synchronization labels . Unlabeled transitions in NP-net components may re autonomously, according to the usual rules for Petri nets. Labeled transitions in the system net should synchronize with transitions (labeled by the same label) in net tokens involved in this transition ring.
In strictly conservative NP-nets, net tokens cannot evolve or disappear. They can move from one place in a system net to another and change their marking, i.e., inner state. In the basic NP-net formalism new net tokens may be created, copied and removed as usual Petri net tokens. It should be noted that although this restriction is rather strong, many interesting multi-agent systems can be modeled with conservative NP-nets.
Here we consider safe and typed NP-nets, i.e., each place in a system net can contain no more than one token: either a black dot token, or a net token of a specic type.
Figure 3 provides an example of a nested Petri net NP1. On the left one can see a system net. The token residing in the place Res is a net token. Its structure and initial marking is shown on the right side of the gure. The net token Release1 R x x
Res x x q1 t2 q2 L Lock2 x
q3 x R Release2 q4 a1
Lock
L Release R a2 a3
SomeW ork represents some sort of resource (for example, a networking or a computational one), capable of performing some internal work (actions). Two threads are trying to access the same resource, but the locking mechanism is preventing them from accessing it simultaneously. The system net synchronizes with the element nets via transitions Lock1, Lock2 and Release1,Release2.
Denition 1 (Nested Petri nets). Let Type be a set of types, Var a set of typed (over Type) variables, and Lab a set of labels. A (typed) nested Petri net (NP-net) NP is a tuple pSN, pE1, . . . , Ekq, υ, λ, W q, where
SN p PSN, TSN, FSNq is a P/T net called a system net; for i 1, k, Ei p PEi , TEi , FEi q is a P/T net called an element net, where all sets of places and transitions in the system and element nets are pairwise disjoint; we suppose, each element net is assigned a type from Type; without loss of generality we shall assume, that Type t E1, . . . , Eku; υ : PSN Type Y tu is a place-typing function ; λ : TNP Lab is a partial transition labeling function, where TNP TSN Y TE1 Y Y TEk ; we write that λptq K when λ is undened at t.
W : FSN Var Y tu is an arc labeling function s.t. for an arc r adjacent to a place p the type of W prq coincides with the type of p.
A marked element net is called a net token.
In what follows for a given NP-net by Anet tp EN, mq | Di 1, . . . , k : EN Ei, m P MpENqu we denote the set of all (possible) net tokens, and by A Anet Y tu the set of all net tokens extended with a black dot token.
Now we come to dening NP-net behavior.
A marking M in an NP-net NP is a function mapping each p P PSN to some (possibly empty) multiset M ppq over A in accordance with the type of p. Thus a marking in an NP-net is dened as a marking of its system net. By abuse of notation, a set of all markings of an NP-net NP will be denoted by MpNPq. We say that a net token pEN, mq resides in p (under marking M ), if M ppq P pEN, mq.
Let t be a transition in SN, t t p1, . . . , piu, t t q1, . . . , qj u be sets of its pre- and post-elements. Then W ptq t W pp1, tq, . . . , W ppi, tq, W pt, q1q, . . . , W pt, qj qu will denote a set of all variables in arc labels adjacent to t. A binding of t is a function b assigning a value bpvq (of the corresponding type) from A to each variable v occurring in W ptq.
A transition t in SN is enabled in a marking M w.r.t. a binding b i @p P t : W pp, tqpbq M ppq, i. e. each input place p adjacent to t contains a value of input arc label W pp, tq.
The enabled transition res yielding a new marking M 1, write M M 1, such that for all places p, M 1ppq p M ppqzW pp, tqpbqq Y W pt, pqpbq.
For net tokens from Anet, which serve as values for input arc variables from W ptq, we say, that they are involved in the ring of t. (They are removed from input places and brought to output places of t).
There are three kinds of steps in an NP-net NP.
An element-autonomous step. Let t be a transition without synchronization labels in a net token. Then an autonomous step is a ring of t according to the usual rules for P/T-nets. An autonomous step in a net token does not change the residence of this net token.
A system-autonomous step is the ring of an unlabeled transition t P TSN in
the system net according to the ring rule for high-level Petri nets (e.g., colored
Petri nets [
A synchronization step. Let t be a transition labeled λ in the system net SN, let t be enabled in a marking M w.r.t. a binding b and let α1, . . . , αn P Anet be net tokens involved in this ring of t. Then t can re provided that in each αi (1 ⁄ i ⁄ n) a transition labeled by the same synchronization label λ is also enabled. The synchronization step goes then in two stages: rst, ring of transitions in all net tokens involved in the ring of t and then, ring of t in the system net w.r.t. binding b.
An NP-net NP is called safe i in every reachable marking in NP there are not more than one token in each place in the system net, and not more that one token in each net token place. Hereinafter we consider only safe NP-nets. 2.4
Conservative NP-nets Now we give a denition of (strictly) conservative NP-nets , as well as some related denitions. We then dene an unfolding operation for a simple class of strictly conservative nets.
Denition 2. conservative i
A safe NP-net N p SN, pE1, . . . , Ekq, υ, λ, W q is called strictly 1. For each t P TSN and for each p P t, D!p1 P t . W pp, tq
W pp, tq 2. For each t P TSN and for each p P t , D!p1 P t . W pp1, tq
W pp, tq W pt, p1q or W pt, pq or
The denition of strict conservativeness ensures that no net token emerges or disappears after a transition ring in the system net.
Note that in [
In conservative nets, instead of considering net tokens (marked element nets residing in places of the system net), we consider identied net tokens: triples xid, EN, my, where id is a unique identier of the token, EN is a structure of the token (i.e., an element net from the set tE1, . . . Eku), and m is a marking in EN. Then every net token in the system net has a unique identier attached to it; thus, tokens with the same marking can be distinguished.
Further we use NTok to denote a set of identied net tokens for a given net. Sometimes, by abuse of notation, for a net token η x id, EN, my in a place x of a marking M , we write M pxq η meaning M pxq tp EN, mqu. By τ pηq we denote a type of a net token pEN, mq, and by Pη (Tη) we denote the set of places (transitions) of the net token, i.e., PEN (TEN). In the rest of the paper we will use the term net token to mean identied net token .
Given a system net SN, a set of net tokens NTok, and a function M mapping places of SN to identiers of NTok, it is easy to restore the set of element nets (which is just a set of types from NTok), and a marking M (which can be easily restored from M). Thus, we speak about net tokens in a marking as separate entities, and, in order to dene an NP-net, we sometimes list identied net tokens.
For a marking M in an NP-net NP we dene marking projections onto the components of NP: 1. The projection of M onto a system net SN, denoted as M SN, is a marking of the at P/T-net SN obtained by replacing all the net tokens in M by black dot tokens, i.e., M SNppq | M ppq|. 2. The projection of M onto a net token η x id, EN, my, denoted as M η, is just m. 3
Translation of Safe Conservative NP-nets into P/T-nets As reachability graph of the unfolding is isomorphic to the reachability graph of the P/T-net, unfoldings can be used in verication. Since safe conservative nested Petri nets have nite number of states, it will be apparent to assume, that they can be translated into classical Petri nets and then can be unfolded according to the classical unfolding rules for further verication.
To make a correct translation we have to set a number of requirements for a translation. The main goal for building a model is the possibility to make a simulation. Simulation implies behavioral equivalence: a possibility to repeat all possible moves of one model on another model. Behavioral equivalence is guaranteed by establishing strong bisimulation equivalence between states of two models. The second requirement is about constructing a reachability graph. It means that we need exact correspondence between nodes (states) of our model. If these two requirements are met, we can build a translation algorithm which allows us to use target model having the same behavioral properties like original for verication and analysis.
Now we present an algorithm for translating a conservative safe nested Petri net into a safe P/T net.
The algorithm will be illustrated by an example of a NP-net NP2, shown in Fig. 4. Here the net on the left is a system net, and the nets on the right are net tokens residing in the places p1 and p2 of the system net. This net will be translated into a safe P/T net PN.
p2 x p1 t1 α x y y z t2 p3 z Element net in p1 : q1 q1 Element net in p2 : k2 k2 k1 α k1 α Fig. 4. NP-net NP2 q2 q2 k3 k3 The translation algorithm: Let NP p SN, pE1, . . . , Ekq, υ, λ, W q be an NPnet with a set NTok of identied net tokens in the initial marking. By I we denote the set of all identiers used in NTok, and by IE I the subset of all identiers for net tokens of type E. The net NP will be translated into a P/T net PN p PPN, TP N, FPNq with an initial marking m0. 1. First, we dene the set PPN of places of the target net PN. For each type E of some place in the system net SN we create a set SE of places for PPN. The set SE will contain a copy of each place of type E in the system net for each net token of type E (labeled by net token identiers) and a copy of each place in PE for each net token of type E, i.e. SE tp p, idq|p P PSN, υppq E, id P IE u Y tpq, idq|q P PE , id P IE u. For a place p in SN with black token type we create just one copy of p without any identier. Then the set PPN of places for the target net PN is created as the union of all these sets. 2. To dene the initial marking for PN we dene an encoding of markings on places from PNP in a NP-net by markings on constructed places from PPN. If a net token η p id, E, mq resides in a place p in a marking M of the system net, then in the target net there are black tokens in the place pp, idq, and all places pq, idq for all q s.t. mpqq 1. If a place of black token type in SN has a black token, then the only corresponding place in PN is also marked by a black token. It is easy to see that this encoding denes a oneto-one correspondence between markings in a safe conservative NP-net and safe markings in PN.
In our example the rst element net resides in a place p1, second - in p2. Thus, correspondingly, we dene marking in a places pp1, 1q and pp2, 2q. The same way marking for places pq1, 1q and pq1, 2q is dened. 3. For each autonomous transition t in a system net SN we build a set Tt of transitions as follows. Each input arc variable of t may be, generally speaking, be binded to any of identied net token of the corresponding type. So, for each such binding we construct a separate transition for PN with appropriate input and output arcs.
Thus for the transition t2 we construct two transitions: t21 and t22 . It is shown in Fig. 5. 4. For each autonomous transition in a net token from NTok identies= d with id we construct a similar transition on places labeled with id. Thus in our example net we obtain four transitions: k21 , k22 , k31 and k32 . Elementautonomous step is illustrated in Fig. 6. 5. A ring of a synchronization transition supposes simultaneous ring of a transition, which belongs to a system net, and ring of some transition, which has the same label in each involved net token. So synchronization step is a combination of Step 3 and Step 4. Thus as in our example there are two element nets, we add transitions for each net, marked with α1 and α2. Suchwise we can model a synchronization step for every possible initial marking in a system net, which is shown in Fig. 7. Theorem 1. Let NP be a NP-net. Let also PN be a P/T net, obtained from NP by the translation, described above. Then reachability graphs of NP and PN are isomorphic.
Proof. Step 2 of the algorithm denes a one-to-one correspondence between reachable markings of nets NP and PN. It is easy to see that according to translation denition corresponding ring steps in both nets do not violate this correspondence.
Thus we have proven that every safe conservative NP-net can be translated
to behaviorally equivalent safe P/T net. Then the standard algorithm for safe
P/T nets unfolding can be applied for NP-net verication. The problem here is
that the size of the resulting P/T net can grows vastly. In the next section we
describe the algorithm for direct unfolding of safe conservative NP-nets, presented
previously in [
First we introduce a concept of an element-indexed C-Petri net, a construction similar to the construction of the canonical net for a P/T-net; however, each place of the element-indexed C-net is paired with a net token (identier). In this section we suppose that NP p SN, pE1, . . . , Ekq, υ, λ, M 0q is a conservative NP-net, where SN p PSN, TSN, FSNq, Ei p PEi , TEi , FEi q, 0 i ⁄ k. Denition 3 (Element-indexed C-Petri nets). An element-indexed C-net Θ for some element-indexing set J is a C-net such that each place in Θ is marked with an element of J . For our purposes, the set J will be the set of the identied net tokens.
Formally, for a xed net NP, a set of canonical names C is dened as follows: If x P p Ei PEi Y PSNq, ηi P N T ok Y tu , and X is a nite subset of C, then pX, x, ηiq P C; If x p Ei TEi Y TSNq, and X is a nite subset of C, then pX, xq P C.
Then an indexed C-net pP, T, F, M0q is a P/T-net, such that 1. P Y T C; 2. If p p X, x, ηq P P , then p 3. If t p X, xq P P , then t 4. pX, x, ηq P M0 i X H
X;
X; and x P p
The union of element-indexed C-Petri nets is dened component-wise, exactly as it was done for regular C-Petri nets.
We also dene a notion of an adjacent place. According to Denition 2, for every pair pp, tq P PSN TSN, where υppq ^ pp p, tq P FSN _ pt, pq P FSNq, there exists a unique place p1 in a system net such that W pp, tq W pt, p1q or W pp1, tq W pt, pq. Such a place p1 is said to be adjacent to p via t (denoted by xp|,ty). For example, in Fig. 4 the place adjacent to p2 via t1 is xp~2,t1y p3.
Now we are ready to dene a set of element-indexed branching processes (or branching processes for short, when there is no ambiguity) for a given conservative NP-net NP.
Denition 4 (Element-indexed branching processes for conservative nested Petri nets).
The set of element-indexed branching processes for NP is the smallest set of element-indexed C-nets satisfying the following rules: 1. Let
C tpH , p, ηiq | p P PSN, ηi P M 0ppqu Y tpH, p, ηiq | ηi P NTok, p P M 0ηi u be a set of places. The net Θ p C, H, Hq consisting of conditions C and having no transitions is a branching process. Such branching process is said to be initial. 2. Let Θ be a branching process, and B be a subset of conditions of Θ. If B satises the P osEN rule’s premise (Fig. 9), then the net obtained by adding an event e and conditions C to Θ is a branching process. 3. Let Θ be a branching process, and B be a subset of conditions of Θ. If B satises the P osSN rule’s premise (Fig. 9), then the net obtained by adding an event e and conditions C to Θ is a branching process. 4. Let Θ be a branching process, and let B and BE be subsets of conditions of Θ. If B and BE satisfy the P osSync rule’s premise (Fig. 9), then the net obtained by adding an event e and conditions C to Θ is a branching process.
The SyncCond predicate is dened below. 5. Let BS be a (nite or innite) set of branching processes. The union BS is a branching process.
In rules (2)-(4), event e is called a possible extension of Θ.
The SyncCond predicate in rule (4) makes sure that all the components involved in the synchronization step, synchronize correctly. The parameter I contains the id’s of all the net tokens involved in the step. The set E consists of transitions ti in each of the net tokens ηi (i P I), and every ti carries the same label as the transition t from the system net. In order for the synchronization step to go through, each of the ti needs to have its pre-set tcj | j P Jiu active. The places of net tokens corresponding to those in the pre-sets are contained in BE . t P Tηk , λptq K C pPt pe, p, ηkq t t bi | i P Iu B tp xi, bi, ηiq | i P Iu copBq t P TSN, λptq K
t t bi | i P Iu e p B, ttuq and
C tp e, xb}i, ty, ηiq | i P I, ηi uY
tpe, b, q | b P t , υpbq u
B tp xi, bi, ηiq | i P Iu t P TSN, λptq K copB Y BEq t t bi | i P Iu
e p B Y BE, ttu Y Eq and
C tp e, xb}i, ty, ηiq | i P I, ηi uY tpe, b, q | b P t , υpbq uY tpt1, c1i, ηiq | i P I, ηi c1i P Pηi , c1i P ti u , 1. BE iPI tpyj , cj , ηiq | j P Ji, ηi p idi, ENi, μiq P NTok, cj P PENi u ^ copBE q, i.e., BE is a set of reachable conditions that correspond to places in net tokens; 2. E t ti P TENi | i P I, ηi p idi, ENi, μiq P NToku, i.e., E is a subset of transitions in each of the net tokens; 3. @ti P E, λptiq λptq 4. E iPI tcj | j P Ji, ηi P NToku
The rules in Fig. 9 can be explained informally from the operational point of view. Rules P osEN , P osSN , and P osSync are used for generating events that correspond to element-autonomous, system-autonomous, and synchronized rings, respectively.
A possible branching process of NP2 is shown in Fig. 10. In Fig. 10, a transition is labeled with t, if it is of the form pA, tq, and a place is labeled with pp, N q if it is of the form pA, p, N q.
tk3u . . .
tk3u pq2, N1q tk3u pq1, N1q tk2u pq2, N1q tk3u
It was proven in [
Note also that every low-level P/T-net is a special case of an NP-net with
the empty set of element nets and no vertical synchronization. It was shown
also in [
Comparing Two Ways of Nested Petri Net Unfolding We have shown that each conservative safe NP-net can be converted into a behaviorally equivalent classical Petri net, namely their reachability graphs are isomorphic. So, to construct unfoldings for a NP-net we can either translate it into a P/T net and then apply the classical P/T net unfolding procedure, or directly construct NP-nets unfoldings, as it is described in the previous subsection.
The fundamental property of unfoldings states that the reachability graph of the unfolding is isomorphic to the rechability graph of the initial net. Since the fundamental property holds both for P/T net unfoldings and for NP-net unfoldings, we can immediately conclude that both approaches give the same (up to isomorphism) branching process. For our example this is demonstrated by Fig. 10 and Fig. 12.
The dierence is in the complexity of these two solutions. It is easy to see, that when there are several net tokens of the same type in the initial marking, the translation leads to a signicant net growth. Thus e.g. for a system net
tk3u k2 pq2, N2q tk3u pq1, N2q tk2u pq2, N2q
pq2, N2q tk3u pq1, N2q tk2u pq2, N2q k2 α . . . transition t with n input places of the same type and k tokens of this type in the initial marking we are to construct kn copies of this transition in the target P/T net, corresponding to dierent bindings for t-rings. And it is rather clear, that we cannot avoid this, since we are to distinguish markings of net tokens residing in dierent places, and hence to construct a separate P/T net transition for each mode of a system net transition ring.
To check the advantage of the direct unfolding method w.r.t. time complexity for concrete examples we’ve developed a software application which allows 1. translation of a conservative safe nested Petri net into a P/T net and then building an unfolding for it; 2. building an unfolding directly for a nested Petri net.
We expected that a large number of net tokens will cause signicant net growth during translation. The reason for this is that dealing with a system, which consists of a large number of net tokens and incoming arcs, translation of a nested Petri net into a P/T net leads to a signicant growth of the net graph. Since we do not know in advance, which modes of transition ring will be used in the unfolding, we should build an intermediate P/T net with a lot of transitions unnecessary for unfolding, while in direct unfoldings these transition nodes do not appear.
So, we conducted experiments on nets having similar structure, but dierent number of element nets with dierent types. We’ve done a series of experiments with rather small models, which conrm our assumptions. Thus for our example net NP2 we’ve got 0.38 ms. for the direct unfolding, and 0.54 ms. for unfolding via the translation into a P/T net. So, even in the case of two net tokens we get a noticeable dierence in time.
To get representative experiment results we are to do more experiments with larger models of dierent structure.
Application to verication. Having the described above algorithm for NP-nets
unfoldings the basic algorithm (described in [
For example, let’s consider the result of the standard algorithm applied to the
NP-net NP2 from Fig. 4 using the McMillan’s cutting context (in the notation
of [
We have shown a canonical prex for NP2 in Fig. 11. This canonical prex BP C allows us to solve the executability problem: a transition t may re in the NP-net i an event labeled with t is presented in the canonical branching process. For example, one can observe, that because a transition e1 in BP 2 has is labeled with tt1, k1u, the transition t1 is executable in the NP-net. Also, we can easily see that for both tokens k1 may re only once, but k2 and k3 are live transitions. 5
In this paper we’ve proposed and compared two ways of unfolding for safe
conservative nested Petri nets. The rst method is based on equivalent translation
of NP-nets into safe P/T nets and then applying standard unfolding procedure
described in the literature. The second method is a direct unfolding, proposed
and justied earlier in [
For that we’ve developed and justied an algorithm for translation of a safe conservative NP-net into an equivalent P/T net. Direct analysis of the algorithm complexity allows us to conclude that the direct unfolding has a distinct advantage in time complexity. To check this advantage with practical examples we’ve implemented the algorithms for translation and unfolding. Experiments on small nets have demonstrated the anticipated benets of direct unfolding.
For further work, we plan to enlarge the complexity of nets and number of experiments.