11institutetext: Department of Information and Computing Sciences, Utrecht
University
Princetonplein 5, 3584 CC Utrecht, The Netherlands
11email<EMAIL_ADDRESS>22institutetext:
Faculty of Computer Science, Free University of Bozen-Bolzano
piazza Domenicani 3, 39100, Bolzano, Italy
22email<EMAIL_ADDRESS>
33institutetext: The University of Melbourne, Victoria 3010, Australia
33email<EMAIL_ADDRESS>44institutetext: Department of
Applied Mathematics and Computer Science,
Technical University of Denmark
Richard Petersens Plads 321, 2800 Kgs. Lyngby, Denmark
44email<EMAIL_ADDRESS>
# On the Reconstructability and Rediscoverability of Typed Jackson Nets
(Extended version)

Daniël Barenholz 11 Marco Montali 22 Artem Polyvyanyy 33 Hajo A. Reijers 11
Andrey Rivkin 2244 Jan Martijn E. M. van der Werf 11

###### Abstract

A process discovery algorithm aims to construct a model from data generated by
historical system executions such that the model describes the system well.
Consequently, one desired property of a process discovery algorithm is
_rediscoverability_ , which ensures that the algorithm can construct a model
that is behaviorally equivalent to the original system. A system often
simultaneously executes multiple processes that interact through object
manipulations. This paper presents a framework for developing process
discovery algorithms for constructing models that describe interacting
processes based on typed Jackson Nets that use identifiers to refer to the
objects they manipulate. Typed Jackson Nets enjoy the _reconstructability_
property which states that the composition of the processes and the
interactions of a decomposed typed Jackson Net yields a model that is
bisimilar to the original system. We exploit this property to demonstrate that
if a process discovery algorithm ensures rediscoverability, the system of
interacting processes is rediscoverable.

##  1 Introduction

Business processes are fundamental to a wide range of systems. A business
process is a collection of activities that, when performed, aims to achieve a
business objective at an organization. Examples of business processes are an
order-to-cash process at a retailer, a medical assessment process at a
hospital, or a credit check process at a bank. Business processes are modeled
using process modeling languages, such as Petri nets, and used for
communication and analysis purposes [1]. Petri nets provide a graphical
representation of the flow of activities within a process and can be used to
model various types of concurrent and sequential behavior [18].

A process discovery algorithm aims to automatically construct a model from
data generated by historical process executions captured in an event log of
the system, such that the model describes the system well. A desired property
of a discovery algorithm is _rediscoverability_. This property states that if
a system $S$, expressed as a model $M$, generates an event log $L$, then a
discovery algorithm with the rediscoverability property should construct $M$
from $L$. In other words, the algorithm can reverse engineer the model of the
system from the data the model has generated. Only a few existing algorithms
guarantee this property. For example, if the model is a block-structured
workflow net, and the event log is directly-follows complete, then the
$\alpha$-Miner algorithm [22] can rediscover the net that generated the event
log. Similarly, again under the assumption that the event log is directly-
follows complete, Inductive Miner [16] can rediscover process trees without
duplicate transitions, self-loops, or silent transitions.

Figure 1: A retailer system of three interacting processes.

Most existing process discovery algorithms assume that a system executes a
single process [4]. Consequently, an event log is defined as a collection of
sequences where a sequence describes the execution of a single process
instance. However, many information systems, such as enterprise resource
planning systems, do not satisfy this assumption. A system often executes
multiple interacting processes [10, 23]. For example, consider a retailer
system that executes three processes: an order, product, and customer
management process, as depicted in Fig. 1. These processes are intertwined.
Specifically, only available products may be ordered, and customers can only
have one order at a time. Consequently, events do not belong to a single
process but relate to several processes. For instance, consider an event $e$
in some event log that occurred as transition $G$ was executed for some
customer $c$ and created a new order $o$ in the system. Event $e$ relates to
the customer process instance $c$ and the order process instance $o$.
Traditional process discovery techniques require event $e$ to be stored in
multiple event logs and generate multiple models, one for each process [7].

A different approach is taken in artifact or object-centric process discovery
[5, 17] and agent system discovery [20, 21]. In object-centric process
discovery, instead of linking each event to a single object, events can be
linked to multiple objects stored in object-centric event logs [8]. Existing
object-centric discovery algorithms project the input event log on each object
type to create a set of “flattened” event logs. For each event log, a model is
discovered, after which these models are combined into a single model [5]. In
general, flattening is lossy [7], as in this step, events can disappear [5],
be duplicated (convergence) [3], or lead to wrong event orders (divergence)
[3]. In agent system discovery, instead of interacting objects, a system is
viewed as composed of multiple autonomous agents, each driving its processes
that interact to achieve an overall objective of the system [20]. An agent
system discovery algorithm proceeds by decomposing the input event log into
multiple event logs, each composed of events performed by one agent (type) and
an event log of interactions, and then discovering agent and interaction
models and composing them into the resulting system [21].

$M$$M_{1}$$\cdots$$M_{n}$$M^{\prime}$$L$$L_{1}$$\cdots$$L_{n}$$D_{1}$$\cdots$$D_{n}$$D^{\prime}$projectprojectcomposecomposeSection
4Section 5generates(?)(?)(?)(?)discoverdiscover(?)(?) Figure 2: The framework
for rediscoverability of systems of interacting processes.

In this paper, we study under what conditions projections in event logs can
guarantee rediscoverability for interacting processes, represented as typed
Jackson Nets, a subclass of typed Petri nets with identifiers [19, 23]. The
class of typed Jackson Nets is inspired by Box Algebra [9] and Jackson Nets
[14], which are (representations of) block-structured workflow nets that are
_sound_ [2] by construction [16]. As we demonstrate, typed Jackson Nets
exhibit a special property: they are _reconstructable_. Composing the
projections of each type is insufficient for reconstructing a typed Jackson
Net. Instead, if the subset-closed set of all type combinations is considered,
the composition returns the original model of the system. We show how the
reconstructability property can be used to develop a framework for
rediscoverability of typed Jackson Nets using traditional process discovery
algorithms. The framework builds upon a divide and conquer strategy, as
depicted in Fig. 2. The principle idea of this strategy is to project an event
log $L$ generated by some model $M$ of the system onto logs
$L_{1},\ldots,L_{n}$. Then, if these projected event logs satisfy the
conditions of a process discovery algorithm, composition of the resulting
models $D_{1},\ldots,D_{n}$ into model $D^{\prime}$ should rediscover the
original model of the system. In this framework, we show that every projected
event log is also an event log of the corresponding projected model.
Consequently, if a process discovery algorithm guarantees the
rediscoverability of projected models, then the composition operator for typed
Jackson Nets can be used to ensure the rediscoverability of the original
system.

The next section presents the basic notions. In Section 3, we introduce typed
Jackson Nets, which, as shown in Section 4, are reconstructable. We define a
framework for developing discovery algorithms that guarantee rediscoverability
in Section 5. We conclude the paper in Section 6.

##  2 Preliminaries

Let $S$ and $T$ be two possibly infinite sets. The powerset of $S$ is denoted
by $\mathcal{P}(S)=\left\\{S^{\prime}\mid S^{\prime}\subseteq S\right\\}$ and
$\left|{S}\right|$ denotes the cardinality of $S$. Two sets $S$ and $T$ are
_disjoint_ if $S\cap T=\emptyset$, with $\emptyset$ denoting the empty set.
The cartesian product of two sets $S$ and $T$, is defined by $S\times
T=\left\\{(a,b)\mid a\in S,b\in T\right\\}$. The generalized cartesian product
for some set $S$ and and sets $T_{s}$ for $s\in S$ is defined as $\Pi_{s\in
S}T_{s}=\left\\{f:S\to\bigcup_{s\in S}T_{s}\mid\forall s\in S:f(s)\in
T_{s}\right\\}$. Given a relation $R\subseteq S\times T$, its range is defined
by $\textsc{rng}(R)=\left\\{y\in T\mid\exists x\in S:(x,y)\in R\right\\}$.
Similarly, the domain of $R$ is defined by $\textsc{dom}(R)=\left\\{x\in
S\mid\exists y\in T:(x,y)\in R\right\\}$. Restricting the domain of a relation
to a set $U$ is defined by ${R}_{{\mid{U}}}=\\{(a,b)\in R\mid a\in U\\}$.

A _multiset_ $m$ over $S$ is a mapping of the form $m:S\rightarrow\mathbb{N}$,
where $\mathbb{N}=\\{0,1,2,\ldots\\}$ denotes the set of natural numbers. For
$s\in S$, $m(s)\in\mathbb{N}$ denotes the number of times $s$ appears in
multiset $m$. We write $s^{n}$ if $m(s)=n$. For $x\not\in S$, $m(x)=0$. We use
$S^{\oplus}$ to denote the set of all finite multisets over $S$ and overload
$\emptyset$ to also denote the empty multiset. The size of a multiset is
defined by $|m|=\sum_{s\in S}m(s)$. The support of $m\in S^{\oplus}$ is the
set of elements that appear in $m$ at least once:
$\mathit{supp}\left(m\right)=\left\\{s\in S\mid m(s)>0\right\\}$. Given two
multisets $m_{1}$ and $m_{2}$ over $S$:  (i) $m_{1}\subseteq m_{2}$(resp.,
$m_{1}\subset m_{2}$) iff $m_{1}(s)\leq m_{2}(s)$ (resp., $m_{1}(s)<m_{2}(s)$)
for each $s\in S$;  (ii) $(m_{1}+m_{2})(s)=m_{1}(s)+m_{2}(s)$for each $s\in
S$; and  (iii) if $m_{1}\subseteq m_{2}$, $(m_{2}-m_{1})(s)=m_{2}(s)-m_{1}(s)$
for each $s\in S$.

