=Paper=
{{Paper
|id=Vol-1591/paper9
|storemode=property
|title=Verification of Nested Petri Nets Using an Unfolding Approach
|pdfUrl=https://ceur-ws.org/Vol-1591/paper9.pdf
|volume=Vol-1591
|authors=Irina A. Lomazova,Vera O. Ermakova
|dblpUrl=https://dblp.org/rec/conf/apn/LomazovaE16
}}
==Verification of Nested Petri Nets Using an Unfolding Approach==
https://ceur-ws.org/Vol-1591/paper9.pdf
Veri cation of Nested Petri Nets Using an
Unfolding Approach
Irina A. Lomazova, and Vera O. Ermakova
National Research University Higher School of Economics,
Myasnitskaya ul. 20, 101000 Moscow, Russia
ilomazova@hse.ru voermakova@edu.hse.ru
Abstract. Nested Petri nets (NP-nets) is an extension of the Petri nets
formalism within the nets-within-nets approach, allowing to model sys-
tems 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 veri cation and compare unfolding
of NP-net translated into classical Petri net with direct component-wise
unfolding.
Keywords: Multi-agent systems, veri cation, Petri nets, nested Petri
nets, unfoldings.
1 Introduction
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 com-
puter science today. They are used in various practical elds and areas, such
as arti cial intelligence, cloud services, grid systems, augmented reality systems
with interactive environment objects, information gathering, mobile agent coop-
eration, 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 [1], can
be used. Nested Petri nets follow 'nets-within-nets' approach [2] and naturally
represent multi-agent systems structure, because tokens in the main system net
are Petri nets themselves, and can have their own behavior.
model checking
To check nested Petri net model properties one of the most popular veri ca-
tion method, , could be used. The basic idea of model checking
is to build a reachability (transition) graph and check properties on this graph.
This work is supported by the Basic Research Program at the National Research
University Higher School of Economics and Russian Foundation for Basic Research,
project No.16-01-00546.
94 PNSE’16 – Petri Nets and Software Engineering
However, there is a crucial problem for veri cation 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 [3,4] was introduced. In [5] applica-
bility of unfoldings for nested Petri nets was studied and the method for con-
structing unfoldings for safe conservative nested Petri nets was proposed. It was
proven there, that unfoldings for nested Petri nets satisfy the unfoldings fun-
damental property, and thus can be used for veri cation of conservative nested
Petri nets similar to the classical unfoldings methods. Classical unfoldings are
conservative safe nested Petri nets
de ned for P/T nets, but in this paper we deal with a restricted subclass of
nested Petri nets . This means that net
tokens, representing agents, cannot be destroyed or created, but can change
their location in the system net and can change their inner states. Thus, the
number of agents is constant and each agent can be identi ed. It was shown
in [5] that for conservative safe nested Petri nets unfoldings can be constructed
in a component-wise manner, what makes practical veri cation of such models
feasible.
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 [5] is really better than constructing unfoldings via
translation of nested Petri nets into safe P/N nets in terms of time complexity.
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 experi-
mentally.
Related Work Nested Petri nets (NP-nets) are widely used in modeling of dis-
tributed systems [6,7,8], serial or recon gurable systems [9,10,11], protocol veri-
cation [12], coordination of sensor networks with mobile agents [13], innovative
space system architectures [14], grid computing [15].
Several methods for NP-nets behavioral analysis were proposed in the litera-
ture, among them compositional methods for checking boundedness and liveness
for nested Petri nets [16], translation of NP-nets into Colored Petri nets in order
to verify them with CPNtools [17], veri cation of a subclass of recursive NP-nets
with SPIN [18].
unfoldings
Unfolding approach and state-space explosion problem are explicitly studied
in the literature. The original development in (of P/T-nets) is due
complete nite pre xes
to [19]. McMillan [3] was the rst to use unfoldings for veri cation. He intro-
duced the concept of of unfoldings, and demonstrated
the applicability of this approach to the veri cation of asynchronous circuits.
I.A. Lomazova and V. Ermakova: Verification of Nested Petri Nets 95
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 ([20,21,22]
to name a few); and the approach has been applied to high-level Petri nets [23],
process algebras [24] and M-nets [23].
The general method for truncating unfoldings, which abstracts from the in-
cutting context
formation one wants to preserve in the nite pre x of the unfolding, was proposed
in [25,26]. This method is based on the notion of a . We use this
approach for de ning branching processes and unfoldings of conservative nested
Petri nets.
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 de ned and compared with con-
structing unfoldings via into P/T nets translation. The last section gives some
conclusions.
2 Preliminaries
Multisets. S multiset m over a set S is a function m : S Ñ
Nat Nat
Let be a nite set. A
, where 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, m
1 we write m m1 i @s P S : mpsq ¤ m1 psq (the
inclusion relation). The sum and the union of two multisets m and m are de ned
1
as usual: @s P S : pm m1 qpsq mpsq p q pm Y qpsq maxpmpsq, m1 psqq.
m1 s , m1
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 pP, T, F q is called a P/T-net.
A marking in a P/T-net N pP, 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, M0 q is
a P/T-net together with its initial marking M 0.
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 m p p q tokens into
each place p P P.
P T , an arc px, tq is called an input arc, and an arc pt, xq
For a transition t
an output arc P P Y T , we de ne the pre-set as x ty |
. For each node x
py, xq P F u and the post-set as x ty | px, yq P F u.
We say that a transition t in a P/T-net N pP, 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
96 PNSE’16 – Petri Nets and Software Engineering
a (possibly empty) sequence of rings M0 ÝtÑ M1 ÝtÑ M2 Ñ
1 2
Ý ÝÑ M from
the initial marking to M . By RM N, M0 p q we denote the set of all reachable
pN, M0 q.
safe
markings in
A marking M is called P P we have M ppq ¤ 1. A
i for all places p
marked P/T-net N is called safe P RMpN, M0 q
i every reachable marking M
is safe. A reachability graph of a P/T-net pN, M0 q presents detailed informa-
tion about the net behavior. It is a labeled directed graph, where vertices are
reachable markings in pN, M0 q, and an arc labeled by a transition t leads from
a vertex v , corresponding to a marking M , to a vertex v , corresponding to a
1
marking M
1 i M Ñ
Ý M 1 in N .
t
2.2 Classical Petri Nets Unfoldings
Branching processes and unfoldings of P/T-nets. Unfoldings are used to de ne
non-sequential (true concurrent) semantics of P/T-nets, and complete pre xes
of unfoldings are used for veri cation. Here we give necessary basic notions and
de nitions, connected with unfoldings. Further details can be found in [27,28].
pP, T, F q be a P/T-net. The following relations are de ned on the
Let N
set P Y T of nodes in N :
1. the causality relation, denoted as , is the transitive closure of F , and ¤ is
con ict
the re exive closure of ; if x y , we say that y causally depends on x.
2. the #
relation, denoted as x, y P P Y T : nodes are in con ict i
Dt, t P T, t t ^ t X t H ^ t ¤ x ^ t ¤ y
1 1 1 1
concurrency co concurrent
;
3. the relation, denoted as : two nodes are if they
are not in con ict and neither of them causally depends on the other.
B co pBq B
occurrence net ON pB, E, Gq
For a set of nodes we write i all nodes in are pairwise concurrent.
An is a safe P/T-net s.t.
1. ON is acyclic;
@p P B : | p| ¤ 1
ON
2. ;
3. @x P B Y E ty | y xu
the set is nite, i.e., each node in has a nite set
of predecessors;
4. @x P B Y E : px#xq, i.e., no node is in self-con ict.
In occurrence nets, elements from B are usually called conditions
events
and elements
from E are called
con guration C ON pB, E, Gq
.
A in an occurrence net is a non-con icting
@x, y P C : px#yq,
local
subset of nodes, which is downwards-closed under , i.e.,
px y q ^ y P C implies x P C . For each x P B Y E we de ne a
con guration of x
and
to be rxs ty | y P B Y E, y xu. The de nition of a local
con guration can be straightforwardly generalized to any non-con icting set of
nodes X B Y E , namely rX s ty | y P B Y E, x P X, y xu.
We de ne the set of branching processes of a given marked P/T-net N
pP, T, F, M0 q using the so-called canonical representation.
The set C of canonical names for N is de ned 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:
I.A. Lomazova and V. Ermakova: Verification of Nested Petri Nets 97
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 B u.
For each C -Petri net CN , the morphism h maps the nodes of CN to the nodes
of N : h ppA, xqq x. If hpyq z, we say that y is labeled by z.
Let S be a ( nite or in nite) set of C -Petri nets. The union of S is de ned
S p
component-wise, i.e.,
q
pP,T,F,M qPS P, pP,T,F,M qPS T, pP,T,F,M qPS F, pP,T,F,M qPS M .
The set of branching processes of a marked P/T-net N pP, T, F, M0 q is
de ned 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 M0 u (consisting of
conditions I and having no events), is a branching process.
2. Let B1 be a branching process and M be a reachable marking of B1 , and
M 1 M , such that hpM 1 q t for some t in T . Let B2 be a net obtained by
adding an event pM , tq and conditions tptpM , tqu, pq | p P t u to B1 . Then
1 1
B2 is a branching process.
3. Let BB be a ( nite, or in nite) 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 tp1 u 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.
t6
t2 p3 t4
p2 t2 p3 t4 p6 t6 p1
p2
p1 t1 t3 p4 t5 p6
p1 t1 t3 p4 t5 p6 t6 p1
p5 p5
Fig. 1. Petri net P N 1 Fig. 2. Branching process of P N 1
A branching process B1 ppP1 , E1 , F1 q, h1 q is called a pre x of a branching
process B2 ppP2 , E2 , F2 q, h2 q (denoted B1 B2 ) i P1 P2 and E1 E2 .
The union of branching processes is called the unfolding of N . It is easy to
see, that the unfolding is the maximal branching process w.r.t the pre x relation
.
The fundamental property of P/T-nets unfoldings [28] states that the behav-
ior of the unfolding is equivalent to the behavior of the original net. Formally it
can be formulated as follows.
98 PNSE’16 – Petri Nets and Software Engineering
Fundamental property of P/T-nets unfoldings. Let M be a reachable marking
in a P/T- net N , and let MU be a reachable marking in U pN q s.t. hpMU q M .
Then
1. if there is a step MU ÝÑ
t
MU1 of U pN q, then there is a step M Ñ
U
Ýt M 1 of N ,
such that hptU q t ^ hpMU q M ;
1 1
Ýt M 1 of N , then there is a step MU ÝÑ
2. if there is a step M Ñ MU1 in U pN q,
t U
such that hptU q t ^ hpMU q M .
1 1
In other words, the fundamental property of unfoldings states that the reach-
ability 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 veri cation.
Unfoldings were de ned and studied for dierent classes of Petri nets, namely
for high-level Petri nets [23], contextual nets [29], time Petri nets [30], Hypernets
[31] (to name a few). All these constructions has similar properties, which act
as a sanity check. Further in the paper we de ne an unfolding operation for
nested Petri nets, which posses a similar fundamental property.
2.3 Nested Petri Nets
strictly conservative
In this paper we deal with nested Petri nets (NP-nets) in particular, a proper
subclass of NP-nets called NP-nets. The basic de nition
of nested Petri nets can be found in [1,8]. Here we give a reduced de nition,
nested Petri nets (NP-nets)
su cient for de ning conservative NP-nets.
system net element nets
In , tokens may be Petri nets themselves. An
components net tokens
NP-net consists of a and . We call these nets the NP-
net . Marked element nets are . Net tokens, as well as
synchronization labels
usual black dot tokens, may reside in places of the system net. Some transitions
in NP-net components may be labeled with . 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
safe typed
modeled with conservative NP-nets.
Here we consider and 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
NP
speci c type.
Figure 3 provides an example of a nested Petri net 1 . 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
I.A. Lomazova and V. Ermakova: Verification of Nested Petri Nets 99
p1 q1
t1 t2
Lock
a1 L
p2 q2
a2
Lock1 L L Lock2
x x
x Res x
p3 q3 SomeW ork
x x
x x
Release1 R R Release2 Release R a3
p4 q4
Fig. 3. NP-net NP1
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 Lock 1 , Lock 2 and Release1 ,Release2 .
De nition 1 (Nested Petri nets). Let Type be a set of types, Var a set of
typed (over Type) , and Lab a set of labels. A (typed)
NP is a tuple pSN, pE , . . . , E q, υ, λ, W q, where
variables nested Petri
net (NP-net) 1 k
SN pPSN , TSN , FSN q is a P/T net called a ;
for i 1, k, E pP , T , F q is a P/T net called an , where
system net
all sets of places and transitions in the system and element nets are pairwise
i Ei Ei Ei element net
disjoint; we suppose, each element net is assigned a type from Type; without
loss of generality we shall assume, that Type tE , . . . , E u;
υ : PSN Ñ Type Y t u is a ;
1 k
λ : TNP Ñ Lab is a partial transition labeling function, where TNP TSN Y
place-typing function
T Y Y T ; we write that λptq K when λ is unde ned at t.
W : FSN Ñ Var Y t u is an s.t. for an arc r adjacent
E1 Ek
to a place p the type of W prq coincides with the type of p.
arc labeling function
A marked element net is called a . net token
Anet tpEN, mq | Di 1, . . . , k : EN
E , m P MpENqu
In what follows for a given NP-net by
i A
we denote the set of all (possible) net tokens, and by
Anet Y t u the set of all net tokens extended with a black dot token.
marking M NP is a function mapping each p P PSN to some
Now we come to de ning NP-net behavior.
A in an NP-net
(possibly empty) multiset M ppq over A in accordance with the type of p. Thus
a marking in an NP-net is de ned as a marking of its system net. By abuse of
100 PNSE’16 – Petri Nets and Software Engineering
NP will be denoted by MpNPq. We
pEN, mq resides in p (under marking M ), if M ppq P pEN, mq.
notation, a set of all markings of an NP-net
Let t be a transition in SN, t tp1 , . . . , pi u, t tq1 , . . . , qj u be sets of its
say that a net token
pre- and post-elements. Then W ptq tW pp1 , tq, . . . , W ppi , tq, W pt, q1 q, . . . , 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 b v p q (of the corresponding type) from A to each
variable v occurring in W ptq.
A transition t in SN enabled
is 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 , write M Ñ M ,
1 1
such that for all places p, M ppq pM ppqzW pp, tqpbqq Y W pt, pqpbq.
1
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).
NP
An element-autonomous step.
There are three kinds of steps in an NP-net .
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
system-autonomous step
the residence of this net token.
A 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
A synchronization step. SN
Petri nets [32]), as described above.
Let t be a transition labeled λ in the system net ,
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 de nition of (strictly) conservative NP-nets , as well as some
related de nitions. We then de ne an unfolding operation for a simple class of
strictly conservative nets.
De nition 2. A safe NP-net N pSN, pE , . . . , E q, υ, λ, W q is called
i
1 k strictly
conservative
1. For each t P TSN and for each p P t, D!p P t . W pp, tq W pt, p q or
1 1
W pp, tq
2. For each t P TSN and for each p P t , D!p P t . W pp , tq W pt, pq or
1 1
W pp, tq
I.A. Lomazova and V. Ermakova: Verification of Nested Petri Nets 101
The de nition of strict conservativeness ensures that no net token emerges
or disappears after a transition ring in the system net.
Note that in [33] NP-nets are called conservative, i tokens cannot disappear
after a transition ring, but can be copied; hence, the number of net tokens in
such conservative NP-nets can be unlimited. Here we consider a more restrictive
subclass of NP-nets with a stable set of net tokens (tokens cannot be copied).
Hereinafter we consider only strictly conservative NP-nets, and call them just
conservative nets for short.
identi ed
In conservative nets, instead of considering net tokens (marked element nets
xid, EN, my, where id is a unique identi er of the token, EN is a structure of the
residing in places of the system net), we consider net tokens: triples
token (i.e., an element net from the set tE1 , . . . Ek u), and m is a marking in EN.
Then every net token in the system net has a unique identi er attached to it;
NTok
thus, tokens with the same marking can be distinguished.
xid, EN, my in a place x
Further we use to denote a set of identi ed net tokens for a given net.
Sometimes, by abuse of notation, for a net token η
of a marking M , we write M pxq η meaning M pxq tpEN, 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., P EN (TEN ). In the rest of the paper we will
net token identi ed net token
SN NTok
use the term to mean .
SN NTok
Given a system net , a set of net tokens , and a function M mapping
NTok
places of to identi ers of , it is easy to restore the set of element nets
(which is just a set of types from ), 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 de ne an NP-net, we sometimes list identi ed net
NP marking projections
tokens.
For a marking M in an NP-net
NP
we de ne onto the
components of :
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æ SN ppq |M ppq|.
2. The projection of M onto a net token η xid, 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 veri cation. 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 veri cation.
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
102 PNSE’16 – Petri Nets and Software Engineering
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 veri cation and analysis.
Now we present an algorithm for translating a conservative safe nested Petri
NP
net into a safe P/T net.
The algorithm will be illustrated by an example of a NP-net 2 , 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 .
p3 k2
p2 Element net in p1 :
k1 q2 k3
q1 α
x y y
t1 α z z
k2
x
Element net in p2 :
k1 q2 k3
p1 t2 q1 α
Fig. 4. NP-net NP2
The translation algorithm: Let NP pSN, pE , . . . , E q, υ, λ, W q
NTok
1 k be an NP-
of identi ed net tokens in the initial marking. By I we
NTok
net with a set
I I
NP
denote the set of all identi ers used in , and by E the subset of all
E
PN pPPN, T N, FPNq
identi ers for net tokens of type . The net will be translated into a P/T
net P with an initial marking m0 .
1. First, we de ne the set P PN 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 P PN .
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 identi ers) and a copy of each
place in PE for each net token of type E , i.e. SE tpp, 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
I.A. Lomazova and V. Ermakova: Verification of Nested Petri Nets 103
type we create just one copy of p without any identi er. Then the set P PN
PN
PN
of places for the target net is created as the union of all these sets.
2. To de ne the initial marking for we de ne an encoding of markings on
places from P NP in a NP-net by markings on constructed places from PPN .
If a net token η pid, 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. mpq q 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 de nes a one-
PN
to-one correspondence between markings in a safe conservative NP-net and
safe markings in .
In our example the rst element net resides in a place p1 , second - in p2 .
Thus, correspondingly, we de ne marking in a places pp1 , 1q and pp2 , 2q. The
pq1 , 1q and pq1 , 2q is de ned.
SN
same way marking for places
3. For each autonomous transition t in a system net we build a set Tt of
transitions as follows. Each input arc variable of t may be, generally speaking,
PN
be binded to any of identi ed net token of the corresponding type. So, for
each such binding we construct a separate transition for with appropriate
input and output arcs.
Thus for the transition t2 we construct two transitions: t21 and t22 . It is
shown in Fig. 5.
p p 3 , 1q k31 pp3 , 1q
p q 1 , 1q pq1 , 1q
k21
p p 1 , 1q p p 1 , 1q
t 21
pq2 , 1q pq2 , 1q
pp2 , 1q p p 2 , 1q
pp2 , 2q p p 2 , 2q
p p 1 , 2q pq2 , 2q p p 1 , 2q pq2 , 2q
t 22
k22
p q 1 , 2q pq1 , 2q k32
p p 3 , 2q pp3 , 2q
Fig. 5. System-autonomous step Fig. 6. Element-autonomous step
104 PNSE’16 – Petri Nets and Software Engineering
4. For each autonomous transition in a net token from identi es=d with NTok
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 . Element-
autonomous 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.
p p 3 , 1q
p q 1 , 1q pp3 , 1q
k31
pq1 , 1q
p p 1 , 1q k21
p p 1 , 1q
pq2 , 1q
pp2 , 1q p q 2 , 1q t21
p p 2 , 1q
α1 α2
pp2 , 2q α1 α2
p p 2 , 2q
p p 1 , 2q pq2 , 2q
p p 1 , 2q pq2 , 2q t22
k22
p q 1 , 2q pq1 , 2q k32
p p 3 , 2q pp3 , 2q
Fig. 7. Synchronization step Fig. 8. The result of translating NP2
into a P/T net
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.
NP PN
Step 2 of the algorithm de nes a one-to-one correspondence between
reachable markings of nets and . It is easy to see that according to
translation de nition corresponding ring steps in both nets do not violate this
correspondence.
I.A. Lomazova and V. Ermakova: Verification of Nested Petri Nets 105
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 veri cation. The problem here is
that the size of the resulting P/T net can grows vastly. In the next section we de-
scribe the algorithm for direct unfolding of safe conservative NP-nets, presented
previously in [5], and then we compare these two approaches.
4 Unfoldings
4.1 Branching Processes of a Conservative NP-net
In this section, we de ne unfoldings of conservative NP-nets into occurrence
nets. We give an inductive de nition of a branching process of an NP-net, and
element-indexed C-Petri net
(similarly to [28]) de ne the unfolding as the maximal branching process.
First we introduce a concept of an , 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 (identi er). In
NP pSN, pE , . . . , E q, υ, λ, M q 0
SN pPSN, TSN, FSNq E pP , T , F q 0 i ¤ k
this section we suppose that 1 k is a conservative
NP-net, where , i Ei Ei Ei , .
De nition 3 (Element-indexed C -Petri nets). An C Θ
for some J is a C -net such that each place in Θ is marked
element-indexed -net
with an element of J . For our purposes, the set J will be the set of the identi ed
element-indexing set
net tokens.
Formally, for a xed net NP, a set of canonical names C is de ned as follows:
If x P p
P Y P q, η P N T ok Yt u, and X is a nite subset of C , then
SN
pX, x, η q P C ;
Ei Ei i
If x p T Y TSN q, and X is a nite subset of C , then pX, xq P C .
i
Ei Ei
Then an indexed C-net pP, T, F, M q is a P/T-net, such that
0
1. P Y T C ;
2. If p pX, x, ηq P P , then p X ;
3. If t pX, xq P P , then t X ;
4. pX, x, ηq P M i X H and x P p P Y PSNq.
0 Ei Ei
Just like for regular C -Petri nets, there exists a function h mapping the nodes
of an element-indexed C -Petri net to the nodes of NP :
#
hpxq
t if x pA, tq
if x pA, p, ηi q
(1)
p
The union of element-indexed C -Petri nets is de ned component-wise, exactly
as it was done for regular C -Petri nets.
We also de ne a notion of an adjacent place . According to De nition 2, for
every pair pp, tq P PSN TSN , where υppq ^ ppp, tq P FSN _ pt, pq P FSN q,
106 PNSE’16 – Petri Nets and Software Engineering
there exists a unique place p p q W pt, p1 q or
1 in a system net such that W p, t
p q p q
W p1 , t adjacent to p via t (denoted by
W t, p . Such a place p1 is said to be
xp|, ty). For example, in Fig. 4 the place adjacent to p2 via t1 is xp~
2 , t1 y p3 .
element-indexed branching processes
branching processes
Now we are ready to de ne a set of (or
NP
for short, when there is no ambiguity) for a given conserva-
tive NP-net .
De nition 4 (Element-indexed branching processes for conservative
nested Petri nets).
The set of for NP is the smallest set of
element-indexed C-nets satisfying the following rules:
element-indexed branching processes
1. Let
NTok, p P M u
C tpH, p, ηi q | p P PSN , ηi P M 0 ppqu Y tpH, p, ηi q | ηi P 0
æηi
be a set of places. The net Θ pC, 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
satis es 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
satis es 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 B be subsets of conditions of
Θ. If B and B satisfy the P osSync rule's premise (Fig. 9), then the net
E
obtained by adding an event e and conditions C to Θ is a branching process.
E
The SyncCond predicate is de ned below.
5. Let BS be a ( nite or in nite) set of branching processes. The union BS
is a branching process.
In rules (2)-(4), event e is called a possible extension of Θ.
TheSyncCond 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 Ji u active.
The places of net tokens corresponding to those in the pre-sets are contained in
BE .
I.A. Lomazova and V. Ermakova: Verification of Nested Petri Nets 107
P osEN :
B tpxi , bi , ηk q | i P I u
e pB, ttuq
copB q
and C
t P Tηk , λptq K
pPt pe, p, ηk q
t t bi | i P I u
P osSN :
B tpxi , bi , ηi q | i P I u
}
copB q t P TSN , λptq K t tbi | i P I u
e pB, ttuq and C tpe, xbi , ty, ηi q | i P I, ηi uY
tpe, b, q | b P t , υ pbq u
P osSync :
B tpxi , bi , ηi q | i P I u t P TSN , λptq K
}
copB Y BE q t t bi | i P I u SyncCondpBE , E, I, Θ, pB, tqq
e pB Y BE , ttu Y E q and C tpe, xbi , ty, ηi q | i P I, ηi uY
tpe, b, q | b P t , υ pbq uY
tpt1 , c1i , ηi q | i P I, ηi ,
c1i P Pηi , c1i P ti u
Fig. 9. Rules for possible extensions of a branching process
We say that the SyncCond BE , E, I, Θ, p pB, tqq predicate is true i the fol-
lowing conditions hold:
BE iPI tpyj , cj , ηi q | j P Ji , ηi pidi , EN NTok
1. i , µi q P , cj P PENi u ^
copBE q, i.e., BE is a set of reachable conditions that correspond to places in
EN , µ q P NToku
net tokens;
2. E tti P TENi | i P I, ηi pidi , i i , i.e., E is a subset of
transitions in each of the net tokens;
@ti P E,
λpti q λptq
E iPI tcj | j P Ji , ηi P NToku
3.
4.
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
NP
rings, respectively.
A possible branching process of 2 is shown in Fig. 10. In Fig. 10, a transi-
tion is labeled with t, if it is of the form p q
A, t , and a place is labeled with p, N p q
if it is of the form pA, p, N q.
108 PNSE’16 – Petri Nets and Software Engineering
k2 pq2 , N2 q tk3 u pq1 , N2 q tk2 u pq2 , N2 q tk3 u
pq2 , N2 q ...
t k3 u
pq2 , N2 q tk3 u pq1 , N2 q tk2 u pq2 , N2 q tk3 u
pq1 , N2 q ...
pp3 , N2 q tt2 u tt 2 u
p p2 , N 2 q ...
α p p3 , N 2 q
p p1 , N 1 q
p p2 , N 1 q
tk3 u t k2 u t k3 u
pq1 , N1 q ...
pq2 , N 1 q pq1 , N1 q pq2 , N1 q
tk3 u t k2 u t k3 u
k2 ...
pq2 , N 1 q pq1 , N1 q pq2 , N1 q
Fig. 10. Branching process of NP2
It was proven in [5] that every element-indexed branching process is an occur-
rence net and that the fundamental property of unfoldings holds for the de nition
of conservative NP-nets unfolding.
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 [5] that the branching process de nition for NP-nets is in accord with
the branching process de nition for low-level Petri nets., i.e. for a P/T-net N
the set of branching processes of N is isomorphic to the set of element-indexed
branching processes of N , when N is considered as an NP-net.
4.2 Comparing Two Ways of Nested Petri Net Unfolding
We have shown that each conservative safe NP-net can be converted into a be-
haviorally 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 subsec-
tion.
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 signi cant net growth. Thus e.g. for a system net
I.A. Lomazova and V. Ermakova: Verification of Nested Petri Nets 109
k2 pq2 , N2 q tk3 u pq1 , N2 q tk2 u pq2 , N2 q
pq2 , N2 q
t k3 u
pq2 , N2 q tk3 u pq1 , N2 q tk2 u pq2 , N2 q
pq1 , N2 q
pp3 , N2 q tt2 u
p p2 , N 2 q
α p p3 , N 2 q
p p1 , N 1 q
p p2 , N 1 q
tk3 u t k2 u
pq1 , N1 q
pq2 , N 1 q pq1 , N1 q pq2 , N1 q
tk3 u t k2 u
k2
pq2 , N 1 q pq1 , N1 q pq2 , N1 q
Fig. 11. Complete branching process of NP2
k2 pq2 , 2q t k32 u pq1 , 2q tk22 u pq2 , 2q t k32 u
pq2 , 2q ...
t k32 u
pq2 , 2q t k32 u pq1 , 2q tk22 u pq2 , 2q tk32 u
pq1 , 2q ...
p p 3 , 2q tt 2 u tt2 u
pp2 , 2q ...
α pp3 , 2q
pp1 , 1q
pp2 , 1q
t k31 u tk21 u t k31 u
pq1 , 1q ...
pq2 , 1q pq1 , 1q pq2 , 1q
t k31 u tk21 u t k31 u
k22 ...
pq2 , 1q pq1 , 1q pq2 , 1q
Fig. 12. Branching process of NP2 obtained via translation to a P/T net
transition t with n input places of the same type and k tokens of this type in the
n
initial marking we are to construct k 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
110 PNSE’16 – Petri Nets and Software Engineering
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 signi cant 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 signi cant 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
NP
with rather small models, which con rm our assumptions. Thus for our example
net 2 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 veri cation. Having the described above algorithm for NP-nets
unfoldings the basic algorithm (described in [26]) for constructing nite pre xes
of unfoldings of low-level P/T-nets can be modi ed in a straightforward way to
obtain an algorithm for constructing nite pre xes of unfoldings of conservative
NP-nets. In fact, the only part of the algorithm that needs to be modi ed is
the PotExt function, which has to be changed in accordance with the possible
cutting context
extension rules in Fig. 9. This is attainable because all the necessary de nitions
(in particular, the de nition of a ) and the theory of canonical
pre xes [25],[26] can be directly extended to cover NP-nets.
NP
For example, let's consider the result of the standard algorithm applied to the
NP-net 2 from Fig. 4 using the McMillan's cutting context (in the notation
of [26], C
1 C 2 ðñ M arkpC 1 q M arkpC 2 q and C 1 C 2 ðñ |C 1 | |C 2 |).
We have shown a canonical pre x for NP 2 in Fig. 11. This canonical pre x
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 , k1 u, 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 Conclusion
In this paper we've proposed and compared two ways of unfolding for safe con-
servative 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
I.A. Lomazova and V. Ermakova: Verification of Nested Petri Nets 111
described in the literature. The second method is a direct unfolding, proposed
and justi ed earlier in [5].
For that we've developed and justi ed 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 advan-
tage 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 bene ts of direct unfolding.
For further work, we plan to enlarge the complexity of nets and number of
experiments.
References
1. Lomazova, I.A.: Nested Petri netsa formalism for speci cation and veri cation of
multi-agent distributed systems. Fundamenta Informaticae 43(1) (2000) 195214
2. Valk, R.: Object petri nets. In: Lectures on Concurrency and Petri Nets. Springer
(2004) 819848
3. McMillan, K.L.: Using unfoldings to avoid the state explosion problem in the
veri cation of asynchronous circuits. In: Computer Aided Veri cation, Springer
(1992) 164177
4. Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains,
part i. Theoretical Computer Science 13(1) (1981) 85108
5. Frumin, D., Lomazova, I.A.: Branching processes of conservative nested Petri nets.
In: VPT@ CAV. (2014) 1935
6. Lomazova, I.A., van Hee, K.M., Oanea, O., Serebrenik, A., Sidorova, N., Voorhoeve,
M.: Nested nets for adaptive systems. Application and Theory of Petri Nets and
Other Models of Concurrency, LNCS (2006) 241260
7. Lomazova, I.A.: Modeling dynamic objects in distributed systems with nested petri
nets. Fundamenta Informaticae 51(1-2) (2002) 121133
8. Lomazova, I.A.: Nested petri nets for adaptive process modeling. In: Pillars of
computer science. Springer (2008) 460474
9. López-Mellado, E., Villanueva-Paredes, N., Almeyda-Canepa, H.: Modelling of
batch production systems using Petri nets with dynamic tokens. Mathematics and
Computers in Simulation 67(6) (2005) 541558
10. Kahloul, L., Djouani, K., Chaoui, A.: Formal study of recon gurable manufacturing
systems: A high level Petri nets based approach. In: Industrial Applications of
Holonic and Multi-Agent Systems. Springer (2013) 106117
11. Zhang, L., Rodrigues, B.: Nested coloured timed Petri nets for production con-
guration of product families. International journal of production research 48(6)
(2010) 18051833
12. Venero, M.L.F., da Silva, F.S.C.: Modeling and simulating interaction protocols
using nested Petri nets. In: Software Engineering and Formal Methods. Springer
(2013) 135150
13. Chang, L., He, X., Lian, J., Shatz, S.: Applying a nested Petri net modeling
paradigm to coordination of sensor networks with mobile agents. In: Proc. of
Workshop on Petri Nets and Distributed Systems, Xian, China. (2008) 132145
14. Cristini, F., Tessier, C.: Nets-within-nets to model innovative space system archi-
tectures. In: Application and Theory of Petri Nets. Springer (2012) 348367
112 PNSE’16 – Petri Nets and Software Engineering
15. Mascheroni, M., Farina, F.: Nets-within-nets paradigm and grid computing. In:
Transactions on Petri Nets and Other Models of Concurrency V. Springer (2012)
201220
16. Dworza«ski, L.W., Lomazova, I.A.: On compositionality of boundedness and live-
ness for nested Petri nets. Fundamenta Informaticae 120(3-4) (2012) 275293
17. Dworza«ski, L., Lomazova, I.A.: Cpn tools-assisted simulation and veri cation of
nested petri nets. Automatic Control and Computer Sciences 47(7) (2013) 393402
18. Venero, M.L.F.: Verifying cross-organizational work ows over multi-agent based
environments. In: Enterprise and Organizational Modeling and Simulation.
Springer (2014) 3858
19. Winskel, G.: Event structures. Springer (1986)
20. Bonet, B., Haslum, P., Hickmott, S., Thiébaux, S.: Directed unfolding of petri
nets. In: Transactions on Petri Nets and Other Models of Concurrency I. Springer
(2008) 172198
21. McMillan, K.L.: A technique of state space search based on unfolding. Form.
Methods Syst. Des. 6(1) (1995) 4565
22. Heljanko, K.: Using logic programs with stable model semantics to solve deadlock
and reachability problems for 1-safe petri nets. Fundamenta Informaticae 37(3)
(1999) 247268
23. Khomenko, V., Koutny, M.: Branching processes of high-level Petri nets. In Gar-
avel, H., Hatcli, J., eds.: Tools and Algorithms for the Construction and Analysis
of Systems. Volume 2619 of Lecture Notes in Computer Science. Springer (2003)
458472
24. Langerak, R., Brinksma, E.: A complete nite pre x for process algebra. In:
Computer Aided Veri cation, Springer (1999) 184195
25. Khomenko, V., Koutny, M., Vogler, W.: Canonical pre xes of Petri net unfoldings.
Acta Informatica 40(2) (2003) 95118
26. Khomenko, V.: Model Checking Based on Pre xes of Petri Net Unfoldings. Ph.D.
Thesis, School of Computing Science, Newcastle University (2003)
27. Esparza, J., Heljanko, K.: Unfoldings: a partial-order approach to model checking.
Springer (2008)
28. Engelfriet, J.: Branching processes of Petri nets. Acta Informatica 28(6) (1991)
575591
29. Baldan, P., Corradini, A., König, B., Schwoon, S.: Mcmillan's complete pre x for
contextual nets. In Jensen, K., Aalst, W.M., Billington, J., eds.: Transactions on
Petri Nets and Other Models of Concurrency I. Volume 5100 of Lecture Notes in
Computer Science. Springer (2008) 199220
30. Fleischhack, H., Stehno, C.: Computing a nite pre x of a time Petri net. In
Esparza, J., Lakos, C., eds.: Application and Theory of Petri Nets 2002. Volume
2360 of Lecture Notes in Computer Science. Springer (2002) 163181
31. Mascheroni, M.: Hypernets: a Class of Hierarchical Petri Nets. Ph.D. Thesis, Facolt
di Scienze Naturali Fisiche e Naturali, Dipartimento di Informatica Sistemistica e
Comunicazione, Università Degli Studi Di Milano Bicocca (2010)
32. Jensen, K., Kristensen, L.M.: Coloured Petri nets: modelling and validation of
concurrent systems. Springer (2009)
33. Dworza«ski, L.W., Lomazova, I.A.: On compositionality of boundedness and live-
ness for nested Petri nets. Fundamenta Informaticae 120(3) (2012) 275293