11institutetext: Department of Mathematics and Computer Science
Eindhoven University of Technology, Eindhoven, the Netherlands
11email<EMAIL_ADDRESS>
#  Exact and Approximated Log Alignments for Processes with Inter-case
Dependencies

Dominique Sommers  Natalia Sidorova  Boudewijn van Dongen

###### Abstract

The execution of different cases of a process is often restricted by inter-
case dependencies through e.g., queueing or shared resources. Various high-
level Petri net formalisms have been proposed that are able to model and
analyze coevolving cases. In this paper, we focus on a formalism tailored to
conformance checking through alignments, which introduces challenges related
to constraints the model should put on interacting process instances and on
resource instances and their roles. We formulate requirements for modeling and
analyzing resource-constrained processes, compare several Petri net extensions
that allow for incorporating inter-case constraints. We argue that the
Resource Constrained $\nu$-net is an appropriate formalism to be used the
context of conformance checking, which traditionally aligns cases individually
failing to expose deviations on inter-case dependencies. We provide formal
mathematical foundations of the globally aligned event log based on theory of
partially ordered sets and propose an approximation technique based on the
composition of individually aligned cases that resolves inter-case violations
locally.

###### Keywords:

Petri nets Conformance checking Inter-case dependencies Shared resources.

##  1 Introduction

Event logs record which activity is executed at which moment of time, and
additionally they often include indications which resources were involved in
which activity, mentioning the exact person(s) or machine(s). The availability
of such event logs enables the use of conformance checking for resource-
constrained processes, analyzing not only the single instance control-flow
perspective, but also checking whether and where the actual process behavior
recorded in an event log deviates from the resource constraints prescribed by
a process model.

Process models, and specifically Petri nets with their precise semantics, are
often used to describe and reason about the execution of a process. In many
approaches, a process model considers a process instance (a case) in isolation
from other cases [1]. In practice, however, a process instance is usually
subject to interaction with other cases and/or resources, whose availability
puts additional constraints on the process execution. In order to expose
workflow deviations caused by inter-case dependencies, it is crucial to use
models considering multiple cases simultaneously.

There are several approaches to modeling and analysis of processes with inter-
case dependencies. In [7] and [12], Petri nets are extended with resources to
model availability of durable resources, with multiple cases competing by
claiming and releasing these _shared_ resources. To distinguish the cases,
$\nu$-Petri nets [22] incorporate name creation and management as a minimal
extension to classical Petri nets, with the advantage that coverability and
termination are still decidable, opposed to more advanced Petri net
extensions. The functionality of $\nu$-Petri nets is inherited in other
extensions such as Catalog Petri nets [11], synchronizing proclet models [10],
resource and instance-aware workflow nets (RIAW-nets) [18], DB-nets [19] and
resource constrained $\nu$-Petri nets [24], all with the ability to handle
multiple cases simultaneously. For the latter, the cases are assumed to follow
the same process, interacting via (abstract) shared resources in a one-to-many
relation, i.e., a resource instance can be claimed by one case at a time. More
sophisticated extensions allow for cases from various perspectives with many-
to-many interactions, via e.g., concepts from databases, shared resources and
proclet channels. This may impose, however, problems of undecidability during
conformance checking, which we discuss in this work.

Many conformance checking techniques use _alignments_ to expose where the
behavior recorded in a log and the model agree, which activities prescribed by
the model are missing in the log and which log activities should not be
performed according to the model [8, 3]. The usual focus is on the control
flow of the process. In more advanced techniques [6, 15, 16, 17], data and/or
resource information is additionally incorporated in the alignments by
considering these perspective only after the control flow [15], by balancing
the different perspectives in a customizable manner [16] or by considering all
perspectives at once [17]. These three types of techniques operate on a case-
by-case basis, which can lead to misleading results in case of shared
resources, e.g., when multiple cases claim the same resource simultaneously.

In our previous work we considered the execution of all process instances by
aligning the complete event log to a resource constrained $\nu$-Petri nets
[24]. In this paper, we present our further steps: (1) We compare how the
existing Petri net extensions support modeling and analysis of processes with
inter-case dependencies by formulating the requirements to such models, and we
argue that $\nu$-nets are an appropriate formalism. (2) We employ the poset
theory to provide mathematical foundations for aligning the complete event log
and exposing deviations of inter-case dependencies; (3) We propose an
approximation method for computing optimal alignments in practice, which
tackles the limitation of the computational efficiency when computing the
complete event log alignment. The approximation method is based on composing
alignments for isolated cases first and then resolving inter-case conflicts
and deviations in the log locally.

The paper is organized as follows. In Section 2 we introduce basic concepts of
the poset theory, Petri nets and event logs. In Section 3 we compare different
Petri net extensions. We provide the mathematical foundations of the complete
event log alignment in Section 4. Section 5 presents the approximation method
for computing alignments. We discuss implications of our work in Section 6.

##  2 Preliminaries

In this section, we introduce basic concepts related to Petri nets and event
logs and present the notations that we will use throughout the paper.

###  2.1 Multisets and posets

We start with definitions and notation regarding multisets and partially
ordered sets.

###### Definition 1

(Multiset) A _multiset_ $m$ over a set $X$ is $m:X\rightarrow\mathbb{N}$.
$X^{\oplus}$ denotes the set of all multisets over $X$. We define the support
$\mathit{supp}(m)$ of a multiset $m$ as the set $\\{x\in X\mid m(x)>0\\}$. We
list elements of the multiset as $[m(x)\cdot x\mid x\in X]$, and write $|x|$
for $m(x)$, when it is clear from context which multiset it concerns.

For two multisets $m_{1},m_{2}$ over $X$, we write $m_{1}\leq m_{2}$ if
$\forall_{x\in X}m_{1}(x)\leq m_{2}(x)$, and $m_{1}<m_{2}$ if $m_{1}\leq
m_{2}\wedge m_{1}\neq m_{2}$. We define $m_{1}+m_{2}=[(m_{1}(x)+m_{2}(x))\cdot
x\mid x\in X]$, and $m_{1}-m_{2}=[\max(0,m_{1}(x)-m_{2}(x))\cdot x\mid x\in
X]$ for $m_{1}\geq m_{2}$.

Furthermore, $m_{1}\sqcup~{}m_{2}=[\max(m_{1}(x),m_{2}(x))\cdot x\mid x\in
X]$, $m_{1}\sqcap m_{2}=[\min(m_{1}(x),m_{2}(x))\cdot x\mid x\in X]$.

In some cases, we consider multisets over a set $X$ as vectors of length
$|X|$, assuming an arbitrary but fixed ordering of elements of $X$.

###### Definition 2

(Partial order, Partially ordered set, Antichains) A _partially ordered set_
(_poset_) $X=(\bar{X},\prec_{X})$ is a pair of a set $\bar{X}$ and a _partial
order_ $\prec_{X}\subseteq X\times X$. We overload the notation and write
$x\in X$ if $x\in\bar{X}$. For $x,y\in X$, we write $x\|_{X}y$ if $x\nprec
y\wedge y\nprec x$ and $x\preceq y$ if $x\prec y\vee x=y$.

Given $\prec_{X}$, we define $\prec_{X}^{+}$ to be the smallest transitively
closed relation containing $\prec_{X}$. Thus $\prec_{X}^{+}$ is a partial
order with $\prec_{X}\subseteq\prec_{X}^{+}$.

We extend the standard set operations of union, intersection, difference and
subsets to posets: for any two posets $X$ and $Y$, $X\circ
Y=(\bar{X}\circ\bar{Y},(\prec_{X}\circ\prec_{Y})^{+})$, with
$\circ\in\\{\cup,\cap,\setminus\\}$ and $Y\subseteq X$ iff
$\bar{Y}\subseteq\bar{X}$ and $\prec_{Y}=\prec_{X}\cap(\bar{Y}\times\bar{Y})$.

A poset $A$ is an _antichain_ if no elements of $A$ are comparable, i.e.,
$\forall_{x,y\in A}~{}x\|y$. For poset $X$, $\mathcal{A}(X)$ denotes the set
of all _antichains_ $A\subseteq X$, and $\mathcal{A}^{+}(X)$ is the set of all
_maximal antichains_ : $\mathcal{A}^{+}(X)=\\{A\mid
A\in\mathcal{A}(X),\forall_{B\in\mathcal{A}(X)}~{}B\subseteq A\implies
B=A\\}$.

Two special maximal antichains are the _minimum_ and _maximum_ elements of
$X$, defined by $\min(X)=\\{x\mid x\in X,\forall_{y\in X}y\nprec
x\\}\in\mathcal{A}^{+}(X)$ and $\max(X)=\\{x\mid x\in X,\forall_{y\in
X}x\nprec y\\}\in\mathcal{A}^{+}(X)$.

We define
$X^{<}=\\{(\bar{Y},\prec_{Y})\mid\bar{Y}=\bar{X},\prec_{X}\subseteq\prec_{Y},\forall_{a,b\in
Y,a\neq b}~{}a\not\|_{Y}b\\}$ to be the set of totally ordered permutations of
$X$ that respect the partial order.

###### Definition 3

(Interval, prefix and postfix in a poset) With a poset $X$ and two antichains
$A,B\in\mathcal{A}(X)$, the _closed jhkcbvinterval_ from $A$ to $B$ is the
subposet defined as follows:
$[A,B]=(\overline{AB},\prec_{X}\cap(\overline{AB}\times\overline{AB}))$ with
$\overline{AB}=\\{x\mid x\in X,A\preceq x\preceq B\\}$, and the half open and
open intervals: $(A,B]=[A,B]\setminus A$, $[A,B)=[A,B]\setminus B$ and
$(A,B)=[A,B)\setminus A$.

Artificial minimal and maximal elements are denoted as $\bot$ and $\top$
respectively, i.e., $\forall_{x\in X}\bot\prec x\prec\top$. $(\bot,A]$,
$(\bot,A)$, $[A,\top)$ $(A,\top)$ denote the corresponding _prefixes and
postfixes_ of an antichain $A\in\mathcal{A}(X)$ in $X$.

###  2.2 Petri nets

Petri nets can be used as a tool for the representation, validation and
verification of workflow processes to provide insights in how a process
behaves [21].

###### Definition 4

(Labeled Petri nets, Pre-set, Post-set) A _labeled Petri net_ [20] is a tuple
$N=(P,T,\mathcal{F},\ell)$, with sets of places and transitions $P$ and $T$,
respectively, such that $P\cap T=\emptyset$, and a multiset of arcs
$\mathcal{F}:(P\times T)\cup(T\times P)\rightarrow\mathbb{N}$ defining the
flow of the net. $\ell:T\rightarrow\Sigma^{\tau}=\Sigma\cup\\{\tau\\}$ is a
_labeling_ function, assigning each transition $t$ a label $\ell(t)$ from
alphabet $\Sigma$ or $\ell(u)=\tau$ for silent transitions.

We assume that the _intersection, union and subsets_ are only defined for two
labeled Petri nets $N_{1}$, $N_{2}$ where $\forall_{t\in T_{1}\cap
T_{2}}\ell_{1}(t)=\ell_{2}(t)$.

Given an element $x\in P\cup T$, its _pre- and post-set_
$\prescript{\bullet}{}{x}$ ($x^{\bullet}$) are multisets defined by
$\prescript{\bullet}{}{x}=[\mathcal{F}(y,x)\cdot y\mid y\in P\cup T]$ and
$x^{\bullet}=[\mathcal{F}(x,y)\cdot y\mid y\in P\cup T]$ resp.

###### Definition 5

(Marking, Enabling and firing of transitions, Reachable markings) A _marking_
$m\in P^{\oplus}$ of a (labeled) Petri net $N=(P,T,\mathcal{F},\ell)$ assigns
how many tokens each place contains and defines the state of $N$.

With $m$ and $N$, a transition $t\in T$ is _enabled_ for firing iff
$m\geq\prescript{\bullet}{}{t}$. We denote the _firing_ of $t$ by
$m\xrightarrow{t}m^{\prime}$, where $m^{\prime}$ is the resulting marking
after firing $t$ and is defined by
$m^{\prime}=m-\prescript{\bullet}{}{t}+t^{\bullet}$. For a transition sequence
$\sigma=\langle t_{1},\dots,t_{n}\rangle$ we write
$m\xrightarrow{\sigma}m^{\prime}$ to denote the consecutive firing of $t_{1}$
to $t_{n}$. We say that $m^{\prime}$ is reachable from $m$ and write
$m\xrightarrow{*}m^{\prime}$ if there is some $\sigma\in T^{*}$ such that
$m\xrightarrow{\sigma}m^{\prime}$.

