=Paper= {{Paper |id=Vol-2795/paper4 |storemode=property |title=Compositional Conformance Checking of Nested Petri Nets and Event Logs of Multi-Agent Systems |pdfUrl=https://ceur-ws.org/Vol-2795/paper4.pdf |volume=Vol-2795 |authors=Khalil Mecheraoui,Julio C. Carrasquel,Irina A. Lomazova }} ==Compositional Conformance Checking of Nested Petri Nets and Event Logs of Multi-Agent Systems== https://ceur-ws.org/Vol-2795/paper4.pdf 
Compositional Conformance Checking of Nested
Petri Nets and Event Logs of Multi-Agent Systems
Khalil Mecheraouia,b , Julio C. Carrasquela and Irina A. Lomazovaa
a
    National Research University Higher School of Economics, Myasnitskaya ul. 20, Moscow, 101000, Russia
b
    University of Constantine 2 β€” Abdelhamid Mehri, Nouvelle ville Ali Mendjeli BP : 67A, Constantine, 25000, Algeria


                                         Abstract
                                         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.

                                         Keywords
                                         Process mining, conformance checking, Petri nets, nested Petri nets, multi-agent systems, fitness




1. Introduction
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 (e.g. [6, 7, 8]). In [6], the
author formalizes the so-called valid decomposition to decompose conformance problems. This
decomposition approach represents no problem from a conformance point of view. In [7], the
authors proposed to decompose models using the idea of single-entry and single-exit (SESE).

MACSPro’2020: Modeling and Analysis of Complex Systems and Processes, October 22-24, 2020, Venice, Italy & Moscow,
Russia
email: k_mecheraoui@esi.dz (K. Mecheraoui); jcarrasquel@hse.ru (J.C. Carrasquel); ilomazova@hse.ru (I.A.
Lomazova)
url: https://www.hse.ru/en/staff/jcarrasquel (J.C. Carrasquel); https://www.hse.ru/en/staff/ilomazova (I.A.
Lomazova)
orcid: 0000-0001-9906-6074 (K. Mecheraoui); 0000-0003-3557-797X (J.C. Carrasquel); 0000-0002-9420-3751 (I.A.
Lomazova)
                                       Β© 2020 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
    CEUR
    Workshop
    Proceedings
                  http://ceur-ws.org
                  ISSN 1613-0073
                                       CEUR Workshop Proceedings (CEUR-WS.org)
Figure 1: A nested Petri net where the system net 𝑆𝑁 models an automated assistant engine, serving
customers concurrently (in this case, agents π‘Ÿ1 and π‘Ÿ2 ).


A SESE component is a subnet that has a simple interface w.r.t the rest of the net. Another
approach is presented in [8] 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 decomposition is artificial, 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-nets) [9] β€” 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 an automated assistant engine that can serve
multiple customers concurrently. A NP-net consists of a system net, i.e., modeling the system’s
environment, and a set of net tokens, denoting interacting agents. Each net token has an inner
Petri net structure describing agent behavior.
   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 several projections 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 notion of fitness. If a
model has perfect 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 that perfectly 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.
This theorem justifies the validity of our compositional approach.
   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.


2. Nested Petri Nets
β„• denotes the set of natural numbers (including zero). Let 𝑆 be a set. The set of all subsets of 𝑆 is
called a power 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 over 𝑆. For
compactness, we write {π‘Ž3 , 𝑏 2 } for {π‘Ž, π‘Ž, π‘Ž, 𝑏, 𝑏}. β„™π‘š (𝑆) denotes the set of all multisets over 𝑆.
𝜎 = βŸ¨π‘Ž1 , π‘Ž2 , ..., π‘Žπ‘› ⟩ ∈ 𝑆 βˆ— denotes a sequence 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 as π‘š0 , and the change into a new marking is defined
by the firing rule. Let 𝑁 = (𝑃, 𝑇 , 𝐹 ) be a Petri net, 𝑋 = 𝑃 βˆͺ 𝑇, the sets β€’ π‘₯ = {𝑦 ∈ 𝑋 |(𝑦, π‘₯) ∈ 𝐹 } and
π‘₯ β€’ = {𝑦 ∈ 𝑋 |(π‘₯, 𝑦) ∈ 𝐹 } denote the preset and the postset of π‘₯ ∈ 𝑋. Transition 𝑑 ∈ 𝑇 is enabled in
                                                                               β€²
a marking π‘š iff β€’ 𝑑 βŠ† π‘š. Then, the firing of 𝑑 leads to a new marking π‘š = π‘š βˆ’ β€’ 𝑑 + 𝑑 β€’ .

Definition 2 (Workflow net). Let 𝑁 = (𝑃, 𝑇 , 𝐹 ) be a Petri net. 𝑁 is a workflow net (WF-net) iff
P contains a source place 𝑖 and a sink place π‘œ s.t. β€’ 𝑖 = π‘œ β€’ = βˆ…, and each node in 𝑁is on a path from 𝑖
to π‘œ.

When modeling individual agents in multi-agent systems, we consider workflow nets [13]. A
WF-net has an initial and a final state, represented by markings π‘š0 = {𝑖} and π‘šπ‘“ = {π‘œ}. Let
𝑁 = (𝑃, 𝑇 , 𝐹 ) be a WF-net, we consider an activity labeling function 𝛿 ∢ 𝑇 β†’ 𝐴, which assigns
an activity label to each transition 𝑑 ∈ 𝑇, 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-net 𝑁 is denoted by ℬ(𝑁 ) and is called the behavior of 𝑁.
   For modeling complex systems, one can use colored Petri nets (CP-nets). In CP-nets, tokens
