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)
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.
β 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 π.
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 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 πΈπ₯ππ.
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 π(π) β β π (type(π)). 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.
π π = (ππ , (πΈ 1 , ..., πΈ π ), π, πΏ), where: 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:
An event log of a multi-agent system β in tabular form, whose expected behavior is modeled in fig. 1.
Freq. π 1 = β¨ (π, π 1 ), (π, π 2 ), (β, π 1 ), (β, π 2 ), (π, ππ , {(π , π 1 )}), (π, ππ , {(π , π 2 )}), (π, ππ , {π 2 }), (π, ππ , {π 1 }) β© 4 π 2 = β¨ (π, π 2 ), (β, π 2 ), (π, π 1 ), (β, π 1 )(π, ππ , {(π , π 2 )}), (π, ππ , {(π , π 1 )}), (π, ππ , {π 1 }), (π, ππ , {π 2 }) β© 1 π 3 = β¨ (π, π 2 ), (π, π 2 ), (π, π 1 ), (β, π 1 ), ((π, ππ , {(π, π 1 )}), (π, ππ , {(π, π 2 )}) β© 1 π 4 = β¨ (π, π 1 ), (π, π 2 ), (β, π 2 ), (π, π 1 ), (π, ππ , {(π, π 2 )}), (π, ππ , {(π, π 1 )}) β© 1 π 5 = β¨ (π, π 1 ), (π, π 2 ), (π, π 1 ), (π, π 2 ), (π, ππ , {(π , π 1 )}), (π, ππ , {(π, π 2 )}), (π, ππ , {π 1 }) β© 2 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.
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
This work is supported by the Basic Research Program at the National Research University Higher School of Economics.
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).
Freq. β¨(π, {π 1 }), (π, {π 2 }), (π, {π 2 }), (π, {π 1 })β© 4 β¨(π, {π 2 }), (π, {π 1 }), (π, {π 1 }), (π, {π 2 })β© 1 β¨(π, {π 1 }), (π, {π 2 })β© 1 β¨(π, {π 2 }), (π, {π 1 })β© 1 β¨(π, {π 1 }), (π, {π 2 }), ( 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.
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
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:
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, π: 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:
, 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:
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 , ..., π π })β©, ππ π π = (π, ππ , {(π 1 , π 1 ), ..., (π π , π π )}, {π 1 , ..., π π }) (cf. Def. 8) we deduce that for π βΎ ππ = β¨π π 1 , ..., π π π β² β©, there is a run π ππ in the system net component where:
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:
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.
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.