$\mathcal{M}(N)=P^{\oplus}$ and it denotes the set of all markings in net $N$
and $\mathcal{R}(N,m)$ the _set of markings reachable_ in net $N$ from marking
$m$.

###### Definition 6

(Place invariant) Let $N=(P,T,\mathcal{F},\ell)$ be a Petri net. A _place
invariant_ [14] is a row vector $I:\bf{P}\rightarrow\mathbb{Q}$ such that
$I\cdot\bf{F}=0$, with $\bf{P}$ and $\bf{F}$ vector representations of $P$ and
$\mathcal{F}$. We denote the set of all place invariants as $\mathcal{I}_{N}$,
which is a linear subspace of $\mathbb{Q}^{P}$.

The main property of a place invariant $I$ in a net $N$ with initial marking
$m_{i}$ is that $\forall_{m_{1},m_{2}\in\mathcal{R}(N,m_{i})}I\cdot
m_{1}=I\cdot m_{2}$.

###### Definition 7

(Net system, Execution poset and sequence, Language) A _net system_ is a tuple
$SN=(N,m_{i},m_{f})$, where $N$ is a (labeled) Petri net, and $m_{i}$ and
$m_{f}$ are respectively the initial and final marking. An _execution
sequence_ in a net system $SN=(N,m_{i},m_{f})$ is a firing sequence from
$m_{i}$ to $m_{f}$. Additionally, an _execution poset_ is a poset of
transition firings, where each totally ordered permutation is a firing
sequence. The _language_ of a net system $SN$ is the set of all execution
sequences in $SN$.

###  2.3 Event logs

An event log records activity executions as events including at least the
occurred activity, the time of occurrence and the case identifier of the
corresponding case. Often resources are also recorded as event attributes,
e.g., the actors executing the action. It is generally known beforehand in
which activities specific _resource roles_ $R$ are involved and which resource
instances $\textnormal{Id}_{r}$ are involved in the process for each role
$r\in R$. We assume that each resource has only one role (function) allowing
to execute a predefined number of tasks, and therefore define the set
$\textnormal{Id}_{R}$ of resource instances of all roles as the disjoint union
of resource instance sets of roles: $\textnormal{Id}_{R}=\uplus_{r\in
R}\textnormal{Id}_{r}$. A _resource instance_ $\rho\in\textnormal{Id}_{R}$
with role $r\in R$ is equipped with capacity, making $\textnormal{Id}_{r}$ and
$\textnormal{Id}_{R}$ both multisets.

###### Definition 8

(Event, Event log, Trace) An _event_ $e$ is a tuple
$(a,t,c,\textnormal{Id}_{R}^{\prime})$, with an _activity_
$a=\operatorname{activity}(e)\in\Sigma$, a _timestamp_
$t=time(e)\in\mathbb{R}$, a _case identifier_
$c=\operatorname{case}(e)\in\textnormal{Id}_{c}$ and a multiset of resource
instances
$\textnormal{Id}_{R}^{\prime}=\operatorname{Res}(e)\leq\textnormal{Id}_{R}$.
Such an event represents that activity $a$ occurred at timestamp $t$ for case
$c$ and is executed by resource instances from $\textnormal{Id}_{R}^{\prime}$
belonging to possibly different resource roles.

An _event log_ $L$ is a set of events with partial order $\prec_{L}$ that
respects the chronological order of the events, i.e., $\forall_{e_{1},e_{2}\in
L}time(e_{1})<time(e_{2})\Longrightarrow e_{2}\not\prec_{L}e_{1}$. An event
log can be partitioned into _traces_ , defined as projections e.g., on the
case identifiers or on the resources names. For every
$c\in\textnormal{Id}_{c}$, $L_{c}$ denotes a trace projected on the case
identifier $c$ defined by $L_{c}=(\\{e\mid e\in
L,\operatorname{case}(e)=c\\},\prec_{L_{c}})$ with
$\prec_{L_{c}}=\\{(e,e^{\prime})\mid(e,e^{\prime})\in\prec_{L},\operatorname{case}(e)=\operatorname{case}(e^{\prime})=c\\}$.

Alternatively, we write $\langle e_{1},e_{2},\cdots\rangle$ for an event log
which is totally ordered, and $a^{\textnormal{Id}_{R}^{{}^{\prime}}}$ and
${\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{a\mathstrut}}^{\textnormal{Id}_{R}^{{}^{\prime}}}$
for events where the case is identified by the activity color (and bar
position) and the time of occurrence is abstracted away from.

For a (labeled) Petri net modeling a process, the transitions’ names or labels
correspond to the activity names found in the recorded event log.

##  3 Modeling, analysis and simulation of case handling systems with inter-
case dependencies

A classical Petri net models a process execution using transition firings and
the corresponding changes of markings without making distinctions between
different cases on which the modeled system works simultaneously. To create a
case view, Workflow nets [2] model processes from the perspective of a single
case. Systems in which cases interact with each other, e.g., by queueing or
sharing resources, need to be modeled in a different way. We show from a
modeling point how this boils down to multiple cases competing over shared
tokens representing resources in a Petri net, which requires an extension on
the formalism of the classical Petri nets. In Sec. 3.1, we motivate the
requirements by providing examples, after which, in Sec. 3.2, we discuss
whether existing Petri net extensions satisfy these requirements. We end, in
Sec. 3.3 by proposing a _minimal extension_ based on $\nu$-Petri nets [22]
that meets each requirement for simulation and analysis of resource-
constrained processes.

###  3.1 Requirements imposed by inter-case dependencies

When modeling systems with inter-case dependencies, i.e., shared resources,
simultaneous cases can interfere in each other’s processing via the resources,
causing inter-case dependencies. To model, simulate and analyze such behavior,
the cases and resources, represented as tokens in a Petri net, should be
handled together and simultaneously in the process model. This introduces the
need for case (R1) and resource isolation (R2) as well as durable resources
(R3) and case-resource correlations (R4), which regular Petri nets are not
capable of. For analysis, like computing alignments (see Section 4), non-
invertible functions can cause state-space explosions (R5). We show for each
requirement, when not satisfied, how simulation and/or analysis concerning
multiple simultaneous cases fails:

Figure 1: Example Petri net $N_{1}$ to argue the requirements, with token
colors denoting different instances.

  * R1

_Distinguishable cases_ are required when dealing with multiple cases. Tokens
involved in a firing of a transition should not belong to different cases,
unless case batching is used. Mixing tokens from different cases, possible in
classical Petri nets, can potentially cause model behavior that is not
possible in the modeled system: Suppose we have a simple operation process
modeled by Petri net $N_{1}$, shown in Fig. 1, where a patient undergoes an
operation involving the activities of preparation $(o_{p})$, assistance
$(o_{a})$, closed surgery $(o_{sc})$ and open surgery $(o_{so})$ which is
followed by closeup $(o_{c})$. We assume case tokens to be indistinguishable.
The language of $(N_{1},[p_{i},2p_{s}],[p_{f},2p_{s}])$ is $\\{\langle
o_{p},o_{a},o_{sc}\rangle,\langle o_{p},o_{sc},o_{a}\rangle,\langle
o_{p},o_{a},o_{so},o_{c}\rangle,$
$\langle o_{p},o_{so},o_{a},o_{c}\rangle\\}$ and the language of the same net
processing two cases with sufficient resources has to consist of all possible
interleaving of two traces belonging to single cases. However, $\\{\langle
o_{p},o_{a},o_{sc},{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{o_{p}\mathstrut}},{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{o_{a}\mathstrut}},{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{o_{so}\mathstrut}},\mathbf{o_{c}}\rangle\\}$
is included in the language of $(N_{1},[2p_{i},2p_{s}],[2p_{f},2p_{s}])$,
which is impossible to obtain by an interleaving of two single cases, as
$o_{c}$ is never enabled after $o_{sc}$ fires. Here and later we use
underlined symbols when referring to the second case in examples. From now on,
we assume case tokens are distinguishable and we have
$m_{i}(p_{i})=(c,{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{c\mathstrut}})$;

  * R2

_Distinguishable resources_ are required when resource instances are uniquely
identifiable. If the tokens in $p_{s}$ are indistinguishable,
$\langle\dots,o_{so}^{\\{x\\}},{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{o_{sc}\mathstrut}}^{\\{x\\}},o_{c}^{\\{x\\}}\rangle$
belongs to the language of $(N_{1},[2p_{i},2p_{s}],[2p_{f},2p_{s}])$. However,
resource instance $x$ can only be claimed by the second case after it has been
released by the first case (by firing transition $o_{c}$), hence it should not
be included in the language. From now on, we assume resource tokens are
distinguishable and we have $m_{i}(p_{s})=(x,y)$;

  * R3

Resources are required to be _durable_ when having a variable number of cases
in the system simultaneously. In $N_{1}$, the resource instances in $p_{s}$
are modeled to be durable, since these instances are always released after
being claimed. However, were arc $(o_{c},p_{s})$ to be removed, problems arise
when observed behavior concerns more than two cases, since after transition
$o_{so}$ fired twice, it is never enabled again, causing a deadlock;

  * R4

Capturing _case-resource correlation_ is required when dealing with multiple
distinguishable cases and resources in order to keep track of which resource
handles which case. Without it, the language of
$(N_{1},[2p_{i},2p_{s}],[2p_{f},2p_{s}])$ includes e.g.,
$\langle\dots,o_{so}^{\\{x\\}},{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{o_{so}\mathstrut}}^{\\{y\\}},{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{o_{c}\mathstrut}}^{\\{x\\}},o_{c}^{\\{y\\}}\rangle$,
which is undesirable as resources $x$ and $y$ have switched cases after
transition $o_{so}$ is fired twice. Case-resource correlation should ensure,
in this case, that transition $o_{c}$ can only be fired using the same
resource as was claimed by firing transition $o_{so}$;

  * R5

Operations on token values (e.g., guards, arc inscriptions) should be
_invertible_ and computable when aligning observed and modeled behavior in
order to keep the problem decidable. Consider e.g., that patients enter the
process by their name and birthdate $v$, which is transformed to an identifier
$c$ in the first transition by an operation $f(v)$ on $(o_{p})$. When activity
$o_{p}$ is missing for a patient, it is undecidable which value $v$ should be
inserted for the firing of $o_{p}$ when $f$ is not invertible.

###  3.2 Existing Petri net extensions

Several extensions on Petri nets have been proposed focusing on multi-case
and/or multi-resource processes able to handle (some) inter-case dependencies.
We go over each extension, describing how they satisfy (and violate)
requirements listed in Sec. 3.1. We propose an extension, which combines
concepts of the described extensions and satisfies all requirements.

_Resource constrained workflow nets_ (RCWF-nets) [12] are Petri nets extended
with resource constraints, where resources are durable units: they are claimed
and then released again (R3). They define structural criteria for its
correctness.

###### Definition 9

(Resource-constrained workflow net [12]) Let $R$ be a set of _resource roles_.
A net system $N=(P_{p}\uplus
P_{r},T,\mathcal{F}_{p}\uplus\mathcal{F}_{r},m_{i},m_{f})$ is a _resource-
constrained workflow net (RCWF-net)_ with the set $P_{p}$ of _production
places_ and the set $P_{r}=\\{p_{r}\mid r\in R\\}$ of _resource places_ iff

  * •

$\mathcal{F}_{p}:(P_{p}\times T)\cup(T\times P_{p})\rightarrow\mathbb{N}$ and
$\mathcal{F}_{r}:(P_{r}\times T)\cup(T\times P_{r})\rightarrow\mathbb{N}$;

  * •

$N_{p}=(P_{p},T,\mathcal{F}_{p},[m_{i}(p)\cdot p\mid p\in
P_{p}],[m_{f}(p)\cdot p\mid p\in P_{p}])$ is a net system, called the
production net of $N$.

The semantics of Petri nets is extended by having colored tokens on production
places (R1) and as resources are shared across all cases, tokens on resource
places are colorless ($\neg$R2, $\neg$R4). A transition is enabled if and only
if there are sufficient tokens on its incoming places using tokens of the same
color on production places.

_$\nu$ -Petri nets_ [22] are an extension of Petri nets with pure name
creation and name management, strictly surpassing the expressive power of
regular Petri nets and they essentially correspond to the minimal object-
oriented Petri nets of [13]. In a $\nu$-Petri net, names can be created,
communicated and matched which can be used to deal with authentication issues
[23], correlation or instance isolation [9]. Name management is formalized by
replacing ordinary tokens by distinguishable ones, thus adding color the the
Petri net.

###### Definition 10