are attached with values belonging to different domains (color types). Let 𝒰 be the set of these
different 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 𝐢𝑃𝑁 = (𝑃, 𝑇 , 𝐹 , t y p e , π‘Š ) where:
    β€’ (𝑃, 𝑇 , 𝐹 ) is a Petri net;
    β€’ t y p e ∢ 𝑃 β†’ 𝒰 is a place-typing function, mapping each place to a type in 𝒰;
    β€’ π‘Š ∢ 𝐹 β†’ 𝐸π‘₯π‘π‘Ÿ is an arc expression function. βˆ€π‘Ÿ ∈ 𝐹, if π‘Ÿ is adjacent to a place 𝑝 ∈ 𝑃, then
      the type of π‘Š (π‘Ÿ) corresponds to the type of 𝑝.
   Let 𝐢𝑃𝑁 = (𝑃, 𝑇 , 𝐹 , t y p e , π‘Š ) be a CP-net over a set of domains 𝒰. A marking 𝑀 in CPN is a
function that maps each place 𝑝 ∈ 𝑃 into a multiset of tokens 𝑀(𝑝) ∈ β„™π‘š (t y p e (𝑝)). For a CPN,
we distinguish an initial marking 𝑀0 and a set of final markings Ξ©. A binding 𝑏 of a transition 𝑑
is a function that assigns a value 𝑏(𝑣) to each variable 𝑣 occurring in the expression of an arc
adjacent to 𝑑. For each variable 𝑣, 𝑏(𝑣) ∈ β‹ƒπ‘„βˆˆπ’° 𝑄. A pair (𝑑, 𝑏), where 𝑏 is a binding of 𝑑, is called
a binding element. An evaluation π‘Š (𝑝, 𝑑)(𝑏) determines token demands (multiset of tokens) on
𝑝 for 𝑑 to be enabled with the binding 𝑏, and the multiset of tokens that the transition 𝑑 removes
from the place 𝑝 when 𝑑 occurs with the binding 𝑏. π‘Š (𝑑, 𝑝)(𝑏) determines the multiset of tokens
added to an output place 𝑝. A transition is enabled in a marking 𝑀 w.r.t a binding 𝑏 iff for all
𝑝 ∈ 𝑃, π‘Š (𝑝, 𝑑)(𝑏) βŠ† 𝑀(𝑝). An enabled transition fires in a marking 𝑀 yielding a new marking
   β€²                                   β€²
𝑀 , such that for all places 𝑝, 𝑀 (𝑝) = (𝑀(𝑝) ⧡ π‘Š (𝑝, 𝑑)(𝑏)) βˆͺ π‘Š (𝑑, 𝑝)(𝑏).
   In the following we consider a subclass of nested Petri nets (NP-nets). A NP-net 𝑁 𝑃 consists
of a colored Petri net called the system 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 of atomic colored tokens. A net token is a marked element net,
whereas an atomic colored token is a data value of some domain 𝐷 ∈ π’Ÿ, 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 domains π’Ÿ (e.g., the type of π‘₯ ∈ 𝑉 is 𝐸1 ) and (ii) 𝐢 is a finite set of constants, typed
only over the set of data domains π’Ÿ. Each arc π‘Ÿ is supplied with an arc expression from 𝐸π‘₯π‘π‘Ÿ.
This arc expression can be either: a sum of variables typed over 𝒩 if t y p e (𝑝) ∈ 𝒫 (𝒩 ) where 𝑝
is a place adjacent to arc π‘Ÿ containing net tokens, or an arbitrary sum of distinct variables and
constants typed over π’Ÿ if t y p e (𝑝) ∈ π’Ÿ where 𝑝 is a place adjacent to arc π‘Ÿ containing atomic
colored tokens.
Definition 4 (Nested Petri net). Let π’Ÿ be a finite set of domains, πΏπ‘Žπ‘ β€” a finite set of syn-
chronization labels and 𝐴 β€” a finite set of activities. A nested Petri net (NP-net) is a tuple
𝑁 𝑃 = (𝑆𝑁 , (𝐸1 , ..., πΈπ‘˜ ), πœ†, 𝛿), where:
     β€’ 𝑆𝑁 = (𝑃𝑆𝑁 , 𝑇𝑆𝑁 , 𝐹𝑆𝑁 , t y p e , π‘Š ) is a colored Petri net (called a system net) with two sets of
       places 𝑃𝑁 𝑒𝑑 and π‘ƒπ΄π‘‘π‘œπ‘š (𝑃𝑁 𝑒𝑑 βˆͺ π‘ƒπ΄π‘‘π‘œπ‘š = 𝑃𝑆𝑁 ), such that for all 𝑝 ∈ 𝑃𝑁 𝑒𝑑 , t y p e (𝑝) βŠ† {𝐸1 , ..., πΈπ‘˜ }
       and for all 𝑝 ∈ π‘ƒπ΄π‘‘π‘œπ‘š , t y p e (𝑝) ∈ π’Ÿ;
     β€’ 𝑓 π‘œπ‘Ÿ 𝑖 = 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 what follows, we consider conservative NP-nets [14]. In a conservative NP-net 𝑁 𝑃 =