A _sequence_ over $S$ of length $n\in\mathbb{N}$ is a function
$\sigma:\\{1,\ldots,n\\}\to S$. If $n>0$ and $\sigma(i)=a_{i}$, for $1\leq
i\leq n$, we write $\sigma=\left\langle a_{1},\ldots,a_{n}\right\rangle$. The
length of a sequence $\sigma$ is denoted by $\left|{\sigma}\right|$. The
sequence of length $0$ is called the _empty sequence_ , and is denoted by
$\epsilon$. The set of all finite sequences over $S$ is denoted by $S^{*}$. We
write $a\in\sigma$ if there is $1\leq i\leq\left|{\sigma}\right|$ such that
$\sigma(i)=a$ and $\mathit{supp}\left(\sigma\right)=\\{a\in S\mid\exists 1\leq
i\leq\left|{\sigma}\right|:\sigma(i)=a\\}$. _Concatenation_ of two sequences
$\nu,\gamma\in S^{*}$, denoted by $\sigma=\nu\cdot\gamma$, is a sequence
defined by
$\sigma:\\{1,\ldots,\left|{\nu}\right|+\left|{\gamma}\right|\\}\rightarrow S$,
such that $\sigma(i)=\nu(i)$ for $1\leq i\leq\left|{\nu}\right|$, and
$\sigma(i)=\gamma(i-\left|{\nu}\right|)$ for $\left|{\nu}\right|+1\leq
i\leq\left|{\nu}\right|+\left|{\gamma}\right|$. Projection of sequences on a
set $T$ is defined inductively by ${\epsilon}_{{\mid{T}}}=\epsilon$,
${(\left\langle a\right\rangle\cdot\sigma)}_{{\mid{T}}}=\left\langle
a\right\rangle\cdot{\sigma}_{{\mid{T}}}$ if $a\in T$ and ${(\left\langle
a\right\rangle\cdot\sigma)}_{{\mid{T}}}={\sigma}_{{\mid{T}}}$ otherwise.
Renaming a sequence with an injective function $r:S\rightarrow T$ is defined
inductively by $\rho_{r}(\epsilon)=\epsilon$, and $\rho_{r}(\left\langle
a\right\rangle\cdot\sigma)=\left\langle
r(a)\right\rangle\cdot\rho_{r}(\sigma)$. Renaming is extended to multisets of
sequences as follows: given a multiset $m\in(S^{*})^{\oplus}$, we define
$\rho_{r}(m)=\sum_{\sigma\in\mathit{supp}\left(m\right)}\sigma(m)\cdot\rho_{r}(\sigma)$.
For example, $\rho_{\\{x\mapsto a,y\mapsto b\\}}(\left\langle
x,y\right\rangle^{3})=\left\langle a,b\right\rangle^{3}$.

A _directed graph_ is a pair $(V,A)$ where $V$ is the set of vertices, and
$A\subseteq V\times V$ the set of arcs. Two graphs $G_{1}=(V_{1},A_{1})$ and
$G_{2}=(V_{2},A_{2})$ are _isomorphic_ , denoted by $G_{1}\leftrightsquigarrow
G_{2}$, if a bijection $b:V_{1}\rightarrow V_{2}$ exists, such that
$(v_{1},v_{2})\in A_{1}$ iff $(b(v_{1}),b(v_{2}))\in A_{2}$.