($\nu$-Petri net [22]) Let $\mathit{Var}$ be a fixed set of variables. A
_$\nu$ -Petri net_ is a tuple $\nu\textit{-}\mathit{N}=\langle
P,T,\mathcal{F}\rangle$, with a set of places $P$, a set of transitions $T$
with $P\cap T=\emptyset$, and a flow function $\mathcal{F}:(P\times
T)\cup(T\times P)\rightarrow\mathit{Var}^{\oplus}$ such that $\forall_{t\in
T}$,
$\Upsilon\cap\prescript{\bullet}{}{t}=\emptyset\;\wedge\;t^{\bullet}\setminus\Upsilon\subseteq\prescript{\bullet}{}{t}$,
where $\prescript{\bullet}{}{t}=\bigcup\limits_{p\in P}supp(\mathcal{F}(p,t))$
and $t^{\bullet}=\bigcup\limits_{p\in P}supp(\mathcal{F}(t,p))$.
$\Upsilon\subset\mathit{Var}$ denotes a set of special variables ranged by
$\nu,\nu_{1},\dots$ to instantiate fresh names.

A marking of $\nu\textit{-}\mathit{N}$ is a function
$m:P\rightarrow\mathit{Id}^{\oplus}$. $\mathit{Id}(m)$ denotes the set of
names in $m$, i.e. $\mathit{Id}(m)=\bigcup\limits_{p\in P}supp(m(p))$.

A mode $\mu$ of a transition $t$ is an injection
$\mu:\mathit{Var}(t)\rightarrow\mathit{Id}$, that instantiates each variable
to an identifier.

For a firing of transition $t$ with mode $\mu$, we write
$m\xrightarrow{t_{\mu}}m^{\prime}$. $t$ is enabled with mode $\mu$ if
$\mu(\mathcal{F}(p,t))\subseteq m(P)$ for all $p\in P$ and
$\mu(\nu)\notin\mathit{Id}(m)$ for all
$\nu\in\Upsilon\cap\mathit{Var}(t)=supp(\cup_{p\in P}\mathcal{F}(p,t))$. The
reached state after the firing of $t$ with mode $\mu$ is the marking
$m^{\prime}$, given by:

$m^{\prime}(p)=m(p)-\mu(\mathcal{F}(p,t))+\mu(\mathcal{F}(t,p))\text{ for all
}p\in P$ (1)

We denote $T_{\mu}$ to be the set of all possible transition firings.

$\nu$-Petri nets support instance isolation for cases and resources requiring
the tokens involved in a transition firing to have matching colors (R1, R2).
Due to the tokens having singular identifiers, correlation between cases and
resources can not be captured ($\neg$R4).

_Resource and instance-aware workflow nets_ (RIAW-nets) [18], are Petri nets
combining the notions from above by defining similar structural criteria for
handling resource constraints on top of $\nu$-Petri nets. However, the
resource places are assumed to only carry black tokens, not allowing for
resource isolation and properly capturing the case-resource correlation.

_Synchronizing proclets_ [10] are a type of Petri net that describe the
behavior of processes with many-to-many interactions: unbounded dynamic
synchronization of transitions, cardinality constraints limiting the size of
the synchronization, and history-based correlation of token identities
(R1,R2). This correlation is captured by message-based interaction, specifying
attributes of a message as correlation attributes (R4). The correlation
constraints are $C_{init}$, $C^{\subseteq}_{match}$ and $C^{=}_{match}$, for
initializing the attributes, partially and fully matching them. $\nu$-Petri
nets are at the basis of proclets handling multiple objects by separating
their respective subnets. While the proclet formalism is sufficient for
satisfying all requirements listed above, they extend to many-to-many
relations, which lifts the restriction that a resource can only be claimed by
a single case.

_Object-centric Petri nets_ [4], similarly to synchronizing proclets, describe
the behavior of processes with multiple perspectives and one-to-many and many-
to-many relations between the different object types. These nets are a
restricted variant of colored Petri nets where places are typed, tokens are
identifiable referring to objects (R1,R2), and transitions can consume and
produce a variable number of tokens. Correlation can be achieved with
additional places of combined types (R4). Again, due to many-to-many
relations, our one-to-many restriction on resources is lifted.

_Database Petri nets_ (DB-nets) [19] are extensions of $\nu$-Petri nets with
multi-colored tokens that allows for multiple types of objects and their
correlation (R1,R2,R4). Additionally, they support underlying read-write
persistent storage consisting of a relational database with full-fledged
constraints. Special “view” places in the net are used to inspect the content
of the underlying data, while transitions are equipped with database update
operations. These are in the general sense not invertible causing
undecidability ($\neg$R5).

_Catalog Petri nets_ (CLog-nets) [11] are similar to DB-nets, but without the
“write” operations (R1,R2,R4). The queries from view places in DB-nets have
been relocated to transition guards, relying solely on the “read-only”
modality for a persistent storage, however suffering from the same
undecidability problem as these guards are not invertible in the general sense
($\neg$R5).

###  3.3 Resource constrained $\nu$-Petri net with fixed color types

We combine conceptual ideas from the extensions described above, by extending
RIAW-nets, which inherit the modeling restrictions from RCWF-nets and name
management from $\nu$-Petri nets, using concepts from DB-nets and CLog-nets.

The resource places from RCWF-nets model the availability of resource
instances by tokens, which is insufficient to capture correlation of cases by
which they are claimed and released. We propose a minimal extension _resource
constrained $\nu$-Petri nets_ (RC $\nu$-net) which additionally contain busy
places $\bar{P}_{r}=\\{\bar{p}_{r}\mid r\in R\\}$ for each resource role.
Token moves from $p_{r}$ to $\bar{p}_{r}$ show that the resource gets
occupied, and moves from $\bar{p}_{r}$ to $p_{r}$ show that the resource
becomes available. Also tests whether there are free/occupied resources can be
modeled. A structural condition is imposed on the net to guarantee that
resources are _durable_ , meaning that resources can neither be created nor
destroyed. This also implies that in the corresponding net system with initial
and final marking $m_{i}$ and $m_{f}$, $m_{i}(p_{r})=m_{f}(p_{r})$ and
$m_{i}(\bar{p}_{r})=m_{f}(\bar{p}_{r})$, for any resource role $r\in R$.

Furthermore, similar to DB-nets and CLog-nets, we extend the tokens from
carrying single data values to multiple. Where DB-nets and CLog-nets allow for
a variable number of predefined color types, we restrict ourselves to two
which are strictly typed, to distinguish between both cases and resources.

###### Definition 11

(Resource-constrained $\nu$-Petri net) Let $C^{\varepsilon}$ be the set of
case ids $\textnormal{Id}_{c}$ extended with ordinary tokens, i.e.,
$\varepsilon\in\textnormal{Id}_{c}$, and $\textnormal{Id}_{R}^{\varepsilon}$
be the set of resource ids extended with ordinary tokens. A _resource-
constrained $\nu$-Petri net_ $N=(P,T,\mathcal{F},m_{i},m_{f})$ is a Petri net
system with $\mathcal{F}:(P\times T)\cup(T\times
P)\rightarrow(\mathit{Var}^{\varepsilon}_{c}\times\mathit{Var}^{\varepsilon}_{r})^{\oplus}$,
where $\mathit{Var}_{c}$ denote case variables and $\mathit{Var}_{r}$ denote
resource variables, allowing for two colored tokens. $P=(P_{p}\uplus
P_{r}\uplus\bar{P}_{r})$, with production places $P_{p}$ and resource
availability and busy places $P_{r}=\\{p_{r}\mid r\in R\\}$ and
$\bar{P}_{r}=\\{\bar{p}_{r}\mid r\in R\\}$. The following modeling
restrictions are imposed on $N$ for each $r\in R$:

  1. 1.

$\prescript{\bullet}{}{p_{r}}+\prescript{\bullet}{}{\bar{p}_{r}}=p_{r}^{\bullet}+\bar{p}_{r}^{\bullet}$,
i.e., $\forall_{t\in
T}~{}\mathcal{F}(p_{r},t)+\mathcal{F}(\bar{p}_{r},t)=\mathcal{F}(t,p_{r})+\mathcal{F}(t,\bar{p}_{r})$;

  2. 2.

$m_{i}(p_{r})=m_{f}(p_{r})$ and $m_{i}(\bar{p}_{r})=m_{f}(\bar{p}_{r})=0$;

A marking of $N$ is a function $m:P\rightarrow(C^{\varepsilon}\times
R^{\varepsilon})^{\oplus}$ with case ids $C$ and resources $R$, which is a
mapping from places to multisets of colored tokens.

A mode of a transition $t$ is an injection
$\mu:(\mathit{Var}^{\varepsilon}_{c}\times\mathit{Var}^{\varepsilon}_{r})(t)\rightarrow(C^{\varepsilon}\times
R^{\varepsilon})$, that instantiates each variable to an identifier.

###### Proposition 1

The resource-constrained $\nu$-Petri nets as defined in Def. 11 satisfy
requirements R1-R5, i.e., they allow to _distinguish cases_ and _resource
instances_ which are _durable_ , and capture _case-resource correlation_ while
restricting to operations that are _invertible_.

###### Proof

The two-colored strictly typed tokens distinguish both the cases (R1) and
resource instances (R2) in the system. The modeling restrictions imposed on
the RC $\nu$-net enforce that for each resource role $r\in R$, tokens can only
move between $p_{r}$ and $\bar{p}_{r}$, i.e., we have the place invariant
$(1,1)$ on $p_{r}$ and $\bar{p}$, implying that
$m(p_{r})+m(\bar{p}_{r})=m_{i}(p_{r})$ for any reachable marking $m$, and that
all resource tokens are returned to $p_{r}$ when the net reaches its final
marking, ensuring that resources are durable (R3). The two colors on tokens
residing in $\bar{p}$ capture correlation between cases and resources
instances (R4), denoting by which case a resource instance is claimed
throughout their interaction. As the transition firing’s modes are bijective
functions, each operation on $N$ is invertible (R5). ∎

Note that the RC $\nu$-net formalism is a restricted version of DB-nets, CLog-
net and synchronizing proclets, as all three can capture the behavior that can
be modeled by RC $\nu$-nets. DB-nets and CLog-nets additionally have database
operations which we deem not relevant for our purposes. Synchronizing proclets
allow for many-to-many interactions, while we assume that a resource instance
cannot be shared by several cases at the same time.

##  4 Complete event logs alignments

Several state-of-the-art techniques in conformance checking use alignments to
relate the recorded executions of a process with a model of this process [5].
An alignment shows how a log or trace can be replayed in a process model,
which can expose deviations explaining either how the process model does not
fit reality or how the reality differs from what should have happened.

Traditionally, this is computed for individual traces, however, as we show in
previous work [24], this fails to expose deviations on a multi-case and
-resource level in processes with inter-case dependencies as described in Sec.
3.3. In this section, we go over the foundations of alignments in Sec. 4.1 and
show how we extend this to compute alignments of complete event logs in
Sec.4.2.

###  4.1 Foundations of alignments

At the core of alignments are three types of moves: log, model, and
synchronous moves (cf. Def. 12), indicating, respectively, that an activity
from the log can not be mimicked in the process model, that the model requires
the execution of some activity not observed in the log, and that observed and
modeled behavior of an activity agree.

###### Definition 12

(Log, model and synchronous moves) Let $L$ be an event log and
$N=(P,T,\mathcal{F},\ell,m_{i},m_{f})$ be a labeled $\nu$-Petri net with
$T_{\mu}$ the set of all possible firings in $N$. We define the set of log
moves $\Gamma_{l}=\\{(e,\gg)\mid e\in L\\}$, the set of model moves
$\Gamma_{m}=\\{(\gg,t_{\mu})\mid t_{\mu}\in T_{\mu}\\}$ and the set of
synchronous moves $\Gamma_{s}=\\{(e,t_{\mu})\mid e\in L,t_{\mu}\in
T_{\mu},\operatorname{activity}(e)=\ell(t)\\}$. As abbreviations, we write
$\Gamma_{ls}=\Gamma_{l}\cup\Gamma_{s}$,
$\Gamma_{lm}=\Gamma_{l}\cup\Gamma_{m}$,
$\Gamma_{ms}=\Gamma_{m}\cup\Gamma_{s}$, and
$\Gamma_{lms}=\Gamma_{l}\cup\Gamma_{m}\cup\Gamma_{s}$.

Log moves and model moves can expose deviations of the real behavior from the
model, by an _alignment_ (cf. Def. 13) on a net $(N,m_{i},m_{f})$ and event
log $L$ (possibly a single trace) which is a poset of moves from Def. 12
incorporating the event log and execution sequences in $N$ from $m_{i}$ to
$m_{f}$:

###### Definition 13