(𝑆𝑁 , (𝐸1 , ..., πΈπ‘˜ ), πœ†, 𝛿), net tokens cannot be cloned or disappear. In a run, there is a stable set of
net tokens which we distinguish using individual agent names. Let 𝑅 be a set of agent names,
we propose a function c l a s s ∢ 𝑅 β†’ {𝐸1 , ..., πΈπ‘˜ }, which maps to each agent name π‘Ÿ an element
net. We denote by (π‘Ÿ, π‘š) a net token which is characterized by an individual agent name π‘Ÿ with
the corresponding element net c l a s s (π‘Ÿ) and a marking π‘š. The set of all possible net tokens is
denoted by 𝑆a g e n t .
   A marking 𝑀 in a NP-net 𝑁 𝑃 is a function mapping each place 𝑝 ∈ 𝑃𝑆𝑁 to a subset of 𝑆a g e n t 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 place 𝑝 (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 𝑆𝑁 of a NP-net, and let be β€’ 𝑑 = {𝑝1 , ..., 𝑝𝑖 } and 𝑑 β€’ = {π‘ž1 , ..., π‘žπ‘— }
the sets of pre- and post-elements of transition 𝑑. π‘Š (𝑑) = {π‘Š (𝑝1 , 𝑑), ..., π‘Š (𝑝𝑖 , 𝑑), π‘Š (𝑑, π‘ž1 ), π‘Š (𝑑, π‘žπ‘— )}
denotes the set of all arc expressions adjacent to 𝑑. A binding of 𝑑 is a function 𝑏 assigning to each
variable 𝑣, occurring in each expression in π‘Š (𝑑), a value 𝑏(𝑣) ∈ β‹ƒπ·βˆˆπ’Ÿ 𝐷 βˆͺ 𝑆a g e n t . A transition 𝑑
in 𝑆𝑁 is enabled in a marking 𝑀 w.r.t a binding 𝑏 if for all 𝑝 ∈ β€’ 𝑑 π‘Š (𝑝, 𝑑)(𝑏) βŠ† 𝑀(𝑝). An enabled
                                                                    β€²
transition fires in a marking 𝑀 yielding a new marking 𝑀 , such that for all places 𝑝 ∈ 𝑃𝑆𝑁 ,
   β€²
𝑀 (𝑝) = (𝑀(𝑝) ⧡ π‘Š (𝑝, 𝑑)(𝑏)) βˆͺ π‘Š (𝑑, 𝑝)(𝑏). For net tokens from 𝑆a g e n t serving as variable values
in input arc expressions from π‘Š (𝑑), we say that they are involved in the firing of 𝑑. They are
removed from input places and brought to output places of 𝑑.
We consider three kinds of steps in a NP-net:

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
WF-nets. This is also written as:
                                                𝛿(𝑑),π‘Ÿ
                                             π‘š βˆ’βˆ’βˆ’βˆ’β†’ π‘šβ€²
System-autonomous step: let 𝑑 ∈ 𝑇𝑆𝑁 be a transition without a synchronization label in the system
net 𝑆𝑁. A system-autonomous step (also called a transfer step when net tokens are involved) is the
firing 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:
                                                      𝛿(𝑑),𝑏
                                                  𝑀 βˆ’βˆ’βˆ’βˆ’β†’ 𝑀 β€²
Table 1
Event attributes in event logs of multi-agent systems.
                          Event type                                           Attributes
               event refers to...                         Activity              Resource                 Data
               (1) an element-autonomous step                  π‘Ž1                     π‘Ÿ1                 none.
               (2) a system-autonomous step                     π‘Ž             (𝑆𝑁 , {π‘Ÿ1 , ..., π‘Ÿπ‘› })   {𝑑1 , ..., π‘‘π‘š }
               (3) a synchronization step                (π‘Ž, π‘Ž1 , ..., π‘Žπ‘› )    (𝑆𝑁 , π‘Ÿ1 , ..., π‘Ÿπ‘› )    {𝑑1 , ..., π‘‘π‘š }


Synchronization step: let 𝑑 ∈ 𝑇𝑆𝑁 be a transition with a synchronization label πœ†(𝑑), and enabled in
a marking 𝑀 w.r.t a binding 𝑏, and let (π‘Ÿ1 , π‘š1 ), ..., (π‘Ÿπ‘› , π‘šπ‘› ) ∈ 𝑆a g e n t be net tokens involved in the
firing of 𝑑. Then, 𝑑 can fire provided that in each (π‘Ÿπ‘– , π‘šπ‘– ) (1 ≀ 𝑖 ≀ 𝑛) there is an enabled transition
labeled with the same value πœ†(𝑑). Thus, a synchronization step goes in two stages: first, the firing
of transitions 𝑑1 , ..., 𝑑𝑛 in all net tokens involved in the firing of 𝑑, and then, the firing of 𝑑 in 𝑆𝑁
w.r.t. a binding 𝑏. This step is denoted by:
                                               𝛿(𝑑),{(𝛿(𝑑𝑖 ),π‘Ÿπ‘– ),1≀𝑖≀𝑛},𝑏
                                           𝑀 βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’β†’ 𝑀 β€²

Definition 5 (Run, Behavior of a nested Petri net). Let 𝑁 𝑃 be a conservative nested Petri
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 𝑁 𝑃.


3. Event Logs of Multi-Agent Systems
An event log of a multi-agent system is a multiset of traces, where a trace is a sequence of events.
Events consist of an activity name, resources which executed the activity or were involved 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 table 1, we consider
three event types: (1) execution of an activity π‘Ž1 by some resource π‘Ÿ1 , (2) execution of an activity
π‘Ž by the system 𝑆𝑁 where 𝑛 resources (agents) are involved, or (3) the simultaneous execution
of activity π‘Ž by 𝑆𝑁, and activities π‘Ž1 , ..., π‘Žπ‘› by resources π‘Ÿ1 , ..., π‘Ÿπ‘› . 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.

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 𝐢 ∈ π’ž ⇔ 𝐢 = 𝐢1 βˆͺ 𝐢2 / 𝐢1 βŠ† 𝑅𝐡 and 𝐢2 ∈ β„™π‘š (𝐷). A trace is a sequence
𝜎 ∈ (β„°ag e n t βˆͺ β„°s y s t e m βˆͺ β„°s y n c )βˆ— where β„°a g e n t = 𝐡 Γ— 𝑅𝐡 , β„°s y s t e m = (𝑆 Γ— {𝑆𝑁 } Γ— π’ž ), and β„°sy n c =
(𝑆 Γ— {𝑆𝑁 } Γ— 𝒫 (𝐡 Γ— 𝑅𝐡 ) Γ— β„™π‘š (𝐷)). β„’ ∈ β„™π‘š (β„°a g e n t , β„°sy s t e m , β„°s y n c )βˆ— is an event log, i.e., a multiset
of traces.

   Table 2 shows an event log β„’ of the multi-agent system modeled in fig. 1. β„’ contains
information on nine traces. A distinct trace can occur multiple times. For instance, trace 𝜎5
Table 2
An event log of a multi-agent system β„’ in tabular form, whose expected behavior is modeled in fig. 1.
   Trace                                                                                                      Freq.
   𝜎1 = ⟨ (𝑑, π‘Ÿ1 ), (𝑑, π‘Ÿ2 ), (β„Ž, π‘Ÿ1 ), (β„Ž, π‘Ÿ2 ), (π‘Ž, 𝑆𝑁 , {(𝑓 , π‘Ÿ1 )}), (π‘Ž, 𝑆𝑁 , {(𝑓 , π‘Ÿ2 )}),                 4
   (𝑏, 𝑆𝑁 , {π‘Ÿ2 }), (𝑏, 𝑆𝑁 , {π‘Ÿ1 }) ⟩
   𝜎2 = ⟨ (𝑑, π‘Ÿ2 ), (β„Ž, π‘Ÿ2 ), (𝑑, π‘Ÿ1 ), (β„Ž, π‘Ÿ1 )(π‘Ž, 𝑆𝑁 , {(𝑓 , π‘Ÿ2 )}), (π‘Ž, 𝑆𝑁 , {(𝑓 , π‘Ÿ1 )}),                  1
   (𝑏, 𝑆𝑁 , {π‘Ÿ1 }), (𝑏, 𝑆𝑁 , {π‘Ÿ2 }) ⟩
   𝜎3 = ⟨ (𝑑, π‘Ÿ2 ), (𝑒, π‘Ÿ2 ), (𝑑, π‘Ÿ1 ), (β„Ž, π‘Ÿ1 ), ((𝑐, 𝑆𝑁 , {(𝑔, π‘Ÿ1 )}), (𝑐, 𝑆𝑁 , {(𝑔, π‘Ÿ2 )}) ⟩                1
   𝜎4 = ⟨ (𝑑, π‘Ÿ1 ), (𝑑, π‘Ÿ2 ), (β„Ž, π‘Ÿ2 ), (𝑒, π‘Ÿ1 ), (𝑐, 𝑆𝑁 , {(𝑔, π‘Ÿ2 )}), (𝑐, 𝑆𝑁 , {(𝑔, π‘Ÿ1 )}) ⟩                 1
   𝜎5 = ⟨ (𝑑, π‘Ÿ1 ), (𝑑, π‘Ÿ2 ), (𝑒, π‘Ÿ1 ), (𝑒, π‘Ÿ2 ), (π‘Ž, 𝑆𝑁 , {(𝑓 , π‘Ÿ1 )}), (𝑐, 𝑆𝑁 , {(𝑔, π‘Ÿ2 )}),                 2
   (𝑏, 𝑆𝑁 , {π‘Ÿ1 }) ⟩



occurred two times. It is a sequence of seven events. First, both activities 𝑑 and 𝑒 were executed
by agents π‘Ÿ1 and π‘Ÿ2 . Next, the system 𝑆𝑁 executed two synchronization steps with agents π‘Ÿ1 and
π‘Ÿ2 , where activities π‘Ž and 𝑓, and later 𝑐 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 and 𝑁 𝑃 β€” 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 transition 𝑑 without
      synchronization label in a net token named π‘Ÿ where 𝛿(𝑑) = π‘Ž, and 𝑑 can fire in a marking
                                                                       𝛿(𝑑),π‘Ÿ
       π‘š producing a new marking π‘šβ€² , i.e., π‘š βˆ’βˆ’βˆ’βˆ’β†’ π‘šβ€² in 𝑁 𝑃 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 where 𝛿(𝑑) = π‘Ž, and 𝑑 can fire in a marking 𝑀 w.r.t.
      a binding 𝑏 such that 𝑏 assigns the atomic tokens 𝑑1 , ..., π‘‘π‘š to the variables in π‘Š (𝑑), i.e.,
            𝛿(𝑑),𝑏
       𝑀 βˆ’βˆ’βˆ’βˆ’β†’ 𝑀 β€² in 𝑁 𝑃.

    β€’ An event (π‘Ž, 𝑆𝑁 , {(π‘Ž1 , π‘Ÿ1 ), ..., (π‘Žπ‘ž , π‘Ÿπ‘ž )}, {𝑑1 , ..., 𝑑𝑝 }) is syntactically correct w.r.t. a step in
      𝑁 𝑃 if there is a transition 𝑑 ∈ 𝑇𝑆𝑁 with synchronization label πœ†(𝑑) where 𝛿(𝑑) = π‘Ž,
      (π‘Ÿ1 , π‘š1 ), ..., (π‘Ÿπ‘› , π‘šπ‘› ) are net tokens involved in the firing of 𝑑 such that in each (π‘Ÿπ‘– , π‘šπ‘– ) there
      is an enabled transition 𝑑𝑖 (𝛿(𝑑𝑖 ) = π‘Žπ‘– ) labeled with the same value πœ†(𝑑), and 𝑑 can fire in
      a marking 𝑀 w.r.t. a binding 𝑏 assigning the atomic tokens 𝑑1 , ..., 𝑑𝑝 and also the agent
                                                                                𝛿(𝑑),{(𝛿(𝑑𝑖 ),π‘Ÿπ‘– ),1≀𝑖≀𝑛},𝑏
       names π‘Ÿ1 , ..., π‘Ÿπ‘ž to the variables in π‘Š (𝑑), i.e., 𝑀 βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’β†’ 𝑀 β€² 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 iff the event log is
Table 3
Projections 𝐿𝑆𝑁 , 𝐿1 , and 𝐿2 from the event log β„’ (cf. Table 2) onto (a) the system net 𝑆𝑁, and agents (b)
π‘Ÿ1 and (c) π‘Ÿ2 from 𝑁 (cf. Fig. 1).

        Trace                                              Freq.
                                                                    Trace          Freq.
        ⟨(π‘Ž, {π‘Ÿ1 }), (π‘Ž, {π‘Ÿ2 }), (𝑏, {π‘Ÿ2 }), (𝑏, {π‘Ÿ1 })⟩     4                                Trace          Freq.
                                                                   βŸ¨π‘‘, β„Ž, 𝑓 ⟩        5
        ⟨(π‘Ž, {π‘Ÿ2 }), (π‘Ž, {π‘Ÿ1 }), (𝑏, {π‘Ÿ1 }), (𝑏, {π‘Ÿ2 })⟩     1                               βŸ¨π‘‘, β„Ž, 𝑓 ⟩        5
                                                                   βŸ¨π‘‘, β„Ž, π‘”βŸ©         1
        ⟨(𝑐, {π‘Ÿ1 }), (𝑐, {π‘Ÿ2 })⟩                             1                               βŸ¨π‘‘, 𝑒, π‘”βŸ©         3
                                                                   βŸ¨π‘‘, 𝑒, π‘”βŸ©         1
        ⟨(𝑐, {π‘Ÿ2 }), (𝑐, {π‘Ÿ1 })⟩                             1                               βŸ¨π‘‘, β„Ž, π‘”βŸ©         1
                                                                   βŸ¨π‘‘, 𝑒, 𝑓 ⟩        2
        ⟨(π‘Ž, {π‘Ÿ1 }), (𝑐, {π‘Ÿ2 }), (𝑏, {π‘Ÿ1 })⟩                 2                                      (c) 𝐿2
                                                                          (b) 𝐿1
                                  (a) 𝐿𝑆𝑁


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, and πœŽβ†Ύπ‘’ β€” the
π‘π‘Ÿπ‘œπ‘—π‘’π‘π‘‘π‘–π‘œπ‘› of sequence 𝜎 on an element 𝑒.

Definition 7 (Trace projection onto an agent). Let 𝑋 = (β„°a g e n t βˆͺ β„°s y s t e m βˆͺ β„°s y n c ) be a set
of events, 𝐡 β€” a set of agent activities, and 𝑅𝐡 β€” a set of agent names. β†Ύπ‘Ÿβˆˆπ‘…π΅ ∈ 𝑋 βˆ— ⟢ π΅βˆ— is a
projection function defined recursively: (1)βŸ¨βŸ©β†Ύπ‘Ÿβˆˆπ‘…π΅ = ⟨⟩ (2) For 𝜎 ∈ 𝑋 βˆ— and 𝑒 ∈ 𝑋:
    β€’ If 𝑒 = (π‘₯, 𝑦) ∈ β„°a g e n t , 𝑦 = π‘Ÿ, then (βŸ¨π‘’βŸ©.𝜎 )β†Ύπ‘Ÿβˆˆπ‘…π΅ = ⟨π‘₯⟩.πœŽβ†Ύπ‘Ÿβˆˆπ‘…π΅ ;
    β€’ If 𝑒 = (π‘₯, 𝑆𝑁 , {(π‘₯1 , 𝑦1 ), ..., (π‘₯𝑛 , 𝑦𝑛 )}, {𝑑1 , ..., 𝑑𝑝 }) ∈ β„°s y n c , 𝑦𝑖 = π‘Ÿ, 1 ≀ 𝑖 ≀ 𝑛, then (βŸ¨π‘’βŸ©.𝜎 )β†Ύπ‘Ÿβˆˆπ‘…π΅ =
       ⟨π‘₯𝑖 ⟩.πœŽβ†Ύπ‘Ÿβˆˆπ‘…π΅ ;
    β€’ Otherwise (βŸ¨π‘’βŸ©.𝜎 )β†Ύπ‘Ÿβˆˆπ‘…π΅ = πœŽβ†Ύπ‘Ÿβˆˆπ‘…π΅                          .

Definition 8 (Trace projection onto a system net). Let 𝑋 = (β„°a g e n t βˆͺ β„°s y s t e m βˆͺ β„°s y n c ) 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: (1) βŸ¨βŸ©β†Ύπ‘†π‘ = ⟨⟩ (2) For 𝜎 ∈ 𝑋 βˆ— and 𝑒 ∈ 𝑋:
    β€’ If 𝑒 = (π‘₯, 𝑆𝑁 , {𝑑1 , ..., 𝑑𝑝 }) ∈ β„°sy s t e m , then (βŸ¨π‘’βŸ©.𝜎 )↾𝑆𝑁 = ⟨(π‘₯, {𝑑1 , ..., 𝑑𝑝 })⟩.πœŽβ†Ύπ‘†π‘ ;
    β€’ If 𝑒 = (π‘₯, 𝑆𝑁 , {(π‘₯1 , 𝑦1 ), ..., (π‘₯𝑛 , 𝑦𝑛 )}, {𝑑1 , ..., 𝑑𝑝 }) ∈ β„°s y n c , then (βŸ¨π‘’βŸ©.𝜎 )↾𝑆𝑁 =
       ⟨(π‘₯, {𝑦1 , ..., 𝑦𝑛 , 𝑑1 , ..., 𝑑𝑝 })⟩.πœŽβ†Ύπ‘†π‘ ;
    β€’ Otherwise (βŸ¨π‘’βŸ©.𝜎 )↾𝑆𝑁 = πœŽβ†Ύπ‘†π‘                        .

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. Table 2) onto components of the NP-net 𝑁 (cf. Fig. 1). Table 3 shows the
three decomposed event logs 𝐿𝑆𝑁 , 𝐿1 , and 𝐿2 resulting from the projection of β„’ 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 marking 𝑀 in a NP-net 𝑁 𝑃, marking
projections onto 𝑁 𝑃 components are defined as follows: (1) the projection of 𝑀 onto a system
net 𝑆𝑁, denoted as 𝑀↾𝑆𝑁 , is a marking of the colored Petri net 𝑆𝑁 obtained by replacing all
net tokens in 𝑀 by their agent names, and (2) the projection of 𝑀 onto a net token (π‘Ÿ, π‘š),
denoted as 𝑀↾(π‘Ÿ,π‘š) , is just π‘š. A system net component 𝑆𝑁, with a marking 𝑀↾𝑆𝑁 and without
synchronization labels, is a CP-net labeled by activity names. A sequence of binding elements
⟨(𝑑1 , 𝑏1 ), ..., (𝑑𝑛 , 𝑏𝑛 )⟩, starting from the initial marking 𝑀0 ↾𝑆𝑁 and ending in a final marking 𝑀𝑓 ↾𝑆𝑁 ,
projected onto the set of system net activities is called a run.

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 of β„’, and 𝐿𝑆𝑁 –- a projection of β„’ onto actions of the system net.
𝐿𝑆𝑁 perfectly fits 𝑆𝑁 if and only if for all 𝜎 = βŸ¨π‘’1 , ..., π‘’π‘š ⟩ ∈ 𝐿𝑆𝑁 , there is a run 𝜎 β€² 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 in π‘Š (𝑑𝑖 ). For 𝑖 = 1, 𝑛, 𝐿𝑖 perfectly fits (π‘Ÿπ‘– , π‘šπ‘– ) if and only if for all 𝜎 = βŸ¨π‘’1 , ..., π‘’π‘š ⟩ ∈ 𝐿𝑖 ,
there is a run 𝜎 β€² in the element net c l a s s (π‘Ÿπ‘– ) 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 log β„’ (cf. Table 2) and the NP-net 𝑁
depicted in fig. 1. Clearly, β„’ perfectly fits 𝑁 𝑃. Also, each projected event log 𝐿𝑆𝑁 , 𝐿1 , or 𝐿2 (cf.
Table 3) perfectly fits the corresponding component in 𝑁 𝑃.

Theorem 1. Given a nested Petri net 𝑁 𝑃 = (𝑆𝑁 , (𝐸1 , ..., πΈπ‘˜ ), πœ†, 𝛿) and an event log
β„’ ∈ β„™π‘š (β„°a g e n t , β„°s y s t e m , β„°s y n c )βˆ— , let (π‘Ÿ1 , π‘š1 ), ..., (π‘Ÿπ‘› , π‘šπ‘› ) be net tokens of 𝑁 𝑃, 𝐿1 , ..., 𝐿𝑛 –
corresponding projections of β„’, and 𝐿𝑆𝑁 – a projection of β„’ onto the system net 𝑆𝑁. β„’ perfectly
fits 𝑁 𝑃 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 , ..., πΈπ‘˜ ), πœ†, 𝛿) β€” a nested
Petri net, and (π‘Ÿ1 , π‘š1 ), ..., (π‘Ÿπ‘› , π‘šπ‘› ) β€” net tokens of 𝑁 𝑃.
   (β‡’) Let 𝜎 = βŸ¨π‘’1 , ..., π‘’π‘š ⟩ ∈ β„’ be such that there is a run 𝜎 β€² = βŸ¨π‘ 1 , ..., π‘ π‘š ⟩ ∈ ℬ(𝑁 𝑃) and for
