This paper presents a compositional conformance checking approach between nested Petri nets and event logs of multi-agent systems. By projecting an event log onto model components, one can perform conformance checking between each projected log and the corresponding component. We formally demonstrate the validity of our approach proving that, to check fitness of a nested Petri net is equivalent to check fitness of each of its components. Leveraging the multi-agent system structure of nested Petri nets, this approach may provide specific conformance diagnostics for each system component as well as to avoid to compute artificial boundaries when decomposing a model for conformance checking.
Lift, thrust, drag, and gravity are the four forces helping an airplane fly. Process mining has similarly four forces to measure its quality namely fitness, generalization, precision, and simplicity [1]. Conformance checking, which is one of the three pillars of process mining, is actually the fitness force 2[]. It allows to check how well modeled behavior conforms reality as recorded in an event log. Conformance checking has become relevant in areas such as business alignment [3], auditing [4], and financial software testing [ 5]. However, current conformance checking approaches fall short when analyzing large event logs of complex multi-agent systems. These systems are characterized by a large number of agents interacting, and exhibiting a high degree of concurrency. In this light, it makes sense to use compositional approaches, where a conformance problem can be decomposed into smaller problems (e6.,g7., [8]). In [6], the author formalizes the so-callveadlid decomposition to decompose conformance problems. This decomposition approach represents no problem from a conformance point of view7.]I,nth[e authors proposed to decompose models using the ideasionfgle-entry and single-exit (SESE).
A SESE component is a subnet that has a simple interface w.r.t the rest of the net. Another approach is presented in8][ to compute the overall conformance of a model by merging previously decomposed fragments.
Nevertheless, these approaches use process models whose structure may not provide a clear distinction between system components and their boundaries. This leads these approaches to increase their complexity to compute such boundaries (e.g., where to decompose a model, how many components, etc). Moreover, it may happen that the decompositionairstificial , i.e., fragments of a decomposed model do not represent a real division of a system, so diagnostics for each real component may not be provided. In this sense, we propose the use of models of multi-agent systems. In particular, we consider nested Petri nets (NP-ne9t]s)—[ an extension of Petri nets, where tokens can be Petri nets themselves, allowing to model multi-agent systems. NP-nets have been already used in the broader context of process modeling and workflow management [10, 11].
Fig. 1 depicts an example of a NP-net describing aanutomated assistant engine that can serve multiple customers concurrently. A NP-net consists osfyastem net, i.e., modeling the system’s environment, and a set ofnet tokens, denoting interacting agents. Each net token has an inner
In this paper, we present a compositional conformance checking approach between nested Petri nets and event logs of multi-agent systems. Given an event log of a multi-agent system, we decompose it into severaplrojections according to the model components. Then, a conformance checking technique (e.g., replay, alignment) can be performed separately between each projection and the corresponding model component (an agent or the system net). We assume that each agent in the event log corresponds to a net token in the nested Petri net model. For this task, we provide clear definitions regarding a subclass of nested Petri nets and event logs of multi-agent systems. To demonstrate the validity of our approach, we consider the notiofitnneosfs . If a model hasperfect fitness, then all log traces can be replayed on the model from beginning to end. In this work, we map such notion of an event log thpaetrfectly fits a model, by defining how an event log of a multi-agent system fits a nested Petri net. Consequently, as an important result of this paper, we state and prove the following theorem: an event log of a multi-agent system perfectly fits a nested Petri net if and only if the event log is syntactically correct w.r.t to the nested Petri net and each projection perfectly fits the corresponding model component.
The remainder of this paper is structured as follows. In section 2, we describe nested Petri nets. In section 3, we define the structure for event logs of multi-agent systems. In section 4, we present the compositional conformance checking approach of nested Petri nets and event logs of multi-agent systems, including the aforementioned theorem and its proof. Finally, section 5 presents some conclusions and future work.
ℕ denotes the set of natural numbers (including zero). Lebte a set. The set of all subsets ofis called apower set, denoted as () , e.g., the power set of = {, } is () = {{, }, {}, {}, ∅} . A over is a mapping ∶ → ℕ . In other words, a multiset is a collection of elements, each of them with certain multiplicity, e.g{.,,, }, {, , }, and ∅ are multisets ove r. For compactness, we write{ 3, 2} for {, , , , } . ℙ () denotes the set of all multisets ov e r. = ⟨ 1, 2, ..., ⟩ ∈ ∗ denotes asequence of length over a set .
Definition 1 (Petri net). A Petri net is a triple = (, , ) , where is the set of places, is the set of transitions, ∩ = ∅ , and ⊆ ( × ) ∪ ( × ) is the set of directed arcs (flow relation). Petri nets [12] is a formalism for modeling and analyzing concurrent distributed systems. As defined above, a Petri net consists of and , which correspond respectively to and of a system. Places may contain tokens, representing resources, control threads, etc. A ∶ → ℕ is a function that assigns tokens to places, denoting a system’s state. The initial marking is denoted a s 0, and the change into a new marking is defined by the firing rule . Let = (, , ) be a Petri net, = ∪ , the sets • = { ∈ |(, ) ∈ } and • = { ∈ |(, ) ∈ } denote thepreset and thepostset of ∈ . Transition ∈ is enabled in a marking if • ⊆ . Then, the firing of leads to anew marking ′ = − • + •. Definition 2 (Workflow net). Let = (, , ) be a Petri net. is a workflow net (WF-net) if P contains a source place and a sink place s.t. • = • = ∅, and each node in is on a path from to .
WF-net has an initial and a final state, represented by markin gs0 = {} and = {} . Let = (, , ) be a WF-net, we consider anactivity labeling function ∶ → , which assigns an activity label to each transiti on∈ , where is a finite set of activities. We define a sequence = ⟨ 1, ..., ⟩ ∈ ∗ as a of a WF-net if there exists a firing sequence⟨ 1, ..., ⟩ that leads from the initial marking 0 = {} of to its final marking = {} s.t. ( ) = (1 ≤ ≤ ) . The set of all possible runs of a WF-n etis denoted byℬ( ) and is called thbeehavior of .
For modeling complex systems, one can use colored Petri nets (CP-nets). In CP-nets, tokens are attached with values belonging to diferent domaincsol(or types). Let be the set of these diferent domains. Then, each place in a CP-net is typed with a domain in indicating the type of tokens it contains. Arcs in CP-nets are annotated with expressions from a language defined over = ∪ , where and are sets of variables and constants. is defined as follows:() An ∈ is an expression in , () if 1, 2 ∈ , then ( 1 + 2) is an expression in .
Definition 3 (Colored Petri net). A colored Petri net is a tuple = (, , , type, ) where: • (, , )
is a Petri net; • type ∶ →
is a place-typing function, mapping each place to a type in ; • ∶ → the type of () is an arc expression function. ∀ ∈ , if is adjacent to a place ∈ , then corresponds to the type of .
Let = (, , , type, ) be a CP-net over a set of domains . A marking in CPN is a function that maps each plac e∈ into a multiset of token s() ∈ ℙ (type()) . For a CPN, we distinguish an initial markin g 0 and a set of final markingsΩ. A binding of a transitio n is a function that assigns a val u(e) to each variabl eoccurring in the expression of an arc adjacent to . For each variab le, () ∈ ⋃∈ . A pair(, ) , where is a binding of , is called a binding element. An evaluatio n(, )() determines token demands (multiset of tokens) on for to be enabled with the binding, and the multiset of tokens that the transitio nremoves from the place when occurs with the bindin g. (, )() determines the multiset of tokens added to an output pla ce. A transition is enabled in a marki ng w.r.t a binding if for all ∈ , (, )() ⊆ () . An enabled transition fires in a marking yielding a new marking ′, such that for all place,s ′() = (() ⧵ (, )()) ∪ (, )() .
In the following we consider a subclass of nested Petri nets (NP-nets). A NP- netconsists of a colored Petri net called tshyestem net , and a set of WF-nets = { 1, ..., } called element nets, which define types of net tokens. In a system net , places contain either a set of net tokens or a multiset ofatomic colored tokens. A net token is a marked element net, whereas an atomic colored token is a data value of some do m∈ai n , where is a finite set of domains. Regarding the system net, we consider a language of expressions defined over = ∪ , where: (i) is a finite set of variables, typed over the set of element nets and data domain s (e.g., the type of ∈ is 1) and (ii) is a finite set of constants, typed only over the set of data domai ns. Each arc is supplied with an arc expression fro m .
is a place adjacent to arcontaining net tokens, or an arbitrary sum of distinct variables and constants typed ove r if type() ∈ where is a place adjacent to arcontaining atomic colored tokens.
Definition 4 (Nested Petri net). Let be a finite set of domains, — a finite set of synchronization labels and — a finite set of activities. A nested Petri net (NP-net) is a tuple = ( , ( 1, ..., ), , ) , where: • = ( ,
, , type, ) is a colored Petri net (called a system net) with two sets of places and for all ∈ and (
∪ , type() ∈ ;
= ), such that for all ∈ , type() ⊆ { 1, ..., } • = • ∶ • ∶ 1, , = ( , , ) is a WF-net, called an element net, s.t. ( ∪ ) ∩ ( ∪ ) = ∅; ↛ is a (partial) synchronization labeling function, where = ∪ 1 ∪...∪ ; → is an activity labeling function, s.t. = 1, ∩ = ∅. in
′ transition fires in a marking () = (() ⧵ (, )()) ∪ (, )()
In what follows, we considecronservative NP-nets [14]. In a conservative NP-net = ( , (
1, ..., ), , ) , net tokens cannot becloned ordisappear. In a run, there is astable set of net tokens which we distinguish using individuaalgent names. Let be a set of agent names, we propose a functionclass ∶ → { 1, ..., }, which maps to each agent name an element net. We denote by(, )
a net token which is characterized by an individual agent namweith the corresponding element nectlass() and a marking . The set of all possible net tokens is denoted by agent .
A marking in a NP-net is a function mapping each plac e∈ to a subset of agent or a multiset over a domain∈ , in accordance with the type of. Hence, elements in() are either distinguishable net tokens or atomic colored tokens which can be repeated. We say that a net token(, ) resides in a plac e (under marking ) if (, ) ∈ () . Thus, the marking of a NP-net is defined by the marking of its system net. For a NP-net, we distinguish an initial marking 0 and a set of final markings ∈ Ω.
Let be a transition in the system net the sets of pre- and post-elements of transiti o.n () = { ( of a NP-net, and let be• = { 1, ..., } and • = { 1, ..., } 1, ), ..., ( , ), (, 1), (, )} denotes the set of all arc expressions adjacen t. tAo binding of is a function assigning to each variabl e , occurring in each expression i(n)
, a value() ∈ is enabled in a marking w.r.t a binding if for all∈ ⋃∈ • (, )() ⊆ () ∪ agent . A transition
. An enabled yielding a new markin g ′, such that for all place∈s ,
. For net tokens from agent serving as variable values in input arc expressions fro m() , we say that they areinvolved in the firing of . They are removed from input places and brought to output places. of
Element-autonomous step: let be a transition without a synchronization label in a net token named , i.e., ()
is not defined. When is enabled in a marking , an element-autonomous step is a firing of in marking , producing a new marking ′, according to the usual firing rules of
be a transition without a synchronization label in the system net . A system-autonomous step (also calledtaransfer step when net tokens are involved) is the ifring of transition according to the firing rule described above for a NP-net. The occurrence of this step in a marking
w.r.t a binding , producing a new marking ′, is denoted by: Synchronization step: let ∈ be a transition with a synchronization lab()el , and enabled in
w.r.t a binding , and let( 1, 1), ..., ( , ) ∈ agent be net tokens involved in the ifring of . Then, can fire provided that in each( , ) (1 ≤ ≤ ) there is an enabled transition labeled with the same valu(e) . Thus, asynchronization step goes in two stages: first, the firing of transitions 1, ..., in all net tokens involved in the firing o f, and then, the firing of in w.r.t. a binding . This step is denoted by: net and — a sequence of steps in . The occurence of from the initial marking 0 of , results in some final marking ∈ Ω, is called a run. The set of all possible runs is denoted by ℬ( )
and is called the behavior of .
Events consist of anactivity name, resources which executed the activity or werinevolved in its execution, and an (optional) multiset of data values. As possible resources we consider a system
or a finite set of agents with distinct names 1, 2, ..., . As shown in table1, we consider
three event types: (
where resources (agents) are involved, or (3) the simultaneous execution of activity by , and activitie s 1, ..., by resource s1, ..., . For cases (2) and (3), events may contain data values used by . We proceed to formally define a trace and an event log of a multi-agent system. ( × { } × ( × of traces.
Definition 6 (Trace, Event log of a multi-agent system).
Let be a system name, — a set of system activities, — a set of data, — a set of agent activities, — a set agent names, and — a set where ∈ ⇔ = ∈ (ℰ agent ∪ ℰsystem ∪ ℰsync ) ∗ where ℰagent = × , ℰsystem = ( × { } × ) , and ℰsync = 1 ∪ 2 / 1 ⊆ and 2 ∈ ℙ () . A trace is a sequence ) × ℙ ()) . ℒ ∈ ℙ (ℰagent , ℰsystem , ℰsync )∗ is an event log, i.e., a multiset
information on nine traces. A distinct trace can occur multiple times. For instance, t5race An event log of a multi-agent system ℒ in tabular form, whose expected behavior is modeled in fig. 1. 1 = ⟨ (, 1), (, 2), (ℎ, 1), (ℎ, 2), (, , {( ,
1)}), (, , {( , Trace (, , { (, , { occurred two times. It is a sequence of seven events. First, both activitieasnd were executed by agents 1 and 2. Next, the system
executed two synchronization steps with agent1s and 2, where activitie s and , and late r and , were executed simultaneously. The trace ended by a system-autonomous step where
executed for agent 1.
Let ℒ be an event log of a multi-agent system an d — a nested Petri net.ℒ is syntactically correct w.r.t. if each event inℒ is syntactically correct w.r.t. a step in where: • An event (, ) is syntactically correct w.r.t. a step in if there is a transitionwithout synchronization label in a net token namedwhere() = , and can fire in a marking producing a new markin g ′, i.e., where ∈ , 1 ≤ ≤ , and c l a s s ( ) = . • An event (, , ∈
1, ..., ) is syntactically correct w.r.t. a step in if there is a transition without synchronization label wher()e = , and can fire in a marking w.r.t.
a binding such that assigns the atomic tokens 1, ..., to the variables i n() , i.e., • An event (, , {(
1, 1), ..., ( , )}, { 1, ..., }) is syntactically correct w.r.t. a step in if there is a transitio n ∈ with synchronization labe(l) where () = , ( 1, 1), ..., ( , ) are net tokens involved in the firing of such that in each( , ) there is an enabled transitio n(( ) = ) labeled with the same valu(e) , and can fire in
w.r.t. a binding assigning the atomic tokens 1, ..., and also the agent names 1, ..., to the variables i n() , i.e.,
), ),1≤≤}, −−−−−−−−−−−−−−−−−→ ′ in . 4. Compositional Conformance Checking of Nested Petri Nets and Event Logs of Multi-Agent Systems In this section, we propose a solution to check conformance of event logs of multi-agent systems and nested Petri nets. We prove that an event log perfectly fits a NP-net if the event log is syntactically correct w.r.t. that NP-net, and each projection of the event log onto a NP-net component perfectly fits that component.
Let ⟨⟩ denote an empty sequence, 1. 2 — concatenation of two sequences, an↾d — the of sequence on an element .
Definition 7 (Trace projection onto an agent). Let = (ℰ agent ∪ ℰsystem ∪ ℰsync ) be a set
of events, — a set of agent activities, and — a set of agent names. ↾∈ ∈ ∗ ⟶ ∗ is a
projection function defined recursively: (
Definition 8 (Trace projection onto a system net). Let = (ℰ agent ∪ ℰsystem ∪ ℰsync ) and
⊆ × where is a set of system activities, ∈ ⇔ = 1 ∪ 2/ 1 ⊆ and 2 ∈ ℙ () ,
is a set of agent names, and is a set of data. ↾ ∈ ∗ ⟶ ∗ is a projection function defined
recursively: (
Def. 7 (resp. Def. 8) is used to project traces of an event log onto net tokens (resp. a system net). A projection of a trace onto a net token yields the sequence of agent activities. A projection onto the system net yields a sequence of pairs where each pair consists of an activity and the set of resources and data involved in this activity execution. For instance, consider the projection of the event logℒ (cf. Table2) onto components of the NP-net (cf. Fig. 1). Table3 shows the three decomposed event logs , 1, and 2 resulting from the projection oℒf onto (a) the system net, (b) agent 1, and (c) agent 2 respectively.
Thus, a conformance checking technique can be applied to each projection and the corresponding
NP-net component, ignoring their synchronization labels. In particular, for the system net,
we replace net tokens by their agent names, which are atomic colored tokens. We consider
synchronization steps as autonomous steps, and for a mark ingin a NP-net , marking
projections onto components are defined as follows: (
Definition 9 (Perfectly fitting event log). Let ℒ be an event log of a multi-agent system and — a nested Petri net. ℒ perfectly fits if and only if for all = ⟨ 1, ..., ⟩ ∈ ℒ there is a run ′ = ⟨ 1, ..., ⟩ ∈ ℬ( ) such that for = 1, , is syntactically correct w.r.t .
Let be a nested Petri netℒ, — an event log,( 1, 1), ..., ( , ) — net tokens of , 1, ..., –- corresponding projections oℒf, and –- a projection ofℒ onto actions of the system net. perfectly fits if and only if for al=l ⟨ 1, ..., ⟩ ∈ , there is a ru n ′ in the system net component where
( 1), 1 ( 2), 2 ( ), ′ = ( 0 −−−−−→ 1 −−−−−→ 2... −1 −−−−−−→ ) and for = 1, , = ( , { 1, ..., }), ( ) = , and is the binding assigns{ 1, ..., } to the variables i n( ). For = 1, , perfectly fits ( , ) if and only if for all= ⟨ 1, ..., ⟩ ∈ , there is a ru n ′ in the element netclass( ) where
( 1) ( 2) ( ) ′ = ( 0 −−−−→ 1 −−−−→ 2... −1 −−−−→ ) and for = 1, , = and( ) = .
An event log perfectly fits a model if all traces in the log can be replayed on the model from beginning to end. For instance, let us consider the event lℒog(cf. Table2) and the NP-net depicted in fig. 1. Clearlyℒ, perfectly fits . Also, each projected event l o g , 1, or 2 (cf.
Theorem 1. Given a nested Petri net = ( , ( 1, ..., ), , ) and an event log ℒ ∈ ℙ (ℰagent , ℰsystem , ℰsync )∗, let ( 1, 1), ..., ( , ) be net tokens of , 1, ..., – corresponding projections of ℒ, and – a projection of ℒ onto the system net . ℒ perfectly ifts if and only if: 1. ℒ is syntactically correct w.r.t ; 2. perfectly fits ; 3. perfectly fits ( , ), 1 ⩽ ⩽ .
Proof. Let ℒ be an event log of a multi-agent system , = ( , ( 1, ..., ), , ) Petri net, and( 1, 1), ..., ( , ) — net tokens of .
(⇒) Let = ⟨ 1, ..., ⟩ ∈ ℒ be such that there is a run ′ = ⟨ 1, ..., ⟩ ∈ ℬ( )
= 1, :
— a nested
and for
• if = (, ) , then = −−−−→ ′ where ∈ , 1 ≤ ≤ , class( ) = , and() = . (
i.e., perfectly fits . We need to prove that • is syntactically correct w.r.t ; system net component where:
• ↾ = ⟨ 1, ..., ′⟩ perfectly fits the system net component, i.e., there is a run in the = ( 0 −−−−−→ 1 −−−−−→ 2... ′−1 −−−−−−−→ ) ( 1), 1 ( 2), 2
( ′), ′ }), ( ) = , and is the binding that assigns{ 1, ..., } • if = (, ,
1, ..., ), then = the atomic tokens 1, ..., to the variables in() . (2) • if = (, , {(
1, 1), ..., ( , )}, { 1, ..., }), then = () = ,
, ( ) = , 1 ≤ ≤ , and is a binding assigning the atomic tokens1, ..., and also the agent name s1, ..., to the variables in() . (3)
″⟩ perfectly fits ( , ), i.e., there is a ru n in the element net = ( 0 −−−−→ 1 −−−−→ 2... −1 −−−−−→ )
(cf. Def. 9).
Taking into account that ′ = ⟨ 1, ..., ⟩ is a run in (which can hold synchronization
labels) where fo r= 1, we have (
⟨⟩, ⟨ ⟩ ↾ = ⎪ ⟨(, { 1, ..., })⟩, ⎨ ⟨(, { 1, ..., , 1, ..., })⟩, = (, , {(
= (, ) = (, , 1, ..., ) 1, 1), ...,
(4) ( , )}, { 1, ..., })
′⟩, there is a ru n in the system net component = ( 0 −−−−−→ 1 −−−−−→ 2... ′−1 −−−−−−−→ ) ( 1), 1 ( 2), 2 ( ′), ′ and for = 1, ′, = ( , { 1, ...,
the variables i n( ). Therefore, ↾
perfectly fits the system net component. }), ( ) = , and is the binding that assigns{ 1, ..., } to Now by the fact that ′ is a run in
(which can hold synchronization labels) where for
= 1, we have (
⟨⟩, ⎪ ⎩ ⟨⟩, ⎧⎪ ⟨ ⟩, 1 ≤ ≤ , = (, )
= (, , {( ℎ (cf. Def. 7) it follows that for↾ = ⟨ 1, ..., ″⟩, 1 ≤ ≤ , there is a ru n in the element net = ( 0 −−−−→ 1 −−−−→ 2... −1 −−−−−→ ) and for = 1, ″, ( ) = . Therefore, ↾ perfectly fits ( , ).
(⇐) Let = ⟨ 1, ..., ⟩ ∈ ℒ be such that is syntactically correct w.r.t , ↾ perfectly fits the system net component, and for = 1, , ↾ perfectly fits ( , ). We need to prove that
Taking into account (4) and (5), and th atis syntactically correct w.r.t , we deduce that by associating to each element of the projected sequences the corresponding resource, elements the proof. can be merged together into the tra ce. Therefore, being ↾ component and for = 1, ↾ perfectly fits ( , ), then perfectly fits perfectly fits the system net and this concludes
In this paper, we proposed a compositional approach for conformance checking of nested Petri nets and event logs of multi-agent systems. Nested Petri nets are a well-known Petri net extension where tokens can be Petri nets themselves, allowing to model multi-agent systems. An event log can be projected onto NP-net components (system net and all agents), so conformance checking can be performed between each projection and the corresponding component. This approach can provide specific conformance diagnostics for each system component. We demonstrated the validity of our approach proving that, an event log perfectly fits a nested Petri net if and only if it is syntactically correct w.r.t the model and each projection perfectly fits the corresponding model component. For future research, we consider the experimental evaluation of our approach against other approaches when checking conformance of multi-agent systems.
This work is supported by the Basic Research Program at the National Research University [2] J. Carmona, B. van Dongen, A. Solti, M. Weidlich, Conformance Checking: Relating
Processes and Models, Springer, 2018. [3] W. van der Aalst, Business alignment: using process mining as a tool for delta analysis and conformance testing, Requirements Engineering 10 (2005) 198–211. [4] W. van der Aalst, K. M. van Hee, J. M. van der Werf, M. Verdonk, Auditing 2.0: Using process mining to support tomorrow’s auditor, Computer 43 (2010) 90–93. [5] I. Itkin, Mind the gap between testing and production: applying process mining to test the resilience of exchange platforms (2019h)t,tps://tinyurl.com/y55sndc,v???? [6] W. van der Aalst, Decomposing petri nets for process mining : a generic approach,
Distributed and Parallel Databases 31 (2013) 471–507. [7] J. Munoz-Gama, J. Carmona, W. Van Der Aalst, Single-entry single-exit decomposed conformance checking, Information Systems 46 (2014) 102–122. [8] W. Lee, H. Verbeek, J. Munoz-Gama, W. van der Aalst, M. Sepúlveda, Recomposing conformance: Closing the circle on decomposed alignment-based conformance checking in process mining, Information Sciences 466 (2018) 55–91. [9] I. A. Lomazova, Nested Petri Nets - a Formalism for Specification and Verification of
Multi-Agent Distributed Systems., Fundamenta Informaticae 43 (2000) 195–214. [10] K. Hee, van, O. Oanea, A. Serebrenik, N. Sidorova, M. Voorhoeve, I. Lomazova, Checking properties of adaptive workflow nets, Fundamenta Informaticae 79 (2007) 347–362. [11] I. A. Lomazova, Nested Petri Nets for Adaptive Process Modeling, volume 4800, Springer, 2008, pp. 460–474. [12] T. Murata, Petri nets: Properties, analysis and applications, Proceedings of the IEEE 77 (1989) 541–580. [13] W. van der Aalst, The Application of Petri Nets to Workflow Management, Journal of
[14] I. A. Lomazova, V. O. Ermakova, Verification of Nested Petri Nets Using an Unfolding Approach, in: L. Cabac, L. M. Kristensen, H. Rölke (Eds.), Petri Nets and Software Engineering, volume 1591 ofCEUR Workshop Proceedings, 2016.