(Alignment) An _alignment_ $\gamma=\operatorname{align}(N,L)$ of an event log
$L=(\bar{L},\prec_{L})$ and a labeled Petri net
$N=(P,T,\mathcal{F},\ell,m_{i},m_{f})$ is a poset
$\gamma=(\bar{\gamma},\prec_{\gamma})$, where
$\bar{\gamma}\subseteq(\Gamma_{l}\cup\Gamma_{s}\cup\Gamma_{m}^{\oplus})$,
having the following properties:

  1. 1.

$\overline{\gamma{\upharpoonright}_{L}}=\bar{L}$ and
$\prec_{L}\subseteq\prec_{\gamma{\upharpoonright}_{L}}$

  2. 2.

$m_{i}\xrightarrow{\gamma{\upharpoonright}_{T}}m_{f}$, i.e.,
$\forall_{\sigma\in(\gamma{\upharpoonright}_{T})^{<}},m_{i}\xrightarrow{\sigma}m_{f}$

with alignment projections on the log events $\gamma{\upharpoonright}_{L}$ and
on the transition firings $\gamma{\upharpoonright}_{T_{\mu}}$:

$\displaystyle\gamma{\upharpoonright}_{L}$
$\displaystyle=\left(\left\\{e\mid(e,t_{\mu})\in\gamma\cap\Gamma_{ls}\right\\},\left\\{(e,e^{\prime})\mid((e,t_{\mu}),(e^{\prime},t^{\prime}_{\mu}))\in\prec_{\gamma}\cap(\Gamma_{ls}\times\Gamma_{ls})\right\\}\right)$
(2) $\displaystyle\gamma{\upharpoonright}_{T}$
$\displaystyle=\left(\left\\{t_{\mu}\mid(e,t_{\mu})\in\gamma\cap\Gamma_{ms}\right\\},\left\\{(t_{\mu},t^{\prime}_{\mu})\mid((e,t_{\mu}),(e^{\prime},t^{\prime}_{\mu}))\in\prec_{\gamma}\cap(\Gamma_{ms}\times\Gamma_{ms})\right\\}\right)$
(3)

Note the slight difference in the definition of an alignment as opposed to our
previous work in [24], where the alignment is simplified from a distributed
run to a poset of moves. The process’s history of states (markings) as it has
supposedly happened in reality can be extracted from the alignment. For the
general case, we introduce the _pseudo-firing_ of transitions from
corresponding alignment’s non-log moves in the process model, to obtain a
pseudo-marking, which can be unreachable or contain a negative number of
tokens:

###### Definition 14

(Pseudo-markings) A _pseudo-marking_ $m$ of a Petri net $N=(P,T,\mathcal{F})$
is a multiset $P\rightarrow\mathbb{Z}$, i.e., the assigned number of tokens a
place contains can be negative. $\widetilde{\mathcal{M}}(N)$ denotes the set
of all pseudo-markings in $N$.

###### Definition 15

(Pseudo-firing of posets) Let $N=(P,T,\mathcal{F},m_{i},m_{f})$ be a RC
$\nu$-net and $\gamma$ be an alignment on $N$. We define a function
$\widetilde{m}:\mathcal{P}(\gamma)\rightarrow\widetilde{\mathcal{M}}(N)$, with
powerset $\mathcal{P}$, to obtain the model pseudo-marking of every subposet
of $\gamma$. For every subposet $\gamma^{\prime}\subseteq\gamma$, we have for
every $p\in P$:

$\widetilde{m}(\gamma^{\prime})(p)=m_{i}(p)+\sum_{(e,t_{\mu})\in\gamma^{\prime}:t_{\mu}\neq\epsilon}\left(\mu\left(\mathcal{F}(t,p)\right)-\mu\left(\mathcal{F}(p,t)\right)\right)$
(4)

i.e., the pseudo-marking is obtained by firing all the transitions of
$\gamma^{\prime}$ with corresponding modes. Note that it is not necessarily
reachable.

An antichain in an alignment denotes a possible point in time, and therefore a
state of the process. By pseudo-firing the respective (open) prefix of the
antichain, we obtain the corresponding _pre- (or post-)antichain marking_ :

###### Definition 16

(Pre- and post-antichain marking) Let $\gamma$ be an alignment and
$G\in\mathcal{A}(\gamma)$ an antichain in $\gamma$. The pre- (post-)antichain
marking defines the marking reached after the pseudo-firing of $(\bot,G)$
($(\bot,G]$), i.e., $\widetilde{m}((\bot,G))$ ($\widetilde{m}((\bot,G])$).

###  4.2 Alignments extended to include inter-case dependencies

The foundational work on constructing alignments is presented in [5] and it
relies on the synchronous product of the Petri net
$N=(P,T,\mathcal{F},\ell,m_{i},m_{f})$ modeling a process and a trace Petri
net
$N_{\sigma}=(P^{(\sigma)},T^{(\sigma)},\mathcal{F}^{(\sigma)},\ell^{(\sigma)},m_{i}^{(\sigma)},m_{f}^{(\sigma)})$
(a Petri net representation of a trace in the event log). The synchronous
product consists of the union of $N$ and $N_{\sigma}$, and a transition
$t_{s}$ for each pair of transitions $(t_{m},t_{l})\in T\times T^{(\sigma)}$
with
$\prescript{\bullet}{}{t_{s}}=\prescript{\bullet}{}{t_{m}}+\prescript{\bullet}{}{t_{l}}$
and $t_{s}^{\bullet}=t_{m}^{\bullet}+t_{l}^{\bullet}$, iff $t_{m}$ and $t_{l}$
share the same label and variables on the incoming arcs, i.e.,
$\ell(t_{m})=\ell^{(\sigma)}(t_{l})$ and $Var(t_{m})=Var(t_{l})$. The
alignment is then computed by a depth-first search on the synchronous product
net from $m_{i}+m_{i}^{(\sigma)}$ to $m_{f}+m_{f}^{(\sigma)}$ using the
$A^{*}$ algorithm, with the firings of transition from $T^{(\sigma)}$, $T$ and
$T^{(s)}$ corresponding to the log, model and synchronous moves from Def. 12
[5].

With $c:\Gamma_{lms}\rightarrow\mathbb{R}^{+}$ a cost function, usually
defined for each $(e,t_{\mu})\in\Gamma_{lms}$ as follows:

$c((e,t_{\mu}))=\begin{cases}0&(e,t_{\mu})\in\Gamma_{s}\\\
1&(e,t_{\mu})\in\Gamma_{lm}\wedge\ell(t)\neq\tau\\\
\epsilon&\ell(t)=\tau\end{cases}$ (5)

The _optimal alignment_ is an alignment $\gamma$ such that
$\sum_{g\in\gamma}c(g)\leq\sum_{g\in\gamma^{\prime}}c(g)$ holds for any
alignment $\gamma^{\prime}$, which prefers synchronous moves over model and
log moves. In terms of conformance checking and exposing realistic deviations,
the optimal alignment provides the “best” explanation for the relation between
observed and modeled behavior.

In Sec. 3.3, we have shown how a RC $\nu$-net is a Petri net formalism with
capability of modeling inter-case dependencies and suitability for conformance
checking. We extend the alignment problem in order to expose inter-case
deviations by adapting the synchronous product net to $\nu$-nets: an RC
$\nu$-net and the log $\nu$-net:

###### Definition 17

(Log $\nu$-Petri net) Given an event log $L$, a _log $\nu$-Petri net_
$N^{(L)}=(P^{(L)},T^{(L)},\mathcal{F}^{(L)},\ell^{(L)},m_{i}^{(L)},m_{f}^{(L)})$
is a labeled $\nu$-net constructed as follows. For every $e\in L$, we make a
transition $t_{e}\in T^{(L)}$ with $\ell^{(L)}(t)=\operatorname{activity}(e)$,
and for each resource instance $\rho_{r}\in supp(\operatorname{Res}(e))$ we
make a place $p\in P^{(L)}$ with $\prescript{\bullet}{}{p}=\emptyset$,
$\prescript{\bullet}{}{p}=[|\rho_{r}|\cdot t]$,
$\mathcal{F}^{(L)}(p,t)=[|\rho_{r}|\cdot(\varepsilon,r)]$ and
$m_{i}^{(L)}(p)((\varepsilon,\rho))=|\rho|$. Further, for every pair
$(e_{1},e_{2})\in\prec_{L}$, we make a place $p\in P^{(L)}$ with
$\prescript{\bullet}{}{p}=[t_{e_{1}}]$, $p^{\bullet}=[t_{e_{2}}]$ and

$\mathcal{F}^{(L)}(t_{e_{1}},p)=\mathcal{F}^{(L)}(p,t_{e_{2}})=\begin{cases}[(c,\varepsilon)]&\operatorname{case}(e_{1})=\operatorname{case}(e_{2})\\\
[(\varepsilon,\varepsilon)]&\text{otherwise}\end{cases}$ (6)

For every $e^{-}\in\min(L)$, we make a place $p^{-}\in P^{(L)}$ with
$\prescript{\bullet}{}{{p^{-}}}=\emptyset$, ${p^{-}}^{\bullet}=[t_{e^{-}}]$
and $m_{i}^{(L)}(p^{-})((case(e^{-}),\varepsilon))=1$. Similarly, for every
$e^{+}\in\max(L)$, we make a place $p^{+}\in P^{(L)}$ with
$\prescript{\bullet}{}{{p^{+}}}=[t_{e^{+}}]$, ${p^{+}}^{\bullet}=\emptyset$
and $m_{f}^{(L)}(p^{+})((case(e^{+}),\varepsilon))=1$.

Computing the _complete event log alignment_ is again a matter of finding a
path from the initial to the final marking in the synchronous product net,
i.e., from $m_{i}+m_{i}^{(L)}$ to $m_{f}+m_{f}^{(L)}$, for which we can use
_any_ of the existing methods as described before. The optimal alignment is
again the one with lowest cost. In terms of complexity, the alignment problem
with an empty event log and an all-zero cost function can be reduced to the
reachability problem for bounded Petri nets from $m_{i}$ to $m_{f}$, which has
exponential worst-case complexity[20]. Adding event to the log $\nu$-Petri net
and a non-zero costs on moves makes the problem strictly more complex.

Note that while $\nu$-Petri nets are inherently unbounded in general due to
the generation of fresh tokens, we can retain boundedness in the context of
alignments, since the bound is predicated by the event log and we can get this
information by preprocessing it.

Figure 2: Process model RC $\nu$-net $N$, with initial and final marking,
annotated with circular and square tokens respectively.

Figure 3: Event log $L$.

Figure 4: Complete event log alignment $\gamma$, with the colors depicting the
move types; green, purple, and yellow for synchronous, model, and log moves
respectively.

Figure 5: Composed alignment ${\widetilde{\gamma}}$ with annotated permutation
and realignment intervals.

Figure 6: Approximated alignment $\gamma^{*}$.

For our running example, modeled in Fig. 6, we extend the small operation
process from Fig. 1 with an assistant resource during the operation, an intake
subprocess $(i_{s},i_{p})$ involving a general practitioner (GP), and a
prescription subprocess with a FIFO waiting room $(p_{w},w_{e},w_{l},p_{r})$,
where the prescription can only be written by the GP involved in the intake,
if appropriate. Both the intake and operation subprocesses can be skipped via
silent transitions $\tau_{1}$ and $\tau_{3}$ respectively in $N$. Fig. 6 shows
the recorded event log $L$ of this process which concerns two patients. An
optimal complete event log alignment on $N$ and $L$, computed by the method
above is presented in Fig. 6.

##  5 Approximation by composition and local realignments

Since multiple cases are executed in parallel, computing the alignment on the
complete event log $L$, as described in Section 4, is a computationally
expensive task. At the same time, one can see that the multi-case and
-resource alignment only deviates from the classical individual alignments
when violations occur on the inter-case dependencies, e.g., when a resource is
claimed while it is already at maximal capacity.

Figure 7: Overview of our approximation method.

We can approximate the alignment of a complete event log $L$ and a Petri net
$N$ by using a composition of individually aligned cases. An overview of this
method is illustrated in Fig. 7, which we subdivide into two parts, described
respectively in Sec. 5.1 and 5.2.

  1. 1.

$L$ is decomposed into the individual cases
($L_{c},L_{{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{c\mathstrut}}}$),
which are aligned to $N$
($\gamma_{c},\gamma_{{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{c\mathstrut}}}$)
and composed using the event log’s partial order $\prec_{L}$
(${\widetilde{\gamma}}$). The result is not necessarily an alignment as inter-
case deviations may be left unresolved;

  2. 2.

We transform this composed alignment into a valid alignment by taking a
permutation (${\widetilde{\gamma}}^{\prime}$) and realigning parts
($[A_{1},B_{1}],[A_{2},B_{2}],[A_{3},B_{3}]$) of the event log locally to
resolve the violations. The approximated alignment ($\gamma^{*}$) is obtained
by substituting the realignments
($\gamma_{AB_{1}},\gamma_{AB_{2}},\gamma_{AB_{3}}$).