𝑗 = 1, π‘š:
                                           𝛿(𝑑),π‘Ÿ
     β€’ if 𝑒𝑖 = (π‘Ž, π‘Ÿ), then 𝑠𝑖 = π‘š βˆ’βˆ’βˆ’βˆ’β†’ π‘šβ€² where 𝑑 ∈ 𝐸𝑖 , 1 ≀ 𝑖 ≀ π‘˜, c l a s s (𝐸𝑖 ) = π‘Ÿ, and 𝛿(𝑑) = π‘Ž. (1)
                                                             𝛿(𝑑),𝑏
     β€’ if 𝑒𝑖 = (π‘Ž, 𝑆𝑁 , 𝑑1 , ..., 𝑑𝑝 ), then 𝑠𝑖 = 𝑀 βˆ’βˆ’βˆ’βˆ’β†’ 𝑀 β€² where 𝛿(𝑑) = π‘Ž, and 𝑏 is a binding assigning
       the atomic tokens 𝑑1 , ..., 𝑑𝑝 to the variables in π‘Š (𝑑). (2)
                                                                                             𝛿(𝑑),{(𝛿(𝑑𝑖 ),π‘Ÿπ‘– ),1β‰€π‘–β‰€π‘ž},𝑏
     β€’ if 𝑒𝑖 = (π‘Ž, 𝑆𝑁 , {(π‘Ž1 , π‘Ÿ1 ), ..., (π‘Žπ‘ž , π‘Ÿπ‘ž )}, {𝑑1 , ..., 𝑑𝑝 }), then 𝑠𝑖 = 𝑀 βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’β†’ 𝑀 β€² where
       𝛿(𝑑) = π‘Ž,, 𝛿(𝑑𝑖 ) = π‘Žπ‘– , 1 ≀ 𝑖 ≀ π‘ž, and 𝑏 is a binding assigning the atomic tokens 𝑑1 , ..., 𝑑𝑝 and
       also the agent names π‘Ÿ1 , ..., π‘Ÿπ‘ž to the variables in π‘Š (𝑑). (3)