Given a finite set $A$ of (action) labels, a _(labeled) transition system_
(LTS) over $A$ is a tuple $\Gamma_{A}=(S,A,s_{0},\to)$, where $S$ is the
(possibly infinite) set of _states_ , $s_{0}$ is the _initial state_ and $\to\
\subset(S\times(A\cup\\{\tau\\})\times S)$ is the _transition relation_ ,
where $\tau\not\in A$ denotes the silent action [12]. In what follows, we
write $s\xrightarrow{a}s^{\prime}$ for $(s,a,s^{\prime})\in\to$. Let
$r:A\to(A^{\prime}\cup\\{\tau\\})$ be an injective, total function. Renaming
$\Gamma$ with $r$ is defined as $\rho_{r}(\Gamma)=(S,A\setminus
A^{\prime},s_{0},\to^{\prime})$ with $(s,r(a),s^{\prime})\in\to^{\prime}$ iff
$(s,a,s^{\prime})\in\to$. Given a set $T$, hiding is defined as
$\hat{\mathtt{H}}_{T}(\Gamma)=\rho_{h}(\Gamma)$ with $h:A\rightarrow
A\cup\\{\tau\\}$ such that $h(t)=\tau$ if $t\in T$ and $h(t)=t$ otherwise.
Given $a\in A$, $p\leavevmode\hbox to22.77pt{\vbox
to8.61pt{\pgfpicture\makeatletter\hbox{\hskip 11.38306pt\lower-2.39996pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.35005pt}{1.7pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\scriptsize{$\leavevmode\nobreak\ a\leavevmode\nobreak\ $}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{ {}}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{ }{}{{
{\pgfsys@beginscope\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@miterjoin{}
{} {}
\pgfsys@moveto{-2.19997pt}{-2.39996pt}\pgfsys@lineto{0.2pt}{0.0pt}\pgfsys@lineto{-2.19997pt}{2.39996pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}{}{}{{}}\pgfsys@moveto{-7.78307pt}{0.0pt}\pgfsys@lineto{7.30028pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{7.30028pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}q$ denotes a _weak
transition relation_ that is defined as follows:  (i) $p\leavevmode\hbox
to22.77pt{\vbox to8.81pt{\pgfpicture\makeatletter\hbox{\hskip
11.38306pt\lower-2.59998pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.35005pt}{1.7pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\scriptsize{$\leavevmode\nobreak\ a\leavevmode\nobreak\ $}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{ {}}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{ }{}{{ {\pgfsys@beginscope
\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{} {}{}{} {}{}{}
\pgfsys@moveto{-2.07999pt}{2.39998pt}\pgfsys@curveto{-1.69998pt}{0.95998pt}{-0.85318pt}{0.28pt}{0.0pt}{0.0pt}\pgfsys@curveto{-0.85318pt}{-0.28pt}{-1.69998pt}{-0.95998pt}{-2.07999pt}{-2.39998pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}{}{}{{}}\pgfsys@moveto{-7.78307pt}{0.0pt}\pgfsys@lineto{7.38307pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{7.58307pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}q$iff
$p(\xrightarrow{\tau})^{*}q_{1}\xrightarrow{a}q_{2}(\xrightarrow{\tau})^{*}q$;
(ii) $p\leavevmode\hbox to22.13pt{\vbox
to8.81pt{\pgfpicture\makeatletter\hbox{\hskip 11.06303pt\lower-2.59998pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.03003pt}{1.7pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\scriptsize{$\leavevmode\nobreak\ \tau\leavevmode\nobreak\ $}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{ {}}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-7.46304pt}{0.0pt}\pgfsys@lineto{7.06305pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{7.26305pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}q$iff
$p(\xrightarrow{\tau})^{*}q$.  Here, $(\xrightarrow{\tau})^{*}$ denotes the
reflexive and transitive closure of $\xrightarrow{\tau}$.

Let $\Gamma_{1}=(S_{1},A,s_{01},\to_{1})$ and
$\Gamma_{2}=(S_{2},A,s_{02},\to_{2})$ be two LTSs. A relation
$R\subseteq(S_{1}\times S_{2})$ is called a _strong simulation_ , denoted as
$\Gamma_{1}\prec_{R}\Gamma_{2}$, if for every pair $(p,q)\in R$ and $a\in
A\cup\\{\tau\\}$, it holds that if $p\xrightarrow{a}_{1}p^{\prime}$, then
there exists $q^{\prime}\in S_{2}$ such that $q\xrightarrow{a}_{2}q^{\prime}$
and $(p^{\prime},q^{\prime})\in R$. Relation $R$ is a _weak simulation_ ,
denoted by $\Gamma_{1}\preccurlyeq_{R}\Gamma_{2}$, iff for every pair
$(p,q)\in R$ and $a\in A\cup\\{\tau\\}$ it holds that if
$p\xrightarrow{a}_{1}p^{\prime}$, then $a=\tau$ and $(p^{\prime},q)\in R$, or
there exists $q^{\prime}\in S_{2}$ such that $q\leavevmode\hbox
to22.77pt{\vbox to6.41pt{\pgfpicture\makeatletter\hbox{\hskip
11.38306pt\lower-0.2pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.35005pt}{1.7pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{\scriptsize{$\leavevmode\nobreak\ a\leavevmode\nobreak\ $}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}{}{ {}}
{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setdash{3.0pt,3.0pt}{0.0pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-7.78307pt}{0.0pt}\pgfsys@lineto{7.30028pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{7.30028pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}_{2}\leavevmode\nobreak\
q^{\prime}$ and $(p^{\prime},q^{\prime})\in R$. Relation $R$ is called a
strong (weak) _bisimulation_ , denoted by $\Gamma_{1}\sim_{R}\Gamma_{2}$
($\Gamma_{1}\approx_{R}\Gamma_{2}$) if both $\Gamma_{1}\prec\Gamma_{2}$
($\Gamma_{1}\preccurlyeq_{R}\Gamma_{2}$) and
$\Gamma_{2}\prec_{R^{-1}}\Gamma_{1}$
($\Gamma_{2}\preccurlyeq_{R^{-1}}\Gamma_{1}$). Given a strong (weak)
(bi)simulation $R$, we say that a state $p\in S_{1}$ is strongly (weakly)
rooted (bi)similar to $q\in S_{2}$, written $p\sim^{r}_{R}q$ (correspondingly,
$p\approx^{r}_{R}q$), if $(p,q)\in R$. The relation is called _rooted_ iff
$(s_{01},s_{02})\in R$. A rooted relation is indicated with a superscript r.

A weighted Petri net is a 4-tuple $(P,T,F,W)$ where $P$ and $T$ are two
disjoint sets of _places_ and _transitions_ , respectively,
$F\subseteq((P\times T)\cup(T\times P))$ is the _flow relation_ , and
$W:F\rightarrow\mathbb{N}^{+}$ is a _weight function_. For $x\in P\cup T$, we
write ${}^{\bullet}{x}=\left\\{y\mid(y,x)\in F\right\\}$ to denote the
_preset_ of $x$ and ${x}^{\bullet}=\left\\{y\mid(x,y)\in F\right\\}$ to denote
the _postset_ of $x$. We lift the notation of preset and postset to sets
element-wise. If for a Petri net no weight function is defined, we assume
$W(f)=1$ for all $f\in F$. A _marking_ of $N$ is a multiset $m\in P^{\oplus}$,
where $m(p)$ denotes the number of _tokens_ in place $\mathit{p}\in P$. If
$m(\mathit{p})>0$, place $\mathit{p}$ is called _marked_ in marking $m$. A
_marked Petri net_ is a tuple $\left(N,m\right)$ with $N$ a weighted Petri net
with marking $m$. A transition $\mathit{t}\in T$ is enabled in
$\left(N,m\right)$, denoted by $\left(N,m\right)[\mathit{t}\rangle$ iff
$W((\mathit{p},\mathit{t}))\leq m(\mathit{p})$ for all
$\mathit{p}\in{}^{\bullet}{\mathit{t}}$. An enabled transition can _fire_ ,
resulting in marking $m^{\prime}$ iff
$m^{\prime}(\mathit{p})+W((\mathit{p},\mathit{t}))=m(\mathit{p})+W((\mathit{t},\mathit{p}))$,
for all $\mathit{p}\in P$, and is denoted by
$\left(N,m\right)[\mathit{t}\rangle\left(N,m^{\prime}\right)$. We lift the
notation of firings to sequences. A sequence $\sigma\in T^{*}$ is a _firing
sequence_ iff $\sigma=\epsilon$, or markings $m_{0},\ldots,m_{n}$ exist such
that $(N,m_{i-1})[\sigma(i)\rangle(N,m_{i})$ for $1\leq
i\leq\left|{\sigma}\right|=n$, and is denoted by
$(N,m_{0})[\sigma\rangle(N,m_{n})$. If the context is clear, we omit the
weighted Petri net $N$. The set of reachable markings of $\left(N,m\right)$ is
defined by $\mathcal{R}(N,m)=\\{m^{\prime}\mid\exists\sigma\in
T^{*}:m[\sigma\rangle m^{\prime}\\}$. The set of all possible finite firing
sequences of $\left(N,m\right)$ is denoted by
$\mathcal{L}(N,m_{0})=\\{\sigma\in{T}^{*}\mid m[\sigma\rangle m^{\prime}\\}$.
The semantics of a marked Petri net $(N,m)$ with $N=(P,T,F,W)$ is defined by
the LTS $\Gamma_{N,m}=(P^{\oplus},T,m_{0},\to)$ with $(m,t,m^{\prime})\in\to$
iff $m[t\rangle m^{\prime}$. A Petri net $N=(P,T,F,W)$ has underlying graph
$(P\cup T,F)$. Two Petri nets $N$ and $N^{\prime}$ are isomorphic, denoted
using $N\leftrightsquigarrow N^{\prime}$, if their underlying graphs are.

A _workflow net_ (WF-net for short) is a tuple
$N=(P,T,F,W,\mathit{in},\mathit{out})$ such that:  (i) $(P,T,F,W)$is a
weighted Petri net;  (ii) $\mathit{in},\mathit{out}\in P$are the source and
sink place, respectively, with
${}^{\bullet}{\mathit{in}}={\mathit{out}}^{\bullet}=\emptyset$;  (iii) every
node in $P\cup T$ is on a directed path from $\mathit{in}$ to $\mathit{out}$.
$N$ is called _$k$ -sound_ for some $k\in\mathbb{N}$ iff  (i) it is proper
completing, i.e., for all reachable markings
$m\in\mathcal{R}(N,[\mathit{in}^{k}])$, if $[\mathit{out}^{k}]\subseteq m$,
then $m=[\mathit{out}^{k}]$;  (ii) it is weakly terminating, i.e., for any
reachable marking $m\in\mathcal{R}(N,[\mathit{in}^{k}])$, the final marking is
reachable, i.e., $[\mathit{out}^{k}]\in\mathcal{R}(N,m)$; and  (iii) it is
quasi-live, i.e., for all transitions $t\in T$, there is a marking
$m\in\mathcal{R}(N,[\mathit{in}])$ such that $m[t\rangle$.  The net is called
_sound_ if it is $1$-sound. If it is $k$-sound for all $k\in\mathbb{N}$, it is
called _generalized sound_ [13].

##  3 Typed Jackson Nets to Model Interacting Processes

In this section, we introduce typed Jackson Nets as subclass of typed Petri
nets with identifiers. We show that this class is a natural extension to
Jackson Nets, which are representations of block-structured workflow nets.
Typed Jackson Nets are identifier sound and live by construction.

$p_{1}$$t_{1}$$p_{2}$$t_{2}$$t_{3}$$p_{3}$$t_{4}$$t_{5}$$p_{4}$ Figure 3: An
example block-structured WF-net. Each block corresponds to a node in the
Jackson type
$\left(p_{1};\left(t_{1};\left(\left(\left(p_{2};\left(\left(t_{2}+t_{3}\right);p_{3}\right)\right)\\#t_{4}\right);\left(t_{5};p_{4}\right)\right)\right)\right)$.
As example, the choice between transitions $t_{2}$ and $t_{3}$ corresponds to
the node $\left(p_{2};\left(\left(t_{2}+t_{3}\right);p_{3}\right)\right)$ .

###  3.1 Jackson Nets

Whereas WF-nets do not put any restriction on the control flow of activities,
block-structured WF-nets divide the control flow in logical blocks [15]. Each
“block” represents a single unit of work that can be performed, where this
unit of work is either atomic (single transition), or one involving multiple
steps (multiple transitions). An example block-structured WF-net is shown in
Fig. 3. The main advantage of block-structured WF-nets, is that the block-
structure ensures that the WF-net is sound by definition [15, 16, 14]. In this
paper, we consider Jackson Types and Jackson Nets [14]. A Jackson Type is a
data structure used to capture all information involved in a single execution
of a WF-net.

######  Definition 1 (Jackson Type [14]).

The set of _Jackson Types_ $\mathcal{J}$ is recursively defined by the
following grammar:

$\displaystyle\mathcal{J}$
$\displaystyle::=\mathscr{A}^{p}\mid\left(\mathscr{A}^{p};\left(\mathcal{J}^{t};\mathscr{A}^{p}\right)\right)$
$\displaystyle\mathcal{J}^{t}$
$\displaystyle::=\mathscr{A}^{t}\mid\left(\mathcal{J}^{t};\left(\mathcal{J}^{p};\mathcal{J}^{t}\right)\right)\mid\left(\mathcal{J}^{t}+\mathcal{J}^{t}\right)$
$\displaystyle\mathcal{J}^{p}$
$\displaystyle::=\mathscr{A}^{p}\mid\left(\mathcal{J}^{p};\left(\mathcal{J}^{t};\mathcal{J}^{p}\right)\right)\mid\left(\mathcal{J}^{p}\parallel\mathcal{J}^{p}\right)\mid\left(\mathcal{J}^{p}\\#\mathcal{J}^{t}\right)$

where
$\mathscr{A}=\mathscr{A}^{p}\cup\mathscr{A}^{t}=\left\\{a,b,c,\ldots\right\\}$
denotes two disjoint sets of atomic types for places and transitions, resp.,
and symbols $;,\parallel,+,\\#$ stand for sequence, parallelism, choices, and
loops. $\triangleleft$

Multiple Jackson Types may exist for the same WF-net. For example, the Jackson
Type
$\left(\left(p_{1};t_{1}\right);\left(\left(\left(p_{2};\left(\left(t_{2}+t_{3}\right);p_{3}\right)\right)\\#t_{4}\right);\left(t_{5};p_{4}\right)\right)\right)$
describes the WF-net of Fig. 3 as well. Each net has a unique representation
[14], called its normal form. We define an algebraic equivalence between types
to allow rewriting into the normal form.

######  Definition 2 (Algebraic equivalence, normal form [14]).

The _algebraic
equivalence_ $\equiv_{alg}$ is the smallest equivalence relation on the set of
Jackson Types that satisfies the following six rules:

$\begin{array}[]{rclcrcl}\left(\left(J_{0};J_{1}\right);J_{2}\right)&\equiv_{alg}&\left(J_{0};\left(J_{1};J_{2}\right)\right)&&\left(\left(J_{0}+J_{1}\right)+J_{2}\right)&\equiv_{alg}&\left(J_{0}+\left(J_{1}+J_{2}\right)\right)\\\
\left(\left(J_{0}\parallel J_{1}\right)\parallel
J_{2}\right)&\equiv_{alg}&\left(J_{0}\parallel\left(J_{1}\parallel
J_{2}\right)\right)&&\left(J_{0}+J_{1}\right)&\equiv_{alg}&\left(J_{1}+J_{0}\right)\\\
\left(J_{0}\parallel J_{1}\right)&\equiv_{alg}&\left(J_{1}\parallel
J_{0}\right)&&\left(\left(J_{0}\\#J_{1}\right)\\#J_{2}\right)&\equiv_{alg}&\left(J_{0}\\#\left(J_{1}\\#J_{2}\right)\right)\end{array}$

with $J_{0},J_{1},J_{2}\in\mathcal{J}$ three Jackson Types.

A Jackson Type is in _normal form_ iff all brackets are moved to the right
using the above rules. $\triangleleft$

The class of Jackson Nets is obtained by recursively applying _generation
rules_ , starting from a singleton net with only one place. These generation
rules are similar to those defined by Murata [18] and preserve soundness [14].
Thus, any Jackson Net is sound by construction.

######  Definition 3 (Jackson Net [14]).

A WF-net $N=(P,T,F,\mathit{in},\mathit{out})$ is called a _Jackson Net_ if it
can be generated from a single place $p$ by applying the following five
generation rules recursively:

$\begin{array}[]{llcll}\mbox{J1:}&p\leftrightarrow\left(p_{1};\left(t;p_{2}\right)\right)&&\mbox{J4:}&p\leftrightarrow\left(p_{1}\parallel
p_{2}\right)\\\
\mbox{J2:}&t\leftrightarrow\left(t_{1};\left(p_{1};t_{2}\right)\right)&&\mbox{J5:}&t\leftrightarrow\left(t_{1}+t_{2}\right)\\\
\mbox{J3:}&p\leftrightarrow\left(p\\#t\right)&&&\\\ \end{array}$

We say that $N$ is generated by $p$. $\triangleleft$

As shown in [14], Jackson Nets are completely determined by Jackson Types, and
vice versa.

######  Theorem 1 (Jackson Nets and Jackson Types are equivalent [14]).

Let $N_{1}$ and $N_{2}$ be two Jackson Nets that are generated by the Jackson
Types $J_{1}$ and $J_{2}$, resp. Then $N_{1}$ and $N_{2}$ are isomorphic iff
$J_{1}\equiv_{alg}J_{2}$. $\triangleleft$

###  3.2 Petri Nets with Identifiers

Whereas WF-nets describe all possible executions for a single case, systems
typically consist of many interacting processes. The latter can be modeled
using typed Petri nets with identifiers (t-PNIDs for short) [23]. In this
formalism, each object is typed and has a unique identifier to be able to
refer to it. Tokens carry vectors of identifiers, which are used to relate
objects. Variables on the arcs are used to manipulate the identifiers.

######  Definition 4 (Identifiers, Types and Variables).

Let $\mathcal{I}$, $\Lambda$, and $\mathcal{V}$ denote countably infinite sets
of identifiers, type labels, and variables, respectively. We define:

  * •

the _domain assignment_ function
$I:\Lambda\rightarrow\mathcal{P}(\mathcal{I})$, such that $I(\lambda_{1})$ is
an infinite set, and $I(\lambda_{1})\cap I(\lambda_{2})\neq\emptyset$ implies
$\lambda_{1}=\lambda_{2}$ for all $\lambda_{1},\lambda_{2}\in\Lambda$;

  * •

the _id typing_ function $\mathtt{type}_{\mathcal{I}}:\mathcal{I}\to\Lambda$
s.t. if $\mathtt{type}_{\mathcal{I}}(\mathtt{id})=\lambda$, then
$\mathtt{id}\in I(\lambda)$;

  * •

a _variable typing_ function
$\mathtt{type}_{\mathcal{V}}:\mathcal{V}\to\Lambda$, prescribing that
$x\in\mathcal{V}$ can be substituted only by values from
$I(\mathtt{type}_{\mathcal{V}}(x))$.

When clear from the context, we omit the subscripts of $\mathtt{type}$. We
lift the $\mathtt{type}$ functions to sets, vectors, and sequences by applying
the function on each of its constituents. $\triangleleft$

In a t-PNID, each place is annotated with a label, called the _place type_. A
place type is a vector of types, indicating types of identifier tokens the
place can carry. Similar to Jackson Types, we use $\left[p,\lambda\right]$ to
denote that place $p$ has type $\alpha(p)=\lambda$. Each arc is inscribed with
a multiset of vectors of identifiers, such that the type of each variable
coincides with the place types. If the inscription is empty or contains a
single element, we omit the brackets.

######  Definition 5 (Typed Petri net with identifiers).

A _typed Petri net with identifiers_ (t-PNID) $N$ is a tuple
$(P,T,F,\alpha,\beta)$, where:

  * •

$(P,T,F)$ is a classical Petri net;

  * •

$\alpha:P\to\Lambda^{*}$ is the _place typing function_ ;

  * •

$\beta:F\to(\mathcal{V}^{*})^{\oplus}$ defines for each arc a multiset of
_variable vectors_ s.t. $\alpha(p)=\mathtt{type}(x)$ for any
$x\in\mathit{supp}\left(\beta((p,t))\right)$ and
$\mathtt{type}(y)=\alpha(p^{\prime})$ for any
$y\in\mathit{supp}\left(\beta((t,p^{\prime}))\right)$ where $t\in T$,
$p\in{}^{\bullet}{t}$, $p^{\prime}\in{t}^{\bullet}$.

$\triangleleft$

A marking of a t-PNID is the configuration of tokens over the set of places.
Each token in a place should be of the correct type, i.e., the vector of
identifiers carried by a token in a place should match the corresponding place
type. The set $\mathtt{C}(\mathit{p})$ defines all possible vectors of
identifiers a place $p$ may carry.

######  Definition 6 (Marking).

Given a t-PNID $N=(P,T,F,\alpha,\beta)$, and place $\mathit{p}\in P$, its _id
set_ is $\mathtt{C}(\mathit{p})=\prod_{1\leq
i\leq|\alpha(\mathit{p})|}I(\alpha(\mathit{p})(i))$. A _marking_ is a function
$m\in\mathbb{M}\left(N\right)$, with
$\mathbb{M}\left(N\right)=P\to({\Lambda}^{*})^{\oplus}$, such that
$m(\mathit{p})\in\mathtt{C}(p)^{\oplus}$, for each place $\mathit{p}\in P$.
The set of identifiers used in $m$ is denoted by $Id(m)=\bigcup_{\mathit{p}\in
P}\textsc{rng}(\mathit{supp}\left(m(\mathit{p})\right))$ The pair
$\left(N,m\right)$ is called a _marked t-PNID_. $\triangleleft$

To define the semantics of a t-PNID, the variables need to be valuated with
identifiers.

######  Definition 7 (Variable sets [23]).

Given a t-PNID $N=(P,T,F,\alpha,\beta)$, $t\in T$ and $\lambda\in\Lambda$, we
define the following sets of variables:

  * •

_input variables_ as
$\smash{{\mathit{In}({t})}=\bigcup_{x\in\beta((p,t)),p\in{}^{\bullet}{t}}\textsc{rng}(\mathit{supp}\left(x\right))}$;

  * •

_output variables_ as
$\smash{{\mathit{Out}({t})}=\bigcup_{x\in\beta((t,p)),p\in{t}^{\bullet}}\textsc{rng}(\mathit{supp}\left(x\right))}$;

  * •

_variables_ as
${\mathit{Var}({t})}={\mathit{In}({t})}\cup{\mathit{Out}({t})}$;

  * •

_emitting variables_ as
${\mathit{Emit}({t})}={\mathit{Out}({t})}\setminus{\mathit{In}({t})}$;

  * •

_collecting variables_ as
${\mathit{Collect}({t})}={\mathit{In}({t})}\setminus{\mathit{Out}({t})}$;

  * •

_emitting transitions_ as $E_{N}(\lambda)=\\{t\mid\exists
x\in{\mathit{Emit}({t})}\wedge\mathtt{type}(x)=\lambda\\}$;

  * •

_collecting transitions_ as $C_{N}(\lambda)=\\{t\mid\exists
x\in{\mathit{Collect}({t})}\wedge\mathtt{type}(x)=\lambda\\}$;

  * •

_types in $N$_ as $\mathtt{type}(N)=\\{\vec{\lambda}\mid\exists p\in
P:\vec{\lambda}\in\alpha(p)\\}$.

$\triangleleft$

A valuation of variables to identifiers is called a _binding_. Bindings are
used to inject new fresh data into the net via variables that emit
identifiers, i.e., via variables that appear only on the output arcs of that
transition. Note that in this definition, freshness of identifiers is local to
the marking, i.e., disappeared identifiers (those fully removed from the net
through collecting transitions) may be reused, as it does not hamper the
semantics of the t-PNID.

######  Definition 8 (Firing rule for t-PNIDs).

Given a marked t-PNID $(N,m)$ with $N=(P,T,F,\alpha,\beta)$, a _binding_ for
transition $t\in T$ is an injective function
$\psi:\mathcal{V}\rightarrow\mathcal{I}$ such that
$\mathtt{type}(v)=\mathtt{type}(\psi(v))$ and $\psi(v)\not\in Id(m)$ iff
$v\in{\mathit{Emit}({t})}$. Transition $t$ is _enabled_ in $(N,m)$ under
binding $\psi$, denoted by $(N,m)[t,\psi\rangle$ iff
$\rho_{\psi}(\beta(p,t))\leq m(p)$ for all $p\in{}^{\bullet}{t}$. Its firing
results in marking $m^{\prime}$, denoted by
$(N,m)[t,\psi\rangle(N,m^{\prime})$, such that
$m^{\prime}(p)+\rho_{\psi}(\beta(p,t))=m(p)+\rho_{\psi}(\beta(t,p))$.
$\triangleleft$

The firing rule is inductively extended to sequences. A marking $m^{\prime}$
is _reachable_ from $m$ if there exists
$\eta\in(T\times(\mathcal{V}\rightarrow\mathcal{I}))^{*}$ such that
$(N,m)[\eta\rangle(N,m^{\prime})$. We denote with $\mathcal{R}(N,m)$ the set
of all markings reachable from $m$ for $\left(N,m\right)$. We use
$\mathcal{L}\left(N,m\right)$ to denote all possible firing sequences of
$\left(N,m\right)$, i.e.,
$\mathcal{L}\left(N,m\right)=\\{\eta\mid(N,m)[\eta\rangle{}\\}$ and
$Id(\eta)=\bigcup_{(t,\psi)\in\eta}\textsc{rng}(\psi)$ for the set of
identifiers used in $\eta$. The execution semantics of a t-PNID is defined as
an LTS that accounts for all possible executions starting from a given initial
marking. We say two t-PNIDs are bisimilar if their induced transition systems
are.

######  Definition 9.

Given a marked t-PNID $(N,m_{0})$ with $N=(P,T,F,\alpha,\beta)$, its induced
transition system is
$\Gamma_{N,m_{0}}=(\mathbb{M}(N),(T\times(\mathcal{V}\to\mathcal{I})),m_{0},\to)$
with $m\xrightarrow{(t,\psi)}m^{\prime}$ iff
$\left(N,m\right)[t,\psi\rangle\left(N,m^{\prime}\right)$. $\triangleleft$

Soundness properties for WF-nets typically consist of proper completion, weak
termination, and quasi-liveness [6]. Extending soundness to t-PNIDs gives
_identifier soundness_ [23]. In t-PNIDs, each object of a given type “enters”
the system through an emitting transition, binding it to a unique identifier.
Identifier soundness intuitively states that it should always be possible to
remove objects (weak type termination), and that once a collecting transition
fires for an object, there should be no remaining tokens referring to the
removed object (proper type completion).

######  Definition 10 (Identifier Soundness [23]).

Let $\left(N,m_{0}\right)$ a marked t-PNID and $\lambda\in\Lambda$ some type.
$\left(N,m_{0}\right)$ is _$\lambda$ -sound_ iff it is

  * •

Proper $\lambda$-completing, i.e., for all $t\in C_{N}(\lambda)$, bindings
$\psi:\mathcal{V}\to\mathcal{I}$ and markings
$m,m^{\prime}\in\mathcal{R}(N,m_{0})$, if $m[t,\psi\rangle m^{\prime}$, then
for all identifiers
$\mathtt{id}\in\textsc{rng}(\left.\psi\right|_{{\mathit{Collect}({t})}})\cap
Id(m)$ and $\mathtt{type}(\mathtt{id})=\lambda$, it holds that
$\mathtt{id}\not\in Id(m^{\prime})$ 111Here, we constrain $\psi$ only to
objects of type $\lambda$ that are only consumed.;

  * •

Weakly $\lambda$-terminating, i.e., for every $m\in\mathcal{R}(N,m_{0})$ and
identifier $\mathtt{id}\in I(\lambda)$ such that $\mathtt{id}\in Id(m)$, there
exists a marking $m^{\prime}\in\mathcal{R}(N,m)$ with $\mathtt{id}\not\in
Id(m^{\prime})$.

If it is $\lambda$-sound for all $\lambda\in\mathtt{type}(N)$, then it is
_identifier sound_. $\triangleleft$

###  3.3 Typed Jackson Nets

In general, identifier soundness is undecidable for t-PNIDs [23]. Similar as
Jackson Nets restrict WF-nets to blocks, _typed Jackson Nets_ (t-JNs) restrict
t-PNIDs to blocks, while guaranteeing identifier soundness and liveness. For
t-JNs, we disallow multiplicity on arcs and variables, i.e., $\beta(f)(v)\leq
1$ for all $f\in F$ and $v\in\mathcal{V}$, and imply a bijection on variables
and identifier types. This prevents place types like $\lambda=\left\langle
x,x\right\rangle$. Assuming a Gödel-like number on types (cf. [14]), place
types and arc inscriptions can be represented as sets. Similar as Jackson
Types describe Jackson Nets, we apply a notation based on Jackson Types to
denote typed Jackson Nets.

######  Definition 11 (Typed Jackson Net).

A t-PNID $N$ is a _typed Jackson Net_ if it can be generated from a set of
transitions $T^{\prime}$ by applying any of the following six generation rules
recursively. If $N$ is generated from a singleton set of transitions (i.e.,
$\left|{T^{\prime}}\right|=1$), $N$ is called _atomic_.

  1. R1

Place Expansion:
$\left[p,\lambda\right]\leftrightarrow\left(\left[p_{1},\lambda\right];\left(t_{1};\left[p_{2},\lambda\right]\right)\right)$

$p$$\nu$$\nu$$\nu$$\nu$$p_{1}$$t$$p_{2}$$\nu$$\nu$$\mu$$\mu$$\nu$$\nu$

  2. R2

Transition Expansion:
$t\leftrightarrow\left(t_{1};\left(\left[p,\lambda\right];t_{2}\right)\right)$,
with ${\mathit{Var}({t})}\subseteq\lambda$

$t$$\nu_{1}$$\nu_{2}$$\nu_{3}$$\nu_{4}$$t_{1}$$p$$t_{2}$$\nu_{1}$$\nu_{2}$$\mu$$\mu$$\nu_{3}$$\nu_{4}$

  3. R3

Place Duplication:
$\left(t_{1};\left(\left[p,\lambda\right];t_{2}\right)\right)\leftrightarrow\left(t_{1};\left(\left(\left[p,\lambda\right]\parallel\left[p^{\prime},\lambda^{\prime}\right]\right);t_{2}\right)\right)$,
with $\lambda^{\prime}\cap{\mathit{Emit}({{p}^{\bullet}})}=\emptyset$

$t_{1}$$p$$t_{2}$$\nu_{1}$$\nu_{2}$$\mu_{1}$$\mu_{2}$$\nu_{3}$$\nu_{4}$$t_{1}$$p$$p^{\prime}$$t_{2}$$\nu_{1}$$\nu_{2}$$\mu_{1}$$\mu_{2}$$\mu_{3}$$\mu_{4}$$\nu_{3}$$\nu_{4}$

  4. R4

Transition Duplication: $t\leftrightarrow\left(t+t^{\prime}\right)$

$t$$\nu_{1}$$\nu_{2}$$\mu_{1}$$\mu_{2}$$\nu_{3}$$\nu_{4}$$t$$t^{\prime}$$\nu_{1}$$\nu_{2}$$\mu_{1}$$\mu_{2}$$\mu_{1}$$\mu_{2}$$\nu_{3}$$\nu_{4}$

  5. R5

Self Loop Addition:
$\left[p,\lambda\right]\leftrightarrow\left(\left[p,\lambda\right]\\#t\right)$

$p$$\nu$$\nu$$\nu$$\nu$$p$$t$$\nu$$\nu$$\mu$$\mu$$\nu$$\nu$

  6. R6

Identifier Introduction:
$t\leftrightarrow\left(t\triangleleft\left(N_{1},\left[p,\lambda\right],N_{2}\right)\right)$,
with $\left(N_{1};\left(\left[p,\lambda\right];N_{2}\right)\right)$ a t-JN and
$\lambda\cap{\mathit{Var}({t})}=\emptyset$

$t$$\nu_{1}$$\nu_{2}$$\nu_{3}$$\nu_{4}$$t$$p$$t_{1}$$t_{2}$$\nu_{1}$$\nu_{2}$$\mu$$\mu$$\mu$$\mu$$\nu_{3}$$\nu_{4}$

$\triangleleft$

An example t-JN is given in Fig. 1. Starting with the product process,
transitions $C$ and $D$ can be reduced using rule $R2$. The resulting
transition is a self-loop transition, and can be reduced using $R5$, resulting
in the block $\left(E\triangleleft\left(A,\mathit{product},B\right)\right)$.
This block can be reduced using $R6$, leaving transition $E$. Transition $E$
is again a self-loop, and can be reduced using $R5$. The block containing
transitions $H$, $J$, $L$ $O$, $N$ and $K$ can be reduced to a single place by
applying rules $R1$, $R2$ and $R5$ repeatedly. The remaining place is a
duplicate place with respect to place $p$, and can be reduced using $R3$.
Applying $R2$ on $G$ and $Z$ results in the block
$\left(G\triangleleft\left(T,\mathit{customer},V\right)\right)$, which can be
reduced to the transition $G$. Hence, the net in Fig. 1 is an atomic t-JN.

######  Theorem 2 (Identifier Soundness of typed Jackson Nets [23]).

Given a t-JN $N$, then $N$ is _identifier sound_ and _live_. $\triangleleft$

##  4 Decomposability of t-JNs

t-PNIDs specify a class of nets with explicitly defined interactions between
objects of different types within one system. However, sometimes one may want
to focus only on some behaviors exhibited by a given set of object types, by
extracting a corresponding net from the original t-PNID model. We formalize
this idea below.

######  Definition 12 (Type projection).

Let $N=(P_{N},T_{N},F_{N},\alpha,\beta)$ be a t-PNID and
$\Upsilon\subseteq\Lambda$ be a set of identifier types. The _type projection_
of $\Upsilon$ on $N$ is a t-PNID
$\pi_{\Upsilon}\left(N\right)=(P_{\Upsilon},T_{\Upsilon},F_{\Upsilon},\alpha_{\Upsilon},\beta_{\Upsilon})$,
where:

  * •

$P_{\Upsilon}=\left\\{p\in P\mid\Upsilon\subseteq\alpha(p)\right\\}$;

  * •

$T_{\Upsilon}=\left\\{t\in T\mid({}^{\bullet}{t}\cup{t}^{\bullet})\cap
P\neq\emptyset\right\\}$;

  * •

$F_{\Upsilon}=F\cap((P_{\Upsilon}\times T_{\Upsilon})\cup(T_{\Upsilon}\times
P_{\Upsilon}))$;

  * •

$\alpha_{\Upsilon}(p)=\Upsilon$, for each $p\in P_{\Upsilon}$;

  * •

$\beta_{\Upsilon}(f)=\left.\beta(f)\right|_{\mathtt{type}_{\mathcal{V}}^{-1}(\Upsilon)}$,
for each $f\in((P_{\Upsilon}\times T_{\Upsilon})\cup(T_{\Upsilon}\times
P_{\Upsilon}))$.

$\triangleleft$

With the next lemma we explore a property of typed Jackson nets that, in a
nutshell, shows that t-JNs are closed under the type projection. This also
indirectly witnesses that t-JNs provide a suitable formalism for specifying
and manipulating systems with multiple communicating components.

######  Lemma 1.

If $N=(P_{N},T_{N},F_{N},\alpha,\beta)$ is a t-JN, then
$\pi_{\Upsilon}\left(N\right)$ is a t-JN as well, for any
$\Upsilon\subseteq\mathtt{type}_{\Lambda}(N)$. $\triangleleft$

######  Proof.

(sketch) Let us assume for simplicity that $N$ is atomic. Then, using rules
from Def. 11, $N$ can be reduced to a single transition. Starting from this
transition, one can construct a t-JN following the net graph construction from
Def. 12 using the same rules (but the identifier introduction one), proviso
that arc inscriptions are always of type $\Upsilon$. Then, it is easy to check
that the constructed net is indeed the type projection of $\Upsilon$ on $N$.

We define next how t-PNIDs can be composed and show that t-JNs are not closed
under the composition.

######  Definition 13 (Composition).

Let $N=(P_{N},T_{N},F_{N},\alpha_{N},\beta_{N})$ and
$M=(P_{M},T_{M},F_{M},\alpha_{M},\beta_{M})$ be two t-PNIDs. Their
_composition_ is defined by:

$N\uplus M=\left(P_{N}\cup P_{M},T_{N}\cup T_{M},F_{N}\cup
F_{M},\alpha_{N}\cup\alpha_{M},\beta_{N}\cup\beta_{M}\right)$

$\triangleleft$

$a$$p$$c$$q$$b$$r$$d$$x$$x$$x$$x$$x$$x$ (a) t-JN $N$

$a$$p$$b$$s$$c$$r$$d$$x$$x$$x$$x$$x$$x$ (b) t-JN $M$

$a$$p$$b$$s$$q$$c$$r$$d$$x$$x$$x$$x$$x$$x$$x$$x$ (c) t-PNID $N\uplus M$

Figure 4: Although both $N$ and $M$ are t-JNs, their composition is not

It is easy to see that the composition of two t-JNs does not automatically
result in a t-JN. Consider nets in Fig. 4. It is easy to see that both $N$ and
$M$ can be obtained by applying R2 from Def. 11. However, their composition
cannot be reduced to a single transition by consecutively applying rules from
Def. 11.

$a$$p_{x}$$p_{xy}$$p_{y}$$b$$c$$q_{x}$$q_{y}$$q_{xy}$$d$$x$$x$$x$$x$$x$$x$$y$$y$$y$$y$$y$$y$$xy$$xy$$xy$$xy$$xy$$xy$
Figure 5: Composition of the projections on $\left\\{\lambda_{1}\right\\}$,
$\left\\{\lambda_{2}\right\\}$ and $\left\\{\lambda_{1},\lambda_{2}\right\\}$
on the t-JN $(a;[p,\left\langle x,y\right\rangle];(b||c);[q,\left\langle
x,y\right\rangle];d)$. Here, type assignments are as follows:
$\alpha(p_{x})=\alpha(q_{x})=\lambda_{1}$,
$\alpha(p_{y})=\alpha(q_{y})=\lambda_{2}$ and
$\alpha(p)=\alpha(q)=\lambda_{1}\lambda_{2}$.

A more surprising observation is that composing type projections of a t-JN may
not result in a t-JN. Take for example the net from Figure 5. Both its
projections on $\left\\{\lambda_{1}\right\\}$ and
$\left\\{\lambda_{2}\right\\}$ are t-JNs. However, bringing them together
using the composition operator results in a t-PNID that is not t-JN: indeed,
since the “copies” of place $p$ appear in three places, and all such copies
have same pre- and post-sets (and only differ by their respective types), it
is impossible to apply identifier elimination rule _R6_ from Def. 11.

As one may observe from the above example, the only difference between
$[p_{xy},\left\langle\lambda_{1},\lambda_{2}\right\rangle]$ and its copies
$p_{x}$ and $p_{y}$ is in their respective types, whereas the identifiers
carried by $p_{x}$ and $p_{y}$ are always contained in $p_{xy}$, and thus both
$p_{x}$ and $p_{y}$ can be seen as subsidiary with respect to $p_{xy}$. We
formalize this observation using the notion of _minor places_ : a place $p$ is
minor to some place $q$ if both $p$ and $q$ have identical pre- and post-sets,
and the type of $q$ subsumes the one of $p$.

######  Definition 14 (Minor places).

Let $N=(P_{N},T_{N},F_{N},\alpha,\beta)$ be a t-PNID. A place $p\in P$ is
_minor to_ a place $q\in P$ iff the following holds:

  * •

${}^{\bullet}{p}={}^{\bullet}{q}$, ${p}^{\bullet}={q}^{\bullet}$ and
$\alpha(p)\subset\alpha(q)$;

  * •

$\beta((t,p))=\left.\beta((t,q))\right|_{\mathtt{type}^{-1}(\alpha(p))}$, for
each $t\in{}^{\bullet}{p}$;

  * •

$\beta((p,t))=\left.\beta((q,t))\right|_{\mathtt{type}^{-1}(\alpha(p))}$, for
each $t\in{p}^{\bullet}$.

$\triangleleft$

We show next that minor places can be added or removed without altering the
overall behavior of the net.

######  Lemma 2.

Let $N=(P,T,F,\alpha,\beta)$ be a t-PNID with initial marking $m_{0}$ s.t.
$m_{0}(p)=m_{0}(q)=\emptyset$, for $p,q\in P$, where $p$ is minor to $q$. Let
$N^{\prime}=(P\setminus\left\\{p\right\\},T,F\setminus(\left\\{(p,t)|t\in{p}^{\bullet}\right\\}\cup\left\\{(t,p)|t\in{}^{\bullet}{p}\right\\}),\alpha,\beta)$
be a t-PNID obtained by eliminating from $N$ place $p$ . Then
$\Gamma_{N,m_{0}}\sim^{r}\Gamma_{N^{\prime},m_{0}}$. $\triangleleft$

######  Proof.

(sketch) It is enough to define a relation
$Q\subseteq\mathcal{R}(N,m_{0})\times\mathcal{R}(N^{\prime},m_{0})$ s.t.
$(m,m^{\prime})\in Q$ iff $m(r)=m^{\prime}(r)$, for $r\in
P\setminus\left\\{p\right\\}$, and
$m(p)(\mathtt{id})=m^{\prime}(q)(\mathtt{id})$, for all
$\mathtt{id}\in\mathtt{C}(\mathit{p})$, and $|m(p)|=|m^{\prime}(q)|$. Then the
lemma statement directly follows from the firing rule of t-PNIDs and that pre-
and post-sets of $p$ and $q$ coincide.

$a$$c$$e$$b$$p$$d$$x$$x$$x$$x$$x$$x$$xy$$xy$$y$$y$$y$$y$ (a) t-PNID $N$ with
$\mathtt{type}(x)=\lambda_{1}$ and $\mathtt{type}(y)=\lambda_{2}$

$a$$c$$b$$p_{x}$$d$$x$$x$$x$$x$$x$$x$$x$$x$ (b) The projection of
$\left\\{\lambda_{1}\right\\}$ on $N$

$c$$e$$p_{y}$$d$$y$$y$$y$$y$$y$$y$ (c) The projection of
$\left\\{\lambda_{2}\right\\}$ on $N$

$a$$c$$e$$b$$p_{x}$$p_{y}$$d$$x$$x$$x$$x$$x$$x$$x$$y$$y$$y$$y$$y$$y$$y$ (d)
The composition of $\pi_{\left\\{\lambda_{1}\right\\}}\left(N\right)$ and
$\pi_{\left\\{\lambda_{2}\right\\}}\left(N\right)$

Figure 6: t-PNID $N$ (6(a)), its singleton projections and their composition

Let us now address the reconstructability property. In a nutshell, a net is
reconstructable if composing all of its type projections returns the same net.
This property is not that trivial to obtain. For example, let us consider
singleton projections (that is, projections
$\pi_{\left\\{\lambda\right\\}}\left(N\right)$ obtained for each
$\lambda\in\mathtt{type}_{\Lambda}(N)$) of the net in Fig. 6. It is easy to
see that such projections “ignore” interactions between objects (or system
components). Thus, the composition of the singleton projections
$\pi_{\left\\{\lambda_{1}\right\\}}\left(N\right)$ and
$\pi_{\left\\{\lambda_{2}\right\\}}\left(N\right)$ from Fig. 6 does not result
in a model that merges $p_{x}$ and $p_{y}$ in one place as the composition
operator cannot recognize component interactions between such projections.
This is reflected in Fig. 6(d).

To be able to reconstruct the original model from its projections (or at least
do it approximately well), one needs to consider a projection reflecting
component interactions. In the case of the net from Figure 6(a), its non-
singleton projection
$\pi_{\left\\{\lambda_{1},\lambda_{2}\right\\}}\left(N\right)$ is depicted in
Figure 7(a). Now, using this projection we can obtain a composition (see
Figure 7(b)) that closely resembles $N$. Notice that, in this composition,
copies of the interaction place $p$ appear three times as places $p_{x}$,
$p_{y}$ and $p_{xy}$, respectively. It is also easy to see that places $p_{x}$
and $p_{y}$ are minor to $p_{xy}$, and $\alpha(p)=\alpha(p_{xy})$ witnesses
that $\pi_{\left\\{\lambda_{1},\lambda_{2}\right\\}}\left(N\right)$ is the
maximal projection defined over types of $N$ s.t. the correct type of $p$ is
“reconstructed”. This leads us to the following result stipulating the
reconstructability property of typed Jackson nets.

$c$$p_{xy}$$d$$xy$$xy$ (a) The projection of
$\left\\{\lambda_{1},\lambda_{2}\right\\}$ on $N$ from Figure 6(a)

$a$$c$$e$$b$$p_{x}$$p_{y}$$p_{xy}$$d$$x$$x$$x$$x$$x$$x$$x$$y$$xy$$xy$$y$$y$$y$$y$$y$$y$
(b) The composition
$\pi_{\left\\{\lambda_{1}\right\\}}\left(N\right)\uplus\pi_{\left\\{\lambda_{2}\right\\}}\left(N\right)\uplus\pi_{\left\\{\lambda_{1},\lambda_{2}\right\\}}\left(N\right)$
for $N$ from Figure 6(a)

Figure 7: Adding the projection
$\pi_{\left\\{\lambda_{1},\lambda_{2}\right\\}}\left(N\right)$ reflecting
interactions to the composition results in the original net $N$ modulo places
minor to $p$ (such as $p_{x}$ and $p_{y}$).

######  Theorem 3.

Let $N=(P,T,F,\alpha,\beta)$ be a t-JN. Then
$\Gamma_{N,\emptyset}\sim^{r}\Gamma_{N^{\prime},\emptyset}$, where
$N^{\prime}=\biguplus\limits_{\emptyset\subset\Upsilon\subseteq\mathtt{type}_{\Lambda}(N)}\pi_{\Upsilon}\left(N\right)$.
$\triangleleft$

######  Proof.

(sketch) The proof immediately follows from the next observation. Among all
possible projections, for each place $p\in P$ there exists a projection
$\pi_{\Upsilon}\left(N\right)$ such that $\alpha(p)=\Upsilon$. This also means
that $\pi_{\Upsilon}\left(N\right)$ contains $p$ and that all other
projections $\pi_{\Upsilon^{\prime}}\left(N\right)$ with
$\Upsilon^{\prime}\subset\Upsilon$ will at most include the minors of $p$.
Following Def. 13, it is easy to see that the composition of all the
projections yields a t-JN identical to $N$ modulo additional place minors
introduced by some of the projections. Showing that the obtained net is
bisimilar to $N$ can be done by analogy with Lemma 2.

Notice that the above result can be made stronger if all the additional minors
(i.e., minors that were not present originally in $N$) are removed using
reduction rules from Def. 11. For simplicity, given a t-PNID $N$ with the set
of places $P$, we denote by $\lfloor P\rfloor$ the set of its minor places.

######  Corollary 1.

Let $N$ be a t-JN and $N^{\prime}$ is as in Thm. 3. Then
$(N,\emptyset)\leftrightsquigarrow(N^{\prime},\emptyset)$, if $\lfloor
P\rfloor=\lfloor P^{\prime}\rfloor$, where $P$ and $P^{\prime}$ are
respectively the sets of places of $N$ and $N^{\prime}$. $\triangleleft$

The above result can be obtained by complementing the proof of Thm. 3 with a
step that applies finitely many t-JN reduction rules to all the minor places
that are in $N^{\prime}$ and not in $N$.

##  5 A Framework for Rediscoverability

In the previous section, we showed that t-JNs enjoy the reconstructability
property: given a t-JN, a composition of _all_ its (proper) type projections
yields a t-JN that is strongly bisimilar to the original one.222Such nets are
also isomorphic if minor places of the composition are removed by
consecutively applying the reduction rules from Def. 11.

In this section, we propose a framework to rediscover systems of interacting
processes that rely on this property. The framework builds upon a divide and
conquer strategy [21]. The first step of the approach is to divide the event
logs over all possible projections. For this, we translate the notion of event
logs to event logs of interacting systems, and show that if these event logs
are generated by a t-JN, projections on these event logs have a special
property: the projected event log can be replayed by the projected net. In
other words, there is no distinction between the projection on the event log,
or that the projected net generated the event log. This observation forms the
basis of the proposed framework for rediscoverability. In the second step, we
conquer the discoverability problem of the system of interacting processes by
first discovering a model for each of the projections, and then composing
these projections into the original system. If the event log and discovery
algorithm guarantee the defined properties, composition yields
rediscoverability.

###  5.1 Event Logs and Execution Traces

In process discovery, an event log is represented as a (multi)set of sequences
of events (called traces), where each sequence represents an execution history
of a process instance. Traditional process discovery assumes the process to be
a WF-net. Consequently, each trace in an event log should correspond to a
sequence of transition firings of the workflow net. If this is the case, the
event log is said to be generated by the WF-net. We generalize this notion to
marked Petri nets.

######  Definition 15 (Event Log).

Given a set of transitions $T$, a set of traces $L\subseteq{T}^{*}$ is called
an _event log_. An event log $L$ _is generated by_ a marked Petri net $(N,m)$
if $(N,m)[\sigma\rangle{}$ for all $\sigma\in L$, i.e.,
$L\subseteq\mathcal{L}(N,m_{0})$. $\triangleleft$

Table 1: Firing sequence for the t-PNID in Fig. 1

transition | x | y | z
---|---|---|---
$A$ | $p1$ |  |
$A$ | $p2$ |  |
$T$ |  |  | $c1$
$G$ |  | $o1$ | $c1$
$C$ | $p1$ |  |
$E$ | $p2$ | $o1$ |

transition | x | y | z
---|---|---|---
$T$ |  |  | $c2$
$H$ |  | $o1$ |
$L$ |  | $o1$ |
$J$ |  | $o1$ |
$B$ | $p2$ |  |
$O$ |  | $o1$ |

transition | x | y | z
---|---|---|---
$D$ | $p1$ |  |
$V$ |  |  | $c2$
$K$ |  | $o1$ |
$Z$ |  | $o1$ | $c1$
$V$ |  |  | $c1$
$B$ | $p1$ |  |

Each sequence in a single process event log assumes to start from the initial
marking of the WF-net. A marked t-PNID, instead, represents a continuously
executing system, for which, given a concrete identifier, exists a single
observable execution that can be recorder in an event log. Thus, event logs
are partial observations of a larger execution within the system: an event log
for a certain type captures only the relevant events that contain identifiers
of that type, and stores these in order of their execution. Since each
transition firing consists of a transition and a binding, a t-PNID firing
sequence induces an event log for each set of types $\Upsilon$. Intuitively,
this induced event log is constructed by a filtering process. For each
possible identifier vector for $\Upsilon$ we keep a firing sequence. Each
transition firing is inspected, and if its binding satisfies an identifier
vector of $\Upsilon$, it is added to the corresponding sequence.

######  Definition 16 (Induced Event Log).

Let $(N,m_{0})$ be a marked t-PNID. Given a non-empty set of types
$\Upsilon\subseteq\mathtt{type}_{\Lambda}(N)$, the _$\Upsilon$ -induced event
log_ of a firing sequence $\eta\in\mathcal{L}(N,m_{0})$ is defined by:
$\mathit{Log}_{\Upsilon}(\eta)=\\{{\eta}_{{\mid{i}}}\mid i\in(Id(\eta)\cap
I(\Upsilon))^{\left|{\Upsilon}\right|}\\}$,where ${\eta}_{{\mid{i}}}$ is
inductively defined by  (1) ${\epsilon}_{{\mid{i}}}=\epsilon$,  (2)
${(\left\langle(t,\psi)\right\rangle\cdot\eta)}_{{\mid{i}}}=\left\langle(t,\psi)\right\rangle\cdot{\eta}_{{\mid{i}}}$if
$\mathit{supp}(i)\subseteq\textsc{rng}(\psi)$, and  (3)
${(\left\langle(t,\psi)\right\rangle\cdot\eta)}_{{\mid{i}}}={\eta}_{{\mid{i}}}$otherwise.
$\triangleleft$

Different event logs can be induced from a firing sequence. Consider, for
example, the firing sequence of the net from Fig. 1 represented as table in
Tbl. 1. As we cannot deduce the types for each of the variables from the
firing sequences in Tbl. 1, we assume that there is a bijection between
variables and types, i.e., that each variable is uniquely identified by its
type, and vice-versa. Like that, we can create an induced log for each
variable, as the type and variable name are interchangeable. For example, the
$x$-induced event log is $\mathit{Log}_{\\{x\\}}=\\{\left\langle
A,E,B\right\rangle,\left\langle A,C,D,B\right\rangle\\}$, and the $z$-induced
event log is $\mathit{Log}_{\\{z\\}}=\\{\left\langle
T,G,Z,V\right\rangle,\left\langle T,V\right\rangle\\}$. Similarly, event logs
can be also induced for combinations of types. In this example, the only non-
empty induced event logs on combined types are
$\mathit{Log}_{\\{y,z\\}}=\\{\left\langle G,Z\right\rangle\\}$ and
$\mathit{Log}_{\\{x,y\\}}=\\{\left\langle E\right\rangle\\}$.

As the firing sequence in Tbl. 1 shows, transition firings (and thus also
events) only show bindings of variables to identifiers. For example, for
firing $G$ with binding $y\mapsto o1$ and $z\mapsto c1$, it is not possible to
derive the token types of the consumed and produced tokens directly from the
table. Therefore, we make the following assumptions for process discovery on
t-PNIDs:

  1. 1.

There are no “black” tokens: all places carry tokens with at least one type,
and all types occur at most once in a place type, i.e., all places refer to at
least one process instance.

  2. 2.

There is a bijection between variables and types, i.e., for each type exactly
one variable is used.

  3. 3.

A Gödel-like number $\mathscr{G}$ is used to order the types in place types,
i.e., for any place $p$, we have
$\mathscr{G}(\alpha(p)(i))<\mathscr{G}(\alpha(p)(j))$ for $1\leq
i<j\leq\left|{\alpha(p)}\right|$ and $p\in P$.

###  5.2 Rediscoverability of Typed Jackson Nets

Whereas traditional process discovery approaches relate events in an event log
to a single object: the process instance, object-centric approaches can relate
events to many objects [11]. Most object-centric process discovery algorithms
(e.g., [5, 17]) use a divide and conquer approach, where “flattening” is the
default implementation to divide the event data in smaller event logs. The
flattening operation creates a trace for each object in the data set, and
combines the traces of objects of the same type in an event log. As we have
shown in Section 4, singleton projections, i.e., those just considering types
in isolation, are insufficient to reconstruct the t-JN that induced the
object-centric event log. A similar observation is made for object-centric
process discovery (cf. [3, 5, 7]): flattening the event data into event logs
generates inaccurate models. Instead, reconstructability can only be achieved
if all possible combinations of types are considered. Hence, for a divide and
conquer strategy, the divide step should involve all possible combinations of
types, i.e., each interaction between processes requires their own event log.
In the remainder of this section, we show that if all combinations of types
are considered, flattening is possible, and traditional process discovery
algorithms can be used to rediscover a system of interacting processes.

For a system of interacting processes, we consider execution traces, i.e., a
firing sequence from the initial marking. Like that, event logs for specific
types or combinations of types are induced from the firing sequence. The
projection of the system on a type or combinations of types, results again in
a t-JN. Similarly, if we project a firing sequence of a t-JN $N$ on a set of
types $\Upsilon$, then this projection is a firing sequence of the
$\Upsilon$-projection on $N$. The property follows directly from the result
that t-JN $N$ is weakly simulated by its $\Upsilon$-projection.

######  Lemma 3.

Let $N$ be a t-JN, and let $\Upsilon\subseteq\mathtt{type}_{\Lambda}(N)$. Then
$\hat{\mathtt{H}}_{U}(\Gamma_{N,\emptyset})\preccurlyeq^{r}\Gamma_{\pi_{\Upsilon}\left(N\right),\emptyset}$,
with $U=T_{N}\setminus T_{\Upsilon}$. $\triangleleft$

######  Proof.

(sketch) Let
$N_{\Upsilon}={\Upsilon}_{{\mid{N}}}=(P_{\Upsilon},T_{\Upsilon},F_{\Upsilon},\alpha_{\Upsilon},\beta_{\Upsilon})$.
We can define a relation
$Q\subseteq\mathbb{M}\left(N\right)\times\mathbb{M}\left(\pi_{\Upsilon}\left(N\right)\right)$
s.t. $Q(m)(p)({a}_{{\mid{I(\Upsilon)}}})=m(p)(a)$ if $p\in P_{\Upsilon}$ and
$Q(m)(p)=m(p)$ otherwise. The rooted weak bisimulation of $Q$ follows directly
from the firing rule of t-PNIDs.

As the lemma shows, projecting a firing sequence yields a firing sequence for
the projected net. A direct consequence of the simulation relation is that, no
matter whether we induce an event log from a firing sequence on the original
net, or induce it from the projected firing sequence, the resulting event logs
are the same.

######  Corollary 2.

Let $(N,m_{0})$ be a marked t-PNID. Given a set of types
$\Upsilon\subseteq\mathtt{type}_{\Lambda}(N)$. Then
$\mathit{Log}_{\Upsilon}(\eta)=\mathit{Log}_{\Upsilon}(\pi_{\Upsilon}\left(\eta\right))$.
$\triangleleft$

Hence, it is not possible to observe whether an induced event log stems from
the original model, or from its projection. Note that the projection may
exhibit more behavior, so the reverse does not hold. In general, not any
induced event log from the projection can be induced from the original model.

In general, a projection does not need to be an atomic t-JN (that is, a t-JN
that can be reduced by applying rules from Def. 11 to a single transition).
However, if the projection is atomic, then its structure is a transition-
bordered WF-net: a WF-net that, instead of having source and sink places, has
a set of start and finish transitions, such that pre-sets (resp., post-sets)
of start (resp., finish) transitions are empty. The closure of a transition-
bordered WF-net is constructed by adding a new source place $i$ so that each
start transition consumes from $i$, and a new sink place $f$ so that each
finish transition produces in $f$.

$M$$M_{1}$$\cdots$$M_{n}$$M^{\prime}$$L$$L_{1}$$\cdots$$L_{n}$$D_{1}$$\cdots$$D_{n}$$D^{\prime}$$\pi$$\pi$$\uplus$$\uplus$$\sim^{r}$$\overline{\mathit{disc}}$$\overline{\mathit{disc}}$
Figure 8: Framework for rediscoverability of typed Jackson Nets. Model $M$
generates an event log $L$. Log projections $L_{1}\ldots L_{n}$ are generated
from projected nets $M_{1}\ldots M_{n}$. Discovery algorithm $\mathit{disc}$
results in nets $D_{1}\ldots D_{n}$, isomorphic to $M_{1}\ldots M_{n}$, which
can be composed in $D^{\prime}$. $D^{\prime}$ is isomorphic to $M^{\prime}$
and thus to $M$.

######  Lemma 4.

Let $N$ be a t-JN and
$\pi_{\Upsilon}\left(N\right)=(P_{\Upsilon},T_{\Upsilon},F_{\Upsilon},\alpha_{\Upsilon},\beta_{\Upsilon})$
for some $\Upsilon\subseteq\mathtt{type}_{\Lambda}(N)$ such that
$\pi_{\Upsilon}\left(N\right)$ is atomic. Let
$\eta\in\mathcal{L}(N,\emptyset)$ be a firing sequence. Then
$\mathit{Log}_{\Upsilon}(\eta)$ is generated by $(N_{\Upsilon},\emptyset)$
with
$N_{\Upsilon}=(P_{\Upsilon}\cup\\{i,f\\},T_{\Upsilon},F_{\Upsilon}\\{(i,t)\mid{}^{\bullet}{t}=\emptyset\\}\cup\\{(t,f)\mid{t}^{\bullet}=\emptyset\\})$.
$\triangleleft$

######  Proof.

(sketch) Let $\sigma\in\mathit{Log}_{\Upsilon}(\eta)$. By construction, each
firing sequence in $\mathit{Log}_{\Upsilon}(\eta)$ has some corresponding
identifier vector that generated the sequence. Assume
$\vec{\upsilon}\in\mathcal{I}^{|\Upsilon|}$ is such a vector for $\sigma$.

Observe that for any transition $t\in T$ if ${}^{\bullet}{t}=\emptyset$,
${\mathit{Emit}({t})}\cap\Upsilon\neq\emptyset$, and similarly, if
${t}^{\bullet}=\emptyset$, ${\mathit{Collect}({t})}\cap\Upsilon\neq\emptyset$.
As $N$ is identifier sound, only ${}^{\bullet}{\sigma(1)}=\emptyset$ and
${\sigma(\left|{\sigma}\right|)}^{\bullet}=\emptyset$. Define relation
$R=\\{(M,m)\mid\forall p\in P:M(p)(\upsilon)=m(p)\\}$ and
$U=\\{(t,\psi)\mid\upsilon\not\subseteq\textsc{rng}(\psi)\\}$, i.e., $U$
contains all transitions that do not belong to $\sigma$. Then $R$ is a weak
simulation, i.e.,
$\hat{\mathtt{H}}_{U}(\Gamma_{N,\emptyset})\preccurlyeq^{r}_{R}\Gamma_{N_{\Upsilon},\emptyset}$
and thus $(N_{\Upsilon},\emptyset)[\sigma\rangle$.

Given a set of types $\Upsilon$, if its projection is atomic, the projection
can be transformed into a workflow net, and for any firing sequence of the
original net, this WF-net can generate the $\Upsilon$-induced event log.
Suppose we have a discovery algorithm $\mathit{disc}$ that can rediscover
models, i.e., given an event log $L$ that was generated by some model $M$,
then $\mathit{disc}$ returns the original model. Rediscoverability of an
algorithm requires some property $P_{\mathit{disc}}(M)$ on the generating
model $M$, and some property $Q_{\mathit{disc}}(L,M)$ on the quality of event
log $L$ with respect to the generating model $M$. In other words, $P(M)$ and
$Q(L,M)$ are premises to conclude rediscoverability for discovery algorithm
$\mathit{disc}$. For example, $\alpha$-miner [22] requires for $P(M)$ that
model $M$ is well-structured, and for $Q(L,M)$ that event log $L$ is directly-
follows complete with respect to model $M$. Similarly, Inductive Miner [16]
requires the generating model $M$ to be a process tree without silent actions
or self-loops ($P(M)$), and that event log $L$ is directly-follows complete
with respect to the original model $M$ ($Q(L,M)$).

######  Definition 17 (Rediscovery).

An algorithm $\mathit{disc}$ can _rediscover_ WF-net $W=(P,T,F,in,out)$ from
event log $L\subseteq{T}^{*}$ if $P_{\mathit{disc}}(W)$ and
$Q_{\mathit{disc}}(L,W)$ imply $\mathit{disc}(L)\leftrightsquigarrow W$.
$\triangleleft$

Thus, suppose there exists a discovery algorithm $\mathit{disc}$ that is –
under conditions $P$ and $Q$ – able to reconstruct a workflow model given an
event log. In other words, given an event log $L$ generated by some model $M$,
$\mathit{disc}$ returns a model that is isomorphic to the generating model.
Now, suppose we have a firing sequence $\eta$ of some t-JN $N$, and some
projection $\Upsilon$. Then, if $P(\pi_{\Upsilon}\left(N\right))$, and
$Q(\mathit{Log}_{\Upsilon}(\eta),\pi_{\Upsilon}\left(N\right))$, then
$\mathit{disc}$ returns a model that is isomorphic to the closure of
$\pi_{\Upsilon}\left(N\right)$, as $\mathit{disc}$ only returns WF-nets. With
$\overline{\mathit{disc}}$ we denote the model where the source and sink
places are removed, i.e.,
$\overline{\mathit{disc}}\leftrightsquigarrow\pi_{\Upsilon}\left(N\right)$.
Then, as shown in Fig. 8, if we discover for every possible combination of
types, i.e., the subset-closed set of all type combinations, a model that is
isomorphic to the type-projected model, then the composition results in a
model that is bisimilar to the original model.

######  Theorem 4 (Rediscoverability of typed Jackson Nets).

Let $N$ be a t-JN, and let $\eta\in\mathcal{L}(N,\emptyset)$ without minor
places. Let $\mathit{disc}$ be a discovery algorithm with properties $P$ and
$Q$ that satisfy Def. 17. If for all
$\emptyset\subset\Upsilon\subseteq\mathtt{type}_{\Lambda}(N)$ the
$\Upsilon$-projection is atomic and satisfies conditions
$P(\pi_{\Upsilon}\left(N\right))$ and
$Q(\mathit{Log}_{\Upsilon}(\eta)),\pi_{\Upsilon}\left(N\right))$, then
$\Gamma_{N,\emptyset}\leftrightsquigarrow\Gamma_{N^{\prime},\emptyset}$ with
$N^{\prime}=\biguplus_{\emptyset\subset\Upsilon\subseteq\mathtt{type}_{\Lambda}(N)}\overline{\mathit{disc}}(\mathit{Log}_{\Upsilon}(\eta))$.

$\triangleleft$

######  Proof.

(sketch) Let $\emptyset\subset\Upsilon\subseteq\mathtt{type}_{\Lambda}(N)$ be
a set of types in $N$. Since $P(\pi_{\Upsilon}\left(N\right))$ and
$Q(\mathit{Log}_{\Upsilon}(\eta)),\pi_{\Upsilon}\left(N\right))$the closure of
$\pi_{\Upsilon}\left(N\right)$ and
$\mathit{disc}(\mathit{Log}_{\Upsilon}(\eta))$ are isomorphic. From the
closure, places $\mathit{in}$ and $\mathit{out}$ exist with
${}^{\bullet}{\mathit{in}}=\emptyset={\mathit{out}{}}^{\bullet}$. As the nets
are isomorphic, we have
${\Upsilon}_{{\mid{N}}}\leftrightsquigarrow\overline{\mathit{disc}}(\mathit{Log}_{\Upsilon}(\eta))$.
Combining the results gives
$\biguplus_{\emptyset\subset\Upsilon\subseteq\mathtt{type}_{\Lambda}(N)}\overline{\mathit{disc}}(\mathit{Log}_{\Upsilon}(\eta))\leftrightsquigarrow\biguplus_{\emptyset\subset\Upsilon\subseteq\mathtt{type}_{\Lambda}(N)}\pi_{\Upsilon}\left(N\right)$.
The statement then follows directly from Cor. 1.

##  6 Conclusion

In this paper, we studied typed Jackson Nets to model systems of interacting
processes, a class of well-structured process models describing manipulations
of object identifiers. As we show, this class of nets has an important
property of reconstructability. In other words, the composition of the
projections on all possible type combinations returns the model of the
original system. Ignoring the interactions between processes results in less
accurate, or even wrong, models. Similar problems occur in the discovery of
systems of interacting processes, such as object-centric process discovery,
where event logs are flattened for each object.

This paper provides a formal foundation for the composition of block-
structured nets, and uses this to develop a framework for the discovery of
systems of interacting processes. We link the notion of event logs used for
process discovery to system executions, and show that it is not possible to
observe whether an event log is generated by a system of interacting
processes, or by a projection of the system. These properties form the key
ingredients of the framework. We show under what conditions a process
discovery algorithm (that guarantees rediscoverability) can be used to
discover the individual processes and their interactions, and how these can be
combined to rediscover a model of interacting processes that is bisimilar to
the original system that generated the event logs.

Although typed Jackson Nets have less expressive power than formalisms like
Object-centric Petri nets [5], proclets [10] or interacting artifacts [17],
this paper shows the limitations and potential pitfalls of discovering
interacting processes. This work aims to lay formal foundations for object-
centric process discovery. As a next step, we plan to implement the framework
and tune our algorithms to discover useful models from industrial datasets.

Acknowledgements. Artem Polyvyanyy was in part supported by the Australian
Research Council project DP220101516.

## References

  * [1] van der Aalst, W.M.P.: Workflow verification: Finding control-flow errors using petri-net-based techniques. In: Lecture Notes in Computer Science, pp. 161–183. Springer Berlin Heidelberg (2000). https://doi.org/10.1007/3-540-45594-9_11, https://doi.org/10.1007/3-540-45594-9%5F11
  * [2] van der Aalst, W.M.P.: Verification of workflow nets. In: Petri Nets. LNCS, vol. 1248, pp. 407–426. Springer (1997). https://doi.org/10.1007/3-540-63139-9_48
  * [3] van der Aalst, W.M.P.: Object-centric process mining: Dealing with divergence and convergence in event data. In: SEFM 2019. pp. 3–25. No. 11724 in LNCS, Springer (2019)
  * [4] van der Aalst, W.M.P.: Foundations of process discovery. In: Process Mining Handbook. LNBIP, vol. 448. Springer (2022)
  * [5] van der Aalst, W.M.P., Berti, A.: Discovering object-centric petri nets. Fundamenta Informaticae 1–4(175), 1–40 (2020)
  * [6] van der Aalst, W.M.P., van Hee, K.M., ter Hofstede, A.H.M., Sidorova, N., Verbeek, H.M.W., Voorhoeve, M., Wynn, M.T.: Soundness of workflow nets: classification, decidability, and analysis. Formal Asp. Comput. 23(3), 333–363 (2011)
  * [7] Adams, J.N., Park, G., Levich, S., Schuster, D., van der Aalst, W.M.P.: A framework for extracting and encoding features from object-centric event data. In: ICSOC 2022. pp. 36–53. No. 13740 in LNCS, Springer (2022)
  * [8] Berti, A., van der Aalst, W.M.P.: OC-PM: analyzing object-centric event logs and process models. International Journal on Software Tools for Technology Transfer (Sep 2022). https://doi.org/10.1007/s10009-022-00668-w, https://doi.org/10.1007/s10009-022-00668-w
  * [9] Best, E., Devillers, R., Koutny, M.: The box algebra=petri nets+process expressions. Information and Computation 178(1), 44–100 (oct 2002). https://doi.org/10.1006/inco.2002.3117, https://doi.org/10.1006/inco.2002.3117
  * [10] Fahland, D.: Describing behavior of processes with many-to-many interactions. In: Application and Theory of Petri Nets and Concurrency, pp. 3–24. Springer International Publishing (2019). https://doi.org/10.1007/978-3-030-21571-2_1, https://doi.org/10.1007/978-3-030-21571-2%5F1
  * [11] Ghahfarokhi, A.F., Park, G., Berti, A., van der Aalst, W.M.P.: OCEL: A standard for object-centric event logs. In: ADBIS 2021. CCIS, vol. 1450, pp. 169–175. Springer (2021)
  * [12] van Glabbeek, R.J.: The linear time — branching time spectrum II. In: CONCUR'93, pp. 66–81. Springer Berlin Heidelberg (1993). https://doi.org/10.1007/3-540-57208-2_6, https://doi.org/10.1007/3-540-57208-2%5F6
  * [13] van Hee, K., Sidorova, N., Voorhoeve, M.: Soundness and separability of workflow nets in the stepwise refinement approach. In: Applications and Theory of Petri Nets 2003, pp. 337–356. Springer Berlin Heidelberg (2003). https://doi.org/10.1007/3-540-44919-1_22, https://doi.org/10.1007/3-540-44919-1%5F22
  * [14] van Hee, K.M., Hidders, J., Houben, G.J., Paredaens, J., Thiran, P.: On the relationship between workflow models and document types. Information Systems 34(1), 178–208 (Mar 2009). https://doi.org/10.1016/j.is.2008.06.003, https://doi.org/10.1016/j.is.2008.06.003
  * [15] Kopp, O., Martin, D., Wutke, D., Leyman, F.: The difference between graph-based and block-structured business process modelling languages. EMISAJ 4(1), 3–13 (2009)
  * [16] Leemans, S.J.J., Fahland, D., van der Aalst, W.M.P.: Discovering block-structured process models from event logs - a constructive approach. In: Application and Theory of Petri Nets and Concurrency, pp. 311–329. Springer Berlin Heidelberg (2013). https://doi.org/10.1007/978-3-642-38697-8_17, https://doi.org/10.1007/978-3-642-38697-8%5F17
  * [17] Lu, X., Nagelkerke, M., van de Wiel, D., Fahland, D.: Discovering interacting artifacts from ERP systems. IEEE Trans. Serv. Comput. 8(6), 861–873 (2015)
  * [18] Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (Apr 1989). https://doi.org/10.1109/5.24143, https://doi.org/10.1109/5.24143
  * [19] Polyvyanyy, A., van der Werf, J.M.E.M., Overbeek, S., Brouwers, R.: Information systems modeling: Language, verification, and tool support. In: CAiSE. Lecture Notes in Computer Science, vol. 11483, pp. 194–212. Springer (2019)
  * [20] Tour, A., Polyvyanyy, A., Kalenkova, A.A.: Agent system mining: Vision, benefits, and challenges. IEEE Access 9, 99480–99494 (2021)
  * [21] Tour, A., Polyvyanyy, A., Kalenkova, A.A., Senderovich, A.: Agent miner: An algorithm for discovering agent systems from event data. CoRR abs/2212.01454 (2022)
  * [22] van der Aalst, W., Weijters, T., Maruster, L.: Workflow Mining: Discovering Process Models from Event Logs. Knowledge & Data Engineering 16(9), 1128–1142 (2004)
  * [23] van der Werf, J.M.E.M., Rivkin, A., Polyvyanyy, A., Montali, M.: Data and process resonance. In: Application and Theory of Petri Nets and Concurrency, pp. 369–392. Springer International Publishing (2022). https://doi.org/10.1007/978-3-031-06653-5_19, https://doi.org/10.1007/978-3-031-06653-5%5F19