The implementation of both the original method from [24] and the approximation
method for computing complete event log alignments is available at
gitlab.com/dominiquesommers/mira, including the examples used in this paper
and some additional examples.

###  5.1 Composing individual alignments

For every case $c\in\textnormal{Id}_{c}$, we have the trace $L_{c}$ (cf. Def.
8) projected on the case identifier $c$. As described in Sec.4, the optimal
complete event log alignment $\gamma_{L}$ consists of individual alignments
$\gamma_{c}$, on $N$ and $L_{c}$ for every $c\in\textnormal{Id}_{c}$, composed
together respecting the event log’s partial order $\prec_{L}$, where each
$\gamma_{c}$ is not necessarily optimal with regard to $L_{c}$.

It is computationally less expensive to compute the optimal alignments
$\gamma_{c}=\operatorname{align}(N,L_{c})$ for each $c\in\textnormal{Id}_{c}$
and then approximate $\gamma_{L}$. We create a composed alignment
${\widetilde{\gamma}}$ with the optimal individual alignments and the event
log’s partial order, as defined in Def. 18. Fig.6 shows the composed alignment
for the running example with additional annotations (in red) which we cover
later.

###### Definition 18

(Composed alignment) Given a Petri net $N$ and an event log $L$ with traces
$L_{c}$ for $c\in\textnormal{Id}_{c}$, let
$\gamma_{c}=\operatorname{align}(N,L_{c})$ be the corresponding optimal
individual alignments. The _composed alignment_
${\widetilde{\gamma}}=\doublecup_{c\in\textnormal{Id}_{c}}\gamma_{c}$ is the
union of individual alignments with the extended partial order on the
synchronous moves, defined as the transitive closure of the union of partial
orders from the individual alignments and the partial order on moves imposed
by the partial order $\prec_{L}$ of the event log:

$\prec_{\widetilde{\gamma}}\;=\left(\bigcup_{c\in\textnormal{Id}_{c}}\prec_{\gamma_{c}}\cup\prec_{\gamma_{L}}\right)^{+}$
(7)

with
$\prec_{\gamma_{L}}=\left\\{\left((e,t_{\mu}),(e^{\prime},t^{\prime}_{\mu})\right)\mid
e\prec_{L}e^{\prime},(e,t_{\mu}),(e^{\prime},t^{\prime}_{\mu})\in(\gamma\cap\Gamma_{ls})\right\\}$.

Recall that for every sequence
$\sigma\in{\widetilde{\gamma}}{\upharpoonright}_{T}$ of an alignment
${\widetilde{\gamma}}$, we have $m_{i}\xrightarrow{\sigma}m_{f}$, i.e.,
$\sigma$ is a firing sequence in $N$. This property is not guaranteed for a
composed alignment, even in the absence of inter-case deviations. In the
presence thereof, we say that a composed alignment is _violating_ as there
exists no such sequence.

###### Definition 19

(Violating composed alignment) Let
$\rho_{r}\in\mathit{supp}(\textnormal{Id}_{R})$ be a resource instance and
${\widetilde{\gamma}}=\doublecup_{c\in\textnormal{Id}_{c}}\gamma_{c}$ a
composed alignment. We define

$\mathcal{S}({\widetilde{\gamma}})=\\{(\bar{\widetilde{\gamma}}^{\prime},\prec_{{\widetilde{\gamma}}^{\prime}})\mid\bar{\widetilde{\gamma}}=\bar{\widetilde{\gamma}}^{\prime},\prec_{\widetilde{\gamma}}\subseteq\prec_{{\widetilde{\gamma}}^{\prime}},\prec_{{\widetilde{\gamma}}^{\prime}}=(\prec_{{\widetilde{\gamma}}^{\prime}})^{+},\forall_{g\in{\widetilde{\gamma}}}g\nprec_{{\widetilde{\gamma}}^{\prime}}g\\}$
(8)

as the set of transitively closed and acyclic antichain permutations of
${\widetilde{\gamma}}$ that respect the partial order
$\prec_{\widetilde{\gamma}}$.

${\widetilde{\gamma}}$ is in violation with any of the resource instances if
and only if:

$\forall_{{\widetilde{\gamma}}^{\prime}\in\mathcal{S}({\widetilde{\gamma}})}\exists_{G\in\mathcal{A}^{+}({\widetilde{\gamma}}^{\prime})}\operatorname{viol}(G)$
(9)

with violation criteria
$\operatorname{viol}:\mathcal{A}^{+}({\widetilde{\gamma}})\rightarrow\mathbb{B}$
defined for each maximal antichain $G\in\mathcal{A}^{+}({\widetilde{\gamma}})$
as follows:

$\operatorname{viol}(G)=\exists_{\rho_{r}\in
supp(\textnormal{Id}_{R})}\left[\widetilde{m}((\bot,G))(p_{r})((\varepsilon,\rho_{r}))<\sum_{(e,t_{\mu})\in
G}\mathcal{F}(p_{r},t)(\mu^{-1}((\varepsilon,\rho_{r})))\right]$ (10)

i.e., there is no way of firing all transitions in the alignment such that at
all times enough capacity is available.

In Fig. 6, antichains meeting the violation criteria are the single moves with
an incoming red arc. In Theorem 5.1 we show that for every sequence of
transitions $\sigma\in{\widetilde{\gamma}}{\upharpoonright}_{T}$ in violating
composed alignment ${\widetilde{\gamma}}$, we have
$m_{i}\not\xrightarrow{\sigma}m_{f}$, i.e., ${\widetilde{\gamma}}$ is not
firable.

###### Theorem 5.1

(A violating composed alignment is not firable) Let
${\widetilde{\gamma}}=\doublecup_{c\in\textnormal{Id}_{c}}\gamma_{c}$ be a
composed alignment on RC $\nu$-net $N=(P,T,\mathcal{F},m_{i},m_{f})$ and event
log $L$, such that ${\widetilde{\gamma}}$ is violating. Then there exists no
firing sequence $\sigma$ in ${\widetilde{\gamma}}$ such that
$m_{i}\xrightarrow{\sigma}m_{f}$.

###### Proof

${\widetilde{\gamma}}$ is violating, therefore, for every
${\widetilde{\gamma}}^{\prime}\in\mathcal{S}({\widetilde{\gamma}})$, there is
a maximal antichain $G\in\mathcal{A}^{{+}}({\widetilde{\gamma}}^{\prime})$ and
resource instance $\rho_{r}\in supp(\textnormal{Id}_{R})$, such that

$\displaystyle\widetilde{m}((\bot,G))(p_{r})((\varepsilon,\rho_{r}))<\sum_{(e,t_{\mu})\in
G}\mathcal{F}(p_{r},t)(\mu^{-1}((\varepsilon,\rho_{r})))$ (11)
$\displaystyle\widetilde{m}((\bot,G))(p_{r})((\varepsilon,\rho_{r}))\>-\sum_{(e,t_{\mu})\in
G}\mathcal{F}(p_{r},t)(\mu^{-1}((\varepsilon,\rho_{r})))<0$ (12)

hence firing the transitions in $G$ leads to a negative marking for
$(\varepsilon,\rho_{r})$ in place $p_{r}$, which is invalid.∎

With an antichain $G\subseteq\mathcal{A}({\widetilde{\gamma}})$, we show in
Lemma 1 that $\widetilde{m}((\bot,G))$ (and $\widetilde{m}{(\bot,G]}$) is
reachable if an only if the prefix $(\bot,G)$ ($(\bot,G]$) is not violating.

###### Lemma 1

(A pre- (and post-)antichain marking in a composed alignment is reachable iff
the corresponding prefix is not violating.) Let
${\widetilde{\gamma}}=\doublecup_{c\in\textnormal{Id}_{c}}\gamma_{c}$ be a
composed alignment on RC $\nu$-net $N=(P,T,\mathcal{F},m_{i},m_{f})$ and event
log $L$ and let $G\in\mathcal{A}({\widetilde{\gamma}})$ be an antichain. Then
the pre- (and post-)antichain marking $\widetilde{m}((\bot,G))$
($\widetilde{m}((\bot,G])$) is reachable if and only if $(\bot,G)$
($(\bot,G]$) is not violating.

###### Proof

We prove the lemma by proving both sides of the bi-implication:

$(\implies)$ $m_{G}=\widetilde{m}((\bot,G))$ is reachable, hence there exists
a sequence $\sigma\in(\bot,G)^{*}$ with
$\prec_{(\bot,G)}\subseteq\prec_{\sigma}$ such that
$m_{i}\xrightarrow{\sigma}m_{G}$. Let
${\widetilde{\gamma}}^{\prime}\in\mathcal{S}({\widetilde{\gamma}})$ be an
antichain permutation with
$\prec_{\sigma}\subseteq\prec_{{\widetilde{\gamma}}^{\prime}}$. Then by
definition of reachable marking, for every maximal antichain
$G\in\mathcal{A}^{+}({\widetilde{\gamma}}^{\prime})$ and every resource
instance $\rho_{r}\in supp(\textnormal{Id}_{R})$, we have
$\widetilde{m}((\bot,G))(p_{r})((\varepsilon,\rho_{r}))\geq\sum_{(e,t_{\mu})\in
G}\mathcal{F}(p_{r},t)(\mu^{-1}((\varepsilon,\rho_{r})))$. Thus $(\bot,G)$ is
not violating.

$(\impliedby)$ $(\bot,G]$ is not violating, hence there exists a
${\widetilde{\gamma}}^{\prime}\in\mathcal{S}((\bot,G])$, such that for all
$G^{\prime}\in\mathcal{A}^{+}({\widetilde{\gamma}}^{\prime})$ and all $\rho\in
supp(\textnormal{Id}_{R})$ we have:

$\widetilde{m}((\bot,G))(p_{r})((\varepsilon,\rho_{r}))\geq\sum_{(e,t_{\mu})\in
G}\mathcal{F}(p_{r},t)(\mu^{-1}((\varepsilon,\rho_{r})))$ (13)

$m_{i}\xrightarrow{\sigma}\widetilde{m}((\bot,G])$ with $\sigma$ respecting
the partial order $\prec_{{\widetilde{\gamma}}^{\prime}}$. ∎

###  5.2 Resolving violations in the composed alignment

Let ${\widetilde{\gamma}}^{\prime}\in\mathcal{S}(\gamma)$ be an antichain
permutation of ${\widetilde{\gamma}}$. Then, by Def. 19, we have a set of
violating maximal antichains (which is empty when ${\widetilde{\gamma}}$ is
not violating) where the corresponding transitions are not enabled. Instead of
needing to align the complete event log, we show that we can resolve
violations locally around such antichain. For each violating antichain $G$,
there exists an interval $[A,B]\subseteq{\widetilde{\gamma}}^{\prime}$ with
$A\preceq G\preceq B$ such that $[A,B]$ is alignable, formally defined in Def.
20.

###### Definition 20

(Alignable interval) Let
$\gamma=\doublecup_{c\in\textnormal{Id}_{c}}\gamma_{c}$ be a composed
alignment on RC $\nu$-net $N=(P,T,\mathcal{F},m_{i},m_{f})$ and event log $L$,
and let $A,B\in\mathcal{A}(\gamma)$ be two antichains. We say that the
interval $[A,B]$ is alignable if and only if $m_{B}=\widetilde{m}((\bot,B])$
is reachable from $m_{A}=\widetilde{m}((\bot,A))$, i.e.,
$m_{A}\xrightarrow{*}m_{B}$, assuming $m_{A}$ is reachable.

Note that $[\min(\gamma^{\prime}),\max(\gamma^{\prime})]$ is always an
alignable interval. We use our running example to show that it can be taken
locally around $G$ instead, e.g.,
$[\\{{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{i_{s}\mathstrut}}\\},\\{i_{p}\\}]$
with
$G=\\{{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{i_{s}\mathstrut}}\\}$
(cf. Fig. 6). Note how the violation can be resolved by substituting $[A,B]$
by a subalignment from $m_{A}=\widetilde{m}((\bot,A))$ to
$m_{B}=\widetilde{m}((\bot,B])$.

In order to prove statements that do not depend on a chosen realignment
mechanism, we now assume that there exists a function
$f_{\widetilde{\gamma}}:\mathcal{A}^{+}({\widetilde{\gamma}})\rightarrow\mathcal{P}({\widetilde{\gamma}})$
that produces an alignable interval $[A,B]$ for an arbitrary
$G\in\mathcal{A}^{+}({\widetilde{\gamma}})$.