i.e., 𝜎 perfectly fits 𝑁 𝑃. We need to prove that

     β€’ 𝜎 is syntactically correct w.r.t 𝑁 𝑃;

     β€’ 𝜎 ↾𝑆𝑁 = βŸ¨π‘’1𝑠 , ..., π‘’π‘š
                            𝑠 ⟩ perfectly fits the system net component, i.e., there is a run 𝜎
                              β€²                                                                𝑆𝑁 in the
       system net component where:
                                               𝛿(𝑑1 ),𝑏1          𝛿(𝑑2 ),𝑏2                  𝛿(π‘‘π‘šβ€² ),π‘π‘šβ€²
                              πœŽπ‘†π‘ = (𝑀0 βˆ’βˆ’βˆ’βˆ’βˆ’β†’ 𝑀1 βˆ’βˆ’βˆ’βˆ’βˆ’β†’ 𝑀2 ...π‘€π‘šβ€² βˆ’1 βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’β†’ 𝑀𝑓 )

       , and for 𝑖 = 1, π‘šβ€² , 𝑒𝑖𝑠 = (π‘Žπ‘– , {𝑑1𝑖 , ..., 𝑑𝑝𝑖 }), 𝛿(𝑑𝑖 ) = π‘Žπ‘– , and 𝑏𝑖 is the binding that assigns {𝑑1𝑖 , ..., 𝑑𝑝𝑖 }
       to the variables in π‘Š (𝑑𝑖 );

     β€’ for 𝑖 = 1, 𝑛, 𝜎 β†Ύπ‘Ÿπ‘– = βŸ¨π‘Ž1𝑖 , ..., π‘Žπ‘š
                                          𝑖 ⟩ perfectly fits (π‘Ÿ , π‘š ), i.e., there is a run 𝜎 in the element net
                                            β€³                  𝑖 𝑖                           π‘Ÿπ‘–
       c l a s s (π‘Ÿπ‘– ) where:
                                                    𝛿(𝑑1 )            𝛿(𝑑2 )              𝛿(π‘‘π‘šβ€³ )
                                     πœŽπ‘Ÿπ‘– = (π‘š0 βˆ’βˆ’βˆ’βˆ’β†’ π‘š1 βˆ’βˆ’βˆ’βˆ’β†’ π‘š2 ...π‘šπ‘šβˆ’1 βˆ’βˆ’βˆ’βˆ’βˆ’β†’ π‘šπ‘“ )
       and for 𝑗 = 1, π‘šβ€³ , 𝛿(𝑑𝑗 ) = π‘Žπ‘—π‘– .

   By the fact that 𝜎 perfectly fits 𝑁 𝑃, it follows trivially that 𝜎 is syntactically correct w.r.t 𝑁 𝑃