$\displaystyle
W({\widetilde{\gamma}}^{\prime}_{V})=\\{[\min(\gamma_{v}),\max(\gamma_{v})]\mid$
$\displaystyle~{}\gamma_{v}\subseteq{\widetilde{\gamma}}^{\prime}_{V},\forall_{g\in\gamma_{v},g^{\prime}\in{\widetilde{\gamma}}^{\prime}_{V}\setminus\gamma_{v}}g\|_{{\widetilde{\gamma}}^{\prime}_{V}}g^{\prime},$
(14)
$\displaystyle~{}\forall_{g\in\gamma_{v}}\exists_{g^{\prime}\in\gamma_{v}}g\not\|_{\gamma_{v}}g^{\prime}\\}$

with
${\widetilde{\gamma}}^{\prime}_{V}=\bigcup_{G\in\mathcal{A}^{+}({\widetilde{\gamma}}^{\prime})}f_{{\widetilde{\gamma}}^{\prime}}(G)$,
denotes the set of alignable intervals covering every violating antichain in
${\widetilde{\gamma}}^{\prime}$, and it is annotated in red for the running
example in Fig. 6, with the three intervals
$[\\{{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{i_{s}\mathstrut}}\\},\\{i_{p}\\}]$,
$[\\{{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{o_{p}\mathstrut}}\\},\\{o_{f}\\}]$,
and
$[\\{{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{w_{e}\mathstrut}}\\},\\{\tau\\}]$
covering the violating antichains
$\\{{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{i_{s}\mathstrut}}\\}$,
$\\{{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{o_{p}\mathstrut}}\\}$,
$\\{{\color[rgb]{0.93,0.53,0.18}\definecolor[named]{pgfstrokecolor}{rgb}{0.93,0.53,0.18}\underline{o_{so}\mathstrut}}\\}$,
and $\\{w_{e}\\}$.

We resolve the violations in ${\widetilde{\gamma}}^{\prime}$ by substituting
every interval $[A,B]\in W({\widetilde{\gamma}}^{\prime}_{V})$ by an alignment
$\gamma_{AB}$ on $N$ and $[A,B]{\upharpoonright}_{L}$ from
$m_{A}=\widetilde{m}((\bot,A))$ to $m_{B}=\widetilde{m}((\bot,B])$.

Since, for now, we assume that every interval $f(G)$ is alignable, a
subalignment $\gamma_{AB}$ exists. The approximated alignment
$\gamma^{*}=(\bar{\gamma}^{*},\prec_{\gamma^{*}})$ is then defined as follows:

$\displaystyle\bar{\gamma}^{*}$ $\displaystyle=\bigcup_{[A,B]\in
W({\widetilde{\gamma}}^{\prime}_{V})}\bar{\gamma}_{AB}\cup(\bar{\widetilde{\gamma}}\setminus\bar{\widetilde{\gamma}}^{\prime}_{V})$
(15) $\displaystyle\prec_{\gamma^{*}}$ $\displaystyle=\left(\bigcup_{[A,B]\in
W({\widetilde{\gamma}}^{\prime}_{V})}\prec_{\gamma_{AB}}\cup\left\\{(g_{1},g_{2})\mid
g_{1},g_{2}\in\gamma\setminus{\widetilde{\gamma}}^{\prime}_{V},g_{1}\prec_{{\widetilde{\gamma}}^{\prime}}g_{2}\right\\}\right)^{+}$
(16)

$\gamma^{*}$ for the running example is shown in Fig. 6 with substituted
realignments for the intervals annotated in red from Fig. 6. Note that
$\gamma^{*}$ is an approximation of the optimal alignment $\gamma$ from Fig. 6
as $c(\gamma^{*})\geq c(\gamma)$, due to the local realignments. In Theorem
5.2 we show that $\gamma^{*}$ is a valid alignment.

###### Theorem 5.2

($\gamma^{*}$ is an alignment.) Let
${\widetilde{\gamma}}=\doublecup_{c\in\textnormal{Id}_{c}}\gamma_{c}$ be a
composed alignment on RC $\nu$-net $N=(P,T,\mathcal{F},m_{i},m_{f})$ and event
log $L$ and let
${\widetilde{\gamma}}^{\prime}\in\mathcal{S}({\widetilde{\gamma}})$ be an
antichain permutation of ${\widetilde{\gamma}}$, with
$W({\widetilde{\gamma}}^{\prime}_{V})$ the set of alignable intervals covering
every violating antichain in ${\widetilde{\gamma}}^{\prime}$.

$\gamma^{*}=(\bar{\gamma}^{*},\prec_{\gamma^{*}})$, following Eqs. 15 and 16,
is a valid alignment, i.e., it has properties (1), (2) and (3) from Def. 13.

###### Proof

We prove that $\gamma^{*}$ is an alignment by induction on the size of
$W({\widetilde{\gamma}}^{\prime}_{V})$. For the base case with
$|W({\widetilde{\gamma}}^{\prime}_{V})|=0$, we have
$\bar{\gamma}^{*}=\bar{\widetilde{\gamma}}$ and
$\prec_{\gamma^{*}}=\prec_{{\widetilde{\gamma}}^{\prime}}$. By definition,
$\bar{{\widetilde{\gamma}}{\upharpoonright}_{L}}=\bar{L}$ and
$\prec_{L}\subseteq\prec_{{\widetilde{\gamma}}{\upharpoonright}_{L}}$.
Furthermore, since $|W({\widetilde{\gamma}}^{\prime}_{V})|=0$, we know that
for all $G\in\mathcal{A}^{+}({\widetilde{\gamma}}^{\prime})$, we have
$\neg\operatorname{viol}(G)$, implying that
$m_{i}\xrightarrow{{\widetilde{\gamma}}^{\prime}}m_{f}$.

Let us assume that $\gamma^{*}$ is an alignment for
$|W({\widetilde{\gamma}}^{\prime}_{V})|=w$. We prove the statement for
$W^{\prime}({\widetilde{\gamma}}^{\prime}_{V})=W({\widetilde{\gamma}}^{\prime}_{V})\cup\\{[A,B]\\}$
with $|W^{\prime}({\widetilde{\gamma}}^{\prime}_{V})|=w+1$ and
$[A,B]\in\min(W^{\prime}({\widetilde{\gamma}}^{\prime}_{V}))$. For every
maximal antichain $G\in\mathcal{A}^{+}((\bot,A))$ before $A$, i.e., $G\prec
A$, we have $\neg\operatorname{viol}(G)$, which we prove by contradiction.
Assume $\operatorname{viol}(G)$, then by our assumption of the existence of
$f_{{\widetilde{\gamma}}^{\prime}}$, there is an alignable interval
$[A^{\prime},B^{\prime}]\subseteq{\widetilde{\gamma}}^{\prime}$ with
$A^{\prime}\preceq G\preceq B^{\prime}$, thus, by $G\prec A$, we have
$[A^{\prime},B^{\prime}]\prec[A,B]$, implying that
$[A,B]\notin\min(W^{\prime}({\widetilde{\gamma}}^{\prime}))$ which is a
contradiction. By Lemma 1 and the assumption that
$f_{{\widetilde{\gamma}}^{\prime}}(G)$ is an alignable interval,
$m_{i}\xrightarrow{*}m_{A}\xrightarrow{*}m_{B}$ and $[A,B]$ can be substituted
by $\gamma_{AB}$ without violations in $(\bot,B]$, completing the proof. ∎

###  5.3 Obtaining minimal local alignable intervals

We propose a method to find an antichain permutation of a composed alignment
${\widetilde{\gamma}}$ together with the intervals
$W({\widetilde{\gamma}}_{V})$ such that all violations can be resolved by
realigning these intervals as described in Sec. 5.2. For computational
efficiency, we choose to minimize the number of moves in the intervals that
need to be realigned.

We formulate this as an Integer Linear Programming (ILP) problem. The
objective of the ILP problem is to adjust the partial order of
${\widetilde{\gamma}}$, such that alignable intervals can be identified around
violating antichains, preferring intervals with fewer moves.

Let there be a (possibly arbitrary) fixed order in ${\widetilde{\gamma}}$ and
$\textnormal{Id}_{R}$ such that each element has a unique index, i.e., for
every $1\leq i\leq n_{\widetilde{\gamma}}$, ${\widetilde{\gamma}}(i)$ and
$(e(i),t_{\mu}(i))$ both denote the $i^{\text{th}}$ move in
${\widetilde{\gamma}}$, with $n_{\widetilde{\gamma}}=|{\widetilde{\gamma}}|$.
Furthermore, for every $1\leq j\leq n_{r}$, $\textnormal{Id}_{R}(j)$ denotes
the $j^{\text{th}}$ resource instance, with
$n_{r}=|supp(\textnormal{Id}_{R})|$.

Let $\mathbf{R}$ be a $n_{\widetilde{\gamma}}\times n_{\widetilde{\gamma}}$
matrix, with $\mathbf{R}$ defined for every two indices $1\leq i,j\leq
n_{\widetilde{\gamma}}$ such that $\mathbf{R}_{ij}$ is a binary value denoting
$({\widetilde{\gamma}}(i),{\widetilde{\gamma}}(j))\in\prec_{{\widetilde{\gamma}}}$.
For each $c\in\textnormal{Id}_{c}$, we introduce the set $I_{c}$ of indices
corresponding to moves in
${\widetilde{\gamma}}{\upharpoonright}_{\gamma_{c}}$. Furthermore, we use
$[1..n]=\\{1,\dots,n\\}$ as an abbreviation for the set of all indices from 1
to $n$.

The set of minimal alignable intervals containing all violations, denoted by
$W({\widetilde{\gamma}}^{\prime}_{V})$, with
${\widetilde{\gamma}}^{\prime}_{V}$ given by

${\widetilde{\gamma}}^{\prime}_{V}=\bigcup_{i,j\in[1..n_{\widetilde{\gamma}}]:\mathbf{X}_{ij}-\mathbf{R}_{ij}=1}[{\widetilde{\gamma}}(j),{\widetilde{\gamma}}(i)]$
(17)

where $\mathbf{X}$ denotes the new partial order relation between alignment
moves which respects the resources capacities and provides the solution to

$\text{Minimize
}\sum_{i,j\in[1..n_{\widetilde{\gamma}}]}(1-\mathbf{R}_{ij})\mathbf{R}_{ji}\mathbf{X}_{ij}+\epsilon\cdot(1-\mathbf{R}_{ij})(1-\mathbf{R}_{ji})\mathbf{X}_{ij}$
(18)

subject to

$\displaystyle\forall_{i,j\in[1..n_{\widetilde{\gamma}}]}$
$\displaystyle\mathbf{X}_{ij}$ $\displaystyle\in\\{0,1\\}$ (19)
$\displaystyle\forall_{c\in\textnormal{Id}_{c}}\forall_{i,j\in I_{c}}$
$\displaystyle\mathbf{X}_{ij}$ $\displaystyle=\mathbf{R}_{ij}$ (20)
$\displaystyle\forall_{i,j\in[1..n_{\widetilde{\gamma}}]}$
$\displaystyle\mathbf{R}_{ij}+(1-\mathbf{X}_{ij})-\mathbf{X}_{ji}$
$\displaystyle\leq 1$ (21)
$\displaystyle\forall_{i,j,k\in[1..n_{\widetilde{\gamma}}]}$
$\displaystyle\mathbf{X}_{ij}+\mathbf{X}_{jk}-\mathbf{X}_{ik}$
$\displaystyle\leq 1$ (22)
$\displaystyle\forall_{i\in[1..n_{\widetilde{\gamma}}]}$
$\displaystyle(1-\mathbf{X}_{i\bullet})\mathbf{C}^{\downarrow}-\mathbf{X}_{\bullet
i}^{T}\mathbf{C}^{\uparrow}$ $\displaystyle\leq\mathbf{k}$ (23)

with $\mathbf{C}^{\downarrow}$ and $\mathbf{C}^{\uparrow}$ both
$n_{\widetilde{\gamma}}\times n_{r}$ matrices counting how many resource
instances are claimed and released respectively for every alignment move. Both
are defined for every $i\in[1..n_{\widetilde{\gamma}}]$ and $k\in[1..n_{r}]$
with $(e,t_{\mu})={\widetilde{\gamma}}(i)$ and
$\rho_{r}=\textnormal{Id}_{R}(k)$:

$\mathbf{C}^{\downarrow}_{ik}=\mathcal{F}(p_{r},t)((\varepsilon,\mu^{{-1}}(\rho_{r})))\text{
and
}\mathbf{C}^{\uparrow}_{ik}=\mathcal{F}(t,p_{r})((\varepsilon,\mu^{{-1}}(\rho_{r})))$
(24)

and capacity vector $\mathbf{k}$ of length $n_{r}$, defined as
$\mathbf{k}_{k}=|\textnormal{Id}_{R}(k)|$ for every $k\in[1..n_{r}]$.

$\mathbf{X}$ provides the solution of a new partial order of moves in
${\widetilde{\gamma}}$ such that all violations are resolved and the least
number of partial order relations is removed. For the running example, the
additional arcs from the solution $\mathbf{X}$ are shown in red in Fig. 6.

We refer to App. 0.A for the correctness proof of the ILP problem, where we
show (1) the effectiveness of each constraint, (2) that there always exists a
solution, (3) that the optimal solution has zero cost if and only if the
composed alignment is not violating, and (4) that each interval obtained in
$W({\widetilde{\gamma}}^{\prime}_{V})$ is alignable.

##  6 Conclusion

We have formulated the requirements for modeling and analyzing processes with
inter-case dependencies and argued that our previously proposed Petri net
extension named Resource Constrained $\nu$-Petri nets meets them. This paper
continues on work presented in [24], where we showed that the traditional
methods of aligning observed behavior with the modeled one fall short when
dealing with coevolving cases, as they consider isolated cases only. The
technique we present here aligns multiple cases simultaneously, exposing
violations on inter-case dependencies. We developed and implemented an
approximation technique based on a composition of individual alignments and
local resolution of violations, which is an important advancement for the use
of the technique in practice.

There can be ambiguity in the interpretation of the exposed violations, e.g.,
was the activity executed but not recorded, executed by an “incorrect”
resource instance, or not executed at all? In [24], we briefly touched upon
relaxations of the synchronous product model as a means to improve the
deviations’ interpretability. One such relaxation helps to detect situations
when a step required by the model was skipped in a process execution, and the
resources needed for the step were not available at the time when it should
have been executed. Adding “resource-free” model moves for transitions allows
to capture such deviations. Such special moves, when present in the alignment,
reduce the ambiguity and provide a better explanation, e.g., that the activity
was not executed at all, rather than it might also have been executed but not
recorded. For future work, we plan to extend and formalize the relaxations,
and evaluate the insights obtained with the alignments based on a real-life
case study.

####  6.0.1 Acknowledgments.

This work is done within the project “Certification of production process
quality through Artificial Intelligence (CERTIF-AI)”, funded by NWO (project
number: 17998).

## References

  * [1] Wil M.P. van der Aalst.  The application of Petri nets to workflow management.  Journal of circuits, systems, and computers, 8(01):21–66, 1998\.
  * [2] Wil M.P. van der Aalst.  Data science in action.  In Process mining, pages 3–23. Springer, 2016.
  * [3] Wil M.P. van der Aalst, Arya Adriansyah, and Boudewijn F. van Dongen.  Replaying history on process models for conformance checking and performance analysis.  Wiley Interdisciplinary Reviews: Data Mining and Knowledge Discovery, 2(2):182–192, 2012.
  * [4] Wil M.P. van der Aalst and Alessandro Berti.  Discovering object-centric Petri nets.  Fundamenta informaticae, 175(1-4):1–40, 2020.
  * [5] Arya Adriansyah.  Aligning observed and modeled behavior.  PhD thesis, Mathematics and Computer Science, 2014.
  * [6] Mahdi Alizadeh, Xixi Lu, Dirk Fahland, Nicola Zannone, and Wil M.P. van der Aalst.  Linking data and process perspectives for conformance analysis.  Computers & Security, 73:172–193, 2018.
  * [7] Kamel Barkaoui and Laure Petrucci.  Structural analysis of workflow nets with shared resources.  1998\.
  * [8] Josep Carmona, Boudewijn F. van Dongen, Andreas Solti, and Matthias Weidlich.  Conformance checking.  Springer, 2018.
  * [9] Gero Decker and Mathias Weske.  Instance isolation analysis for service-oriented architectures.  In 2008 IEEE International Conference on Services Computing, volume 1, pages 249–256. IEEE, 2008.
  * [10] Dirk Fahland.  Describing behavior of processes with many-to-many interactions.  In International Conference on Applications and Theory of Petri Nets and Concurrency, pages 3–24. Springer, 2019.
  * [11] Silvio Ghilardi, Alessandro Gianola, Marco Montali, and Andrey Rivkin.  Petri nets with parameterised data: modelling and verification (extended version).  arXiv preprint arXiv:2006.06630, 2020.
  * [12] Kees van Hee, Natalia Sidorova, and Marc Voorhoeve.  Resource-constrained workflow nets.  Fundamenta Informaticae, 71(2, 3):243–257, 2006.
  * [13] Olaf Kummer.  Undecidability in object-oriented Petri nets.  In Petri Net Newsletter. Citeseer, 2000.
  * [14] K. Lautenbach.  Liveness in Petri Nets.  Bonn Interner Bericht ISF. Selbstverl. GMD, 1975.
  * [15] Massimiliano de Leoni and Wil M.P. van der Aalst.  Aligning event logs and process models for multi-perspective conformance checking: An approach based on integer linear programming.  In Business Process Management, pages 113–129. Springer, 2013.
  * [16] Felix Mannhardt, Massimiliano de Leoni, Hajo A Reijers, and Wil M.P. van der Aalst.  Balanced multi-perspective checking of process conformance.  Computing, 98(4):407–437, 2016.
  * [17] Azadeh S Mozafari Mehr, Renata M de Carvalho, and Boudewijn F. van Dongen.  Detecting privacy, data and control-flow deviations in business processes.  In International Conference on Advanced Information Systems Engineering, pages 82–91. Springer, 2021.
  * [18] Marco Montali and Andrey Rivkin.  Model checking Petri nets with names using data-centric dynamic systems.  Formal Aspects of Computing, 28(4):615–641, 2016.
  * [19] Marco Montali and Andrey Rivkin.  Db-nets: On the marriage of colored petri nets and relational databases.  In Transactions on Petri Nets and Other Models of Concurrency XII, pages 91–118. Springer, 2017.
  * [20] Tadao Murata.  Petri nets: Properties, analysis and applications.  Proceedings of the IEEE, 77(4):541–580, 1989.
  * [21] James Lyle Peterson.  Petri net theory and the modeling of systems.  Prentice Hall PTR, 1981.
  * [22] Fernando Rosa-Velardo and David de Frutos-Escrig.  Decision problems for Petri nets with names.  arXiv preprint arXiv:1011.3964, 2010.
  * [23] Fernando Rosa-Velardo, David de Frutos-Escrig, and Olga Marroquín-Alonso.  On the expressiveness of mobile synchronizing Petri nets.  Electronic Notes in Theoretical Computer Science, 180(1):77–94, 2007.
  * [24] Dominique Sommers, Natalia Sidorova, and Boudewijn F. van Dongen.  Aligning event logs to resource-constrained $\nu$-Petri nets.  In International Conference on Applications and Theory of Petri Nets and Concurrency, pages 325–345. Springer, 2022.

##  Appendix 0.A Correctness of the ILP problem

We first show the effectiveness of each constraint:

  * •

Constraint 20 ensures that the original partial order of the individual
alignments is preserved. Note that this also ensures $g\nprec g$ for every
$g\in{\widetilde{\gamma}}$;

  * •

Const. 21 enforces that when a relation $g\prec g^{\prime}$ is removed, the
opposite $g^{\prime}\prec g$ is added:

$\mathbf{R}_{ij}=1\wedge\mathbf{X}_{ij}=0\implies\mathbf{X}_{ij}=1$ (25)

  * •

Const. 22 enforces that the transitive closure is covered:

$\mathbf{X}_{ij}=\mathbf{X}_{jk}=1\implies\mathbf{X}_{ik}=1$ (26)

With Const. 22 together with $g\nprec g$ for every $g\in{\widetilde{\gamma}}$
from Const. 20, there can be no loops in the solution of the ILP problem;

  * •

Const. 23 enforces that the solution is not violating with regard to any
resource instance capacities, which we show in Lemma 2.

###### Lemma 2

(Constraint 23 ensures there are no violations) With a composed alignment
${\widetilde{\gamma}}=\doublecup_{c\in\textnormal{Id}_{c}}\gamma_{c}$ and
$\mathbf{X}$ a solution to the ILP problem formulated above. The permutation
${\widetilde{\gamma}}^{\prime}=(\bar{\widetilde{\gamma}}^{\prime},\prec_{{\widetilde{\gamma}}^{\prime}})$
of ${\widetilde{\gamma}}$ following the partial order of $\mathbf{X}$, i.e.,
$\bar{\widetilde{\gamma}}^{\prime}=\bar{\widetilde{\gamma}}$ and
$\prec_{{\widetilde{\gamma}}^{\prime}}=\\{({\widetilde{\gamma}}^{\prime}(i),{\widetilde{\gamma}}^{\prime}(j))\mid
i,j\in[1..n_{\widetilde{\gamma}}],\mathbf{X}_{ij}=1\\}$, is not violating (cf.
Def. 19).

###### Proof

First, let us rewrite Const. 23 to

$\forall_{i\in[1..n_{\widetilde{\gamma}}]}\forall_{k\in[1..n_{r}]}(1-\mathbf{X}_{i\bullet})\mathbf{C}^{\downarrow}_{\bullet
k}-\mathbf{X}^{T}_{i\bullet}\mathbf{C}^{\uparrow}_{\bullet
k}\leq\mathbf{k}_{k}=|\textnormal{Id}_{R}(k)|$ (27)

For ever move index $i\in[1..n_{\widetilde{\gamma}}]$, we can define
$G_{i}=\\{{\widetilde{\gamma}}(j)\mid
j\in[1..n_{\widetilde{\gamma}}],\mathbf{X}_{ij}=\mathbf{X}_{ji}=0\\}$ to be
the maximal antichain in $\mathbf{X}$ that contains ${\widetilde{\gamma}}(i)$.
$(1-\mathbf{X}_{ij})$ and $\mathbf{X}^{T}_{ij})$ relate to $G_{i}$ as follows:

$(1-\mathbf{X}_{ij})=1\iff{\widetilde{\gamma}}(j)\in(\bot,G_{i}]\text{ and
}\mathbf{X}^{T}_{ij}=1\iff{\widetilde{\gamma}}(j)\in(\bot,G_{i})$ (28)

We can now rewrite the Eq. 27 to match the property in Eq. 9, with
abbreviations
$C^{\downarrow}_{\rho_{r}}((e,t_{\mu}))=\mathcal{F}(p_{r},t)((\varepsilon,\mu^{-1}(\rho_{r})))$
and
$C^{\downarrow}_{\rho_{r}}((e,t_{\mu}))=\mathcal{F}(t,p_{r})((\varepsilon,\mu^{-1}(\rho_{r})))$.
Note that
$\mathbf{C}^{\downarrow}_{jk}=C^{\downarrow}_{\textnormal{Id}_{R}(k)}({\widetilde{\gamma}}(j))$
and
$\mathbf{C}^{\uparrow}_{jk}=C^{\uparrow}_{\textnormal{Id}_{R}(k)}({\widetilde{\gamma}}(j))$
for every $j\in[1..n_{\widetilde{\gamma}}]$ and $k\in[1..n_{r}]$. For every
$i\in[1..n_{\widetilde{\gamma}}]$ and $k\in[1..n_{r}]$ with
$\rho=\textnormal{Id}_{R}(k)$, the following holds:

$\displaystyle(1-\mathbf{X}_{i\bullet})\mathbf{C}^{\downarrow}_{\bullet
k}-\mathbf{X}^{T}_{i\bullet}\mathbf{C}^{\uparrow}_{\bullet k}$
$\displaystyle\leq|\rho|$ (29) $\displaystyle\iff$
$\displaystyle\sum_{j\in[1..n_{\gamma}]}\left((1-\mathbf{X}_{ij})\mathbf{C}^{\downarrow}_{jk}-\mathbf{X}^{T}_{ij}\mathbf{C}^{\uparrow}_{jk}\right)$
$\displaystyle\leq|\rho|$ (30) $\displaystyle\iff$
$\displaystyle\sum_{g\in(\bot,G_{i}]}C^{\downarrow}_{\rho}(g)-\sum_{g\in(\bot,G)}C^{\uparrow}_{\rho}(g)$
$\displaystyle\leq|\rho|$ (By Eq. 28) (31) $\displaystyle\iff$
$\displaystyle\sum_{g\in(\bot,G_{i})}\left(C^{\downarrow}_{\rho}(g)-C^{\uparrow}_{\rho}(g)\right)+\sum_{g\in
G}C^{\downarrow}_{\rho}(g)$ $\displaystyle\leq|\rho|$ (32) $\displaystyle\iff$
$\displaystyle|\rho|-\sum_{g\in(\bot,G_{i})}\left(C^{\downarrow}_{\rho}(g)-C^{\uparrow}_{\rho}(g)\right)+\sum_{g\in
G}C^{\downarrow}_{\rho}(g)$ $\displaystyle\geq 0$ (33) $\displaystyle\iff$
$\displaystyle\widetilde{m}((\bot,G))(p_{r})((\varepsilon,\rho_{r}))+\sum_{g\in
G}C^{\downarrow}_{\rho}(g)$ $\displaystyle\geq 0$ (By Def. 15) (34)