(cf. Def. 9).
   Taking into account that 𝜎 β€² = βŸ¨π‘ 1 , ..., π‘ π‘š ⟩ is a run in 𝑁 𝑃 (which can hold synchronization
labels) where for 𝑖 = 1, π‘š we have (1), (2) and (3), and that

                            ⟨⟩,                                            𝑖𝑓 𝑒𝑖 = (π‘Ž, π‘Ÿ)
                          ⎧
                          βŽͺ ⟨(π‘Ž, {𝑑1 , ..., 𝑑𝑝 })⟩,                    𝑖𝑓 𝑒𝑖 = (π‘Ž, 𝑆𝑁 , 𝑑1 , ..., 𝑑𝑝 )             (4)
              βŸ¨π‘’π‘– ⟩ ↾𝑆𝑁 =
                          ⎨ ⟨(π‘Ž, {π‘Ÿ 1 , ..., π‘Ÿ  ,
                                               π‘ž 1𝑑 , ..., 𝑑 𝑝 })⟩, 𝑖𝑓 𝑒 𝑖 =  (π‘Ž, 𝑆𝑁 , {(π‘Ž  ,
                                                                                           1 1π‘Ÿ  ), ...,
                          βŽͺ
                          ⎩                                                          (π‘Žπ‘ž , π‘Ÿπ‘ž )}, {𝑑1 , ..., 𝑑𝑝 })