∎

Next, we go over two important properties of the ILP problem. In Lemma 3, we
show that a solution respecting the constraints always exists for any composed
alignment ${\widetilde{\gamma}}$, and in Lemma 4 we show that if and only if
${\widetilde{\gamma}}$ is not violating as defined in Def. 19, the cost of the
solution is 0.

###### Lemma 3

(There always exists a solution to the ILP problem.) With a composed alignment
${\widetilde{\gamma}}=\doublecup_{c\in\textnormal{Id}_{c}}\gamma_{c}$ and the
ILP problem formulated as above, there exists a solution for $\mathbf{X}$ such
that all constraints hold.

###### Proof

We show by construction that there is always a solution $\mathbf{X}^{\prime}$
to the ILP problem, which respects all constraints. Let there be a (possibly
arbitrary) order in $\textnormal{Id}_{c}$, such that $c_{x}$ denotes the
$x^{\text{th}}$ case identifiers for every $x\in[1..n_{c}]$, with
$n_{c}=|\textnormal{Id}_{c}|$.

$\mathbf{X}^{\prime}=\begin{bmatrix}\mathbf{R}_{c_{1}}&\mathbf{1}&\cdots&\mathbf{1}\\\
\mathbf{0}&\mathbf{R}_{c_{2}}&\cdots&\mathbf{1}\\\
\vdots&\vdots&\ddots&\vdots\\\
\mathbf{0}&\mathbf{0}&\cdots&\mathbf{R}_{c_{n_{c}}}\end{bmatrix}$ (35)

with $\mathbf{R}_{c}=\mathbf{R}_{I_{c}I_{c}}$ for each
$c\in\textnormal{Id}_{c}$ the $|\gamma_{c}|\times|\gamma_{c}|$ submatrix
containing only the elements of the case.

  1. Const. 20

$\mathbf{X}^{\prime}$ trivially respects this constraint as it contains
$\mathbf{R}_{c}$ for each $c\in\textnormal{Id}_{c}$;

  2. Const. 21

Let $i\in I_{c_{x}}$ and $j\in I_{c_{y}}$ be two indices. If $x=y$, this
trivially holds, since $\mathbf{X}^{\prime}$ contains $\mathbf{R}_{c_{x}}$.
Otherwise, by construction of $\mathbf{X}_{ij}$,
$\mathbf{R}_{ij}=1\wedge\mathbf{X}_{ij}=0\implies
j<i\implies\mathbf{X}_{ji}=1$;

  3. Const. 22

Let $i,j,k\in I_{c_{x}},I_{c_{y}},I_{c_{z}}$ respectively. When $x=y=z$, this
trivially holds, since $\mathbf{X}^{\prime}$ contains $\mathbf{R}_{c_{x}}$
which is transitively closed. Otherwise, we know by construction of
$\mathbf{X}^{\prime}$ that with $x\neq y$, $\mathbf{X}^{\prime}_{ij}=1\iff
x<y$ and $\mathbf{X}^{\prime}_{ij}=0\iff x>y$ which we use two prove the two
cases:

    1. (1)

$\mathbf{X}^{\prime}_{ij}=1\wedge x\neq y\implies x<y$.
$\mathbf{X}^{\prime}_{jk}=1\implies y\leq z\implies
x<z\implies\mathbf{X}^{\prime}_{ik}=1$;

    2. (2)

$\mathbf{X}^{\prime}_{jk}=1\wedge y\neq z\implies y<z$.
$\mathbf{X}^{\prime}_{ij}=1\implies x\leq y\implies
x<z\implies\mathbf{X}^{\prime}_{ik}=1$.

Hence $\mathbf{X}^{\prime}$ is transitively closed;

  4. Const. 23

For every $x\in[1..n_{c}]$ and every $i\in I_{c_{x}}$, let $J_{i}=\\{j\mid
j\in[1..n_{\widetilde{\gamma}}],1-\mathbf{X}^{\prime}_{ij}=1\\}$ and
$J_{i}^{\prime}=\\{j\mid j\in[1..n_{\widetilde{\gamma}}],\mathbf{X}^{\prime
T}_{ij}=1\\}$, note that $J^{\prime}\subseteq J$. We know by construction of
$\mathbf{X}^{\prime}$ that for every $y\in[1..n_{c}]$ and every $j\in
I_{c_{y}}$, $1-\mathbf{X}^{\prime}_{ij}=1\implies y\leq x$ and
$\mathbf{X}^{\prime T}_{ij}=1\implies y\leq x$. Therefore

$\forall_{y\in[1..n_{c}]\setminus\\{x\\}}I_{c_{y}}\subseteq J^{\prime}\vee
I_{c_{y}}\cap J^{\prime}=\emptyset$ (36)

holds. Since $\gamma_{c_{y}}$ is an alignment for every $y\in[1..n_{c}]$, we
have for every resource index $k\in[1..n_{r}]$, $\sum_{j\in
I_{c_{y}}}(\mathbf{C}^{\downarrow}_{jk}-\mathbf{C}^{\uparrow}_{jk})=0$ which
together imply that

$\begin{gathered}\sum_{j\in J}\mathbf{C}^{\downarrow}_{jk}-\sum_{j\in
J^{\prime}}\mathbf{C}^{\uparrow}_{jk}=\sum_{y\in[1..n_{c}]}\left(\sum_{j\in
J\cap I_{c_{y}}}\mathbf{C}^{\downarrow}_{jk}-\sum_{j\in J^{\prime}\cap
I_{c_{y}}}\mathbf{C}^{\uparrow}_{jk}\right)\\\ =\sum_{j\in J\cap
I_{c_{x}}}\mathbf{C}^{\downarrow}_{jk}-\sum_{j\in J^{\prime}\cap
I_{c_{x}}}\mathbf{C}^{\uparrow}_{jk}\leq|\textnormal{Id}_{R}(k)|\end{gathered}$
(37)

since $\gamma_{c_{x}}$ is a non-violating alignment.

∎

###### Lemma 4

(Cost=0 if and only if the composed alignment is not violating.) With a
composed alignment
${\widetilde{\gamma}}=\doublecup_{c\in\textnormal{Id}_{c}}\gamma_{c}$, the
solution to the ILP problem formulated above has zero cost if and only if
${\widetilde{\gamma}}$ is not violating as defined in Def. 19, i.e., Eq. 9
does not hold for ${\widetilde{\gamma}}$.

###### Proof

We prove the two sides of the bi-implication:

  * $(\implies)$

Assuming the cost is zero, we have for every
$i,j\in[1..n_{\widetilde{\gamma}}]$,
$\mathbf{R}_{ij}=1\implies\mathbf{X}_{ij}=1$ by the objective function, and
therefore $\\{({\widetilde{\gamma}}(i),{\widetilde{\gamma}}(j))\mid
i,j\in[1..n_{\widetilde{\gamma}}],\mathbf{R}_{ij}=1\\}=\prec_{\mathbf{R}}\subseteq\prec_{\mathbf{X}}=\\{({\widetilde{\gamma}}(i),{\widetilde{\gamma}}(j))\mid
i,j\in[1..n_{\widetilde{\gamma}}],\mathbf{X}_{ij}=1\\}$. Since $\mathbf{X}$
respects Const. 23, $\mathbf{R}$ is not violating either;

  * $(\impliedby)$

Assuming ${\widetilde{\gamma}}$ is not violating, there exists a
${\widetilde{\gamma}}^{\prime}\in\mathcal{S}({\widetilde{\gamma}})$, such that
the resource capacities are respected. Any $\mathbf{X}$ such that
$\prec_{\widetilde{\gamma}}\subseteq\prec_{{\widetilde{\gamma}}^{\prime}}\subseteq\prec_{\mathbf{X}}$
results in zero cost, since for every $i,j\in[1..n_{\widetilde{\gamma}}]$,
$\mathbf{R}_{ij}=1\implies\mathbf{X}_{ij}=1$. Furthermore, the cost can not be
negative as $(1-\mathbf{R}_{ij})\mathbf{X}_{ij}\geq 1$ for every
$i,j\in[1..n_{\widetilde{\gamma}}]$.

∎

Lastly, to fulfill the assumption in Sec. 5 that the intervals around
violating antichains are alignable, we show in Lemma 5 that this is the case
for each interval in $W({\widetilde{\gamma}}^{\prime}_{V})$.

###### Lemma 5

(Each interval $[A,B]\in W({\widetilde{\gamma}}^{\prime}_{V})$ is alignable)
Let ${\widetilde{\gamma}}=\doublecup_{c\in\textnormal{Id}_{c}}\gamma_{c}$ be a
composed alignment and $W({\widetilde{\gamma}}^{\prime}_{V})$ with
${\widetilde{\gamma}}^{\prime}_{V}=\cup_{i,j\in[1..n_{\widetilde{\gamma}}],\mathbf{X}_{ij}-\mathbf{R}_{ij}=1}[{\widetilde{\gamma}}(j),{\widetilde{\gamma}}(i)]$
the set of intervals obtained from the ILP problem formulated above with
solution $\mathbf{X}$. For every $[A,B]\in
W({\widetilde{\gamma}}^{\prime}_{V})$, $[A,B]$ is alignable, i.e., (by Def.
20) $m_{A}\xrightarrow{*}m_{B}$ with $m_{A}=\widetilde{m}((\bot,A))$ and
$m_{B}=\widetilde{m}((\bot,B])$.

###### Proof

Let $[A,B]\in W({\widetilde{\gamma}}^{\prime}_{V})$ be any interval in
$W({\widetilde{\gamma}}^{\prime}_{V})$. We prove that
$m_{A}\xrightarrow{*}m_{B}$ by construction of a subalignment
$\gamma_{AB}=(\bar{\gamma}_{AB},\prec_{\gamma_{AB}})$ constructed as follows:

$\displaystyle\bar{\gamma}_{AB}$
$\displaystyle=\bigcup_{(e,t_{\mu})\in[A,B]\cap\Gamma_{s}}\left\\{(\gg,t_{\mu}),(e,\gg)\right\\}$
(38) $\displaystyle\prec_{\gamma_{AB}}$
$\displaystyle=(\left\\{\left((\gg,t_{\mu}(i)),(\gg,t_{\mu}(j))\right)\mid
i,j\in[1..n_{\gamma}],\gamma(i),\gamma(j)\in[A,B]\setminus\Gamma_{l},\mathbf{X}_{ij}=1\right\\}$
(39)
$\displaystyle~{}\cup\\{((e,t_{\mu}),(e^{\prime},t^{\prime}_{\mu}))\mid(e,t_{\mu}),(e^{\prime},t^{\prime}_{\mu}))\in\prec_{\gamma^{\prime}_{L}},(e,\gg),(e^{\prime},\gg)\in\gamma_{AB}\\})^{+}$

i.e., all synchronous moves are split into a corresponding model and log move
and the partial order for model moves is defined by $\mathbf{X}$ and for the
log moves by the event log’s partial order $\prec_{L}$. There is a $\sigma\in
N(\gamma_{AB})^{*}$ such that $m_{A}\xrightarrow{\sigma}m_{B}$ because of two
properties of $\gamma_{AB}$:

  * •

By Const. 23 and Lemma 2, $\forall_{G\in\mathcal{A}^{+}(\gamma_{AB}),\rho\in
supp(\textnormal{Id}_{R})}\neg\operatorname{viol}(G)$;

  * •

For every $c\in\textnormal{Id}_{c}$, we have, by construction of $\gamma_{AB}$
and the ILP’s constraints,
$\gamma_{AB}{\upharpoonright}_{T_{c}}=[A,B]{\upharpoonright}_{T_{c}}$, with
$T_{c}=\\{t_{\mu}\mid t_{\mu}\in T_{\mu},\exists_{v_{c}\in Var_{c},v_{r}\in
Var_{r})}\mu((v_{c},v_{r}))=(c,*)\\}$. Therefore,
$\gamma_{AB}{\upharpoonright}_{c}=\gamma_{AB}\cap\Gamma_{c}$ is an alignment,
with
$\Gamma_{c}=\\{(e,t_{\mu})\mid(e,t_{\mu})\in\gamma_{AB},\operatorname{case}(e)=c\vee
t_{\mu}\in T_{c}\\}$.

∎