(cf. Def. 8) we deduce that for 𝜎 ↾𝑆𝑁 = βŸ¨π‘’1𝑠 , ..., π‘’π‘š
                                                     𝑠 ⟩, there is a run 𝜎 in the system net component
                                                       β€²                  𝑆𝑁
where:
                                 𝛿(𝑑1 ),𝑏1        𝛿(𝑑2 ),𝑏2              𝛿(π‘‘π‘šβ€² ),π‘π‘šβ€²
                    πœŽπ‘†π‘ = (𝑀0 βˆ’βˆ’βˆ’βˆ’βˆ’β†’ 𝑀1 βˆ’βˆ’βˆ’βˆ’βˆ’β†’ 𝑀2 ...π‘€π‘šβ€² βˆ’1 βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’βˆ’β†’ 𝑀𝑓 )
and for 𝑖 = 1, π‘šβ€² , 𝑒𝑖𝑠 = (π‘Žπ‘– , {𝑑1𝑖 , ..., 𝑑𝑝𝑖 }), 𝛿(𝑑𝑖 ) = π‘Žπ‘– , and 𝑏𝑖 is the binding that assigns {𝑑1𝑖 , ..., 𝑑𝑝𝑖 } to
the variables in π‘Š (𝑑𝑖 ). Therefore, 𝜎 ↾𝑆𝑁 perfectly fits the system net component.
   Now by the fact that 𝜎 β€² is a run in 𝑁 𝑃 (which can hold synchronization labels) where for
𝑖 = 1, π‘š we have (1), (2) and (3), and that for 𝑗 = 1, 𝑛

                           βŸ¨π‘ŽβŸ©,                𝑖𝑓 𝑒𝑖 = (π‘Ž, π‘Ÿπ‘— )
                         ⎧
                         βŽͺ βŸ¨π‘Žπ‘— ⟩, 1 ≀ 𝑗 ≀ π‘ž, 𝑖𝑓 𝑒𝑖 = (π‘Ž, 𝑆𝑁 , {(π‘Ž1 , π‘Ÿ1 ), ..., (π‘Žπ‘ž , π‘Ÿπ‘ž )},   (5)
             βŸ¨π‘’π‘– ⟩ β†Ύπ‘Ÿπ‘— =
                         ⎨                                            {𝑑1 , ..., 𝑑𝑝 })
                         βŽͺ
                         ⎩ ⟨⟩,                 π‘œπ‘‘β„Žπ‘’π‘Ÿπ‘€π‘–π‘ π‘’

(cf. Def. 7) it follows that for 𝜎 β†Ύπ‘Ÿπ‘– = βŸ¨π‘Ž1 , ..., π‘Žπ‘šβ€³ ⟩, 1 ≀ 𝑖 ≀ 𝑛, there is a run πœŽπ‘Ÿπ‘– in the element net
c l a s s (π‘Ÿπ‘– ) where:
                                           𝛿(𝑑1 )      𝛿(𝑑2 )                 𝛿(π‘‘π‘šβ€³ )
                             πœŽπ‘Ÿπ‘– = (π‘š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 𝜎
perfectly fits 𝑁 𝑃.
  Taking into account (4) and (5), and that 𝜎 is syntactically correct w.r.t 𝑁 𝑃, we deduce that by
associating to each element of the projected sequences the corresponding resource, elements
can be merged together into the trace 𝜎. Therefore, being 𝜎 ↾𝑆𝑁 perfectly fits the system net
component and for 𝑖 = 1, 𝑛 𝜎 β†Ύπ‘Ÿπ‘– perfectly fits (π‘Ÿπ‘– , π‘šπ‘– ), then 𝜎 perfectly fits 𝑁 𝑃 and this concludes
the proof.


5. Conclusions and Future Work
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 confor-
mance 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.


Acknowledgments
This work is supported by the Basic Research Program at the National Research University
Higher School of Economics.


References
 [1] W. van der Aalst, Process Mining: Data Science in Action, 2nd ed., Springer, 2016.
 [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 (2019), https://tinyurl.com/y55sndcv, ????
 [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
     Circuits, Systems and Computers 08 (1998) 21–66.
[14] I. A. Lomazova, V. O. Ermakova, Verification of Nested Petri Nets Using an Unfolding Ap-
     proach, in: L. Cabac, L. M. Kristensen, H. RΓΆlke (Eds.), Petri Nets and Software Engineering,
     volume 1591 of CEUR Workshop Proceedings, 2016.