11institutetext: 1HSE University (Russia)
2Faculty of Computer Science, Free University of Bozen-Bolzano (Italy)

# Soundness in Object-centric Workflow Petri Nets

Irina A. Lomazova1 Alexey A. Mitsyuk1 Andrey Rivkin2

###### Abstract

Recently introduced Petri net-based formalisms advocate the importance of
proper representation and management of case objects as well as their co-
evolution. In this work we build on top of one of such formalisms and
introduce the notion of soundness for it. We demonstrate that for nets with
non-deterministic synchronization between case objects, the soundness problem
is decidable.

##  1 Introduction

Traditional workflow nets often focus on a single case in isolation. However,
in reality, the notion of a case is often more complex and may consist of
multiple simultaneously “active” objects with complex inter-relations. This
issue has been already recognized and addressed in various works. Among such,
the seminal work on workflow patterns [6] with the related multiple instance
patterns, works on proclets [2, 3], in which the authors studied interactions
between multiple workflows.

When it comes to analyzing such nets, it is often assumed that, even in the
presence of multiple, simultaneously active process instances each of which
has its own lifecycle, the global system state is composed of their individual
(local) states that, in turn, are rarely addressed in isolation. This becomes
evident when analyzing the process correctness using the concept of soundness.
In the nutshell, the process is called sound if and only if any reachable
process state, starting from its initial configuration, can properly terminate
by reaching the final process configuration without leaving any intermediate
process resources unused. Such soundness requires that the system model has
clearly defined start and end points, and focuses only on the global
termination. This also implies that the model must have a clearly defined
“global” lifecycle, forcing all the lifecycles it embeds to synchronize on the
aforementioned global start and end points.

This assumption is quite common in practice, but it cannot capture a more
complex setting in which, instead of the global lifecyle, one models an
environment or a protocol without clearly defined global start and end points,
and with process instances whose own lifecycles are treated as “first class
citizens” (and thus their local termination comes to the fore). An example of
such setting can be easily found in higher education, where process models can
represent the whole educational lifecycle of a student of more refined
scenarios such as work on a project for some course. Notice that such models
can include multiple, possibly interacting participants (that is, active
cases) and one might be interested in the proper completion only of one of
them. Like that the concept of the global state becomes redundant as each
single case can be treated in isolation. All this calls for a new notion of
soundness that is not based on global, terminal states.

In this work, we address the aforementioned scenario by using the recently
proposed formalism of object-centric Petri nets [4] – a weak variant of
colored Petri nets enriched with a special kind of transfer arcs. Using such
nets, one can easily represent lifecycles of multiple objects and define their
local start and end points. By drawing inspiration from multi-agent systems,
where each agent is represented with a separate workflow and its successful
completion in isolation can happen irrespectively from other workflows, we
introduce a new notion of soundness. There, we focus on local terminal states
only, assuming that a system can have any number of participants being
simultaneously active. We propose constructive techniques for isolating
behaviors of interest without alternating the global process behavior and
introduce a new notion of soundness that focuses on an individual object
lifecyle, treating all other objects as its environment. Moreover, we
conjecture that checking this new variant of soundness is decidable.

##  2 Motivating example

We start by discussing an example that illustrates issues arising when one
wants to model an environment consisting of multiple lifecycles and touches
upon main ideas that we develop later on in our proposal. The example in
Figure 1 models a project work scenario in a university. There, all three
workflow nets model behaviors of three different entities (or objects): a
project team leader, a project team member and a project. Both project team
leaders and members are students. Projects are performed in small teams each
of which consists of three students: one team leader and two team members.

In Figure 1, separate entities are modeled using ordinary WF-nets. Figure 1(a)
shows a workflow of a team member. Figure 1(b) illustrates how a team leader
behaves. Project itself has its own prescribed sequence of key milestones.
These make up a process workflow that is shown in Figure 1(c). Let us consider
behavior of separate entities in more detail.

$pm_{1}$$join1$$join2$$pm_{2}$$attend\ i.\ m.$$pm_{3}$$submit\
m.$$discuss$$back$$pm_{d}$$present\
project$$repeat$$pm_{4}$$complete$$fail$$pm_{5}$

(a) Team member

$pl_{1}$$create$$pl_{2}$$start$$pl_{3}$$attend\ i.\ m.$$pl_{4}$$submit\
m.$$discuss$$back$$pl_{d}$$present\
project$$pl_{5}$$repeat$$complete$$fail$$pl_{6}$

(b) Team leader

$p_{1}$$create$$p_{2}$$p_{3}$$join1$$join2$$p_{4}$$p_{5}$$start$$p_{6}$$submit\
m.$$\tau$$p_{7}$$complete$$fail$$p_{8}$

(c) Project workflow

Figure 1: Three different types of objects from the university project work
scenario

We will begin from the project workflow shown in Figure 1(c). Firstly, the
project has to be $create$d. It is done by a student who was chosen to be a
team leader. Student can start working on a project if there are three members
in their team. Thus, two team members have to $join$ to as soon as the team
was created. After this the students can start working on their project (this
decision is taken by the team leader). From project point of view, the team
has to $submit$ part of the solution to supporting learning environment at
least once. There can be multiple submissions as well. Then, the project
finishes either by successful $complet$etion or by $fail$ure.

Let us consider now how student members behave. One may notice similarities
between models in Figure 1(a) and Figure 1(b). A team leader (see Figure 1(b))
$create$s the project, then $start$s it. After that each leader $attends$ the
initial meeting and, at any time, can $discuss$ with other team members the
project. Any $submis$sion of each team need to be approved by the team leader.
The final point of each project is its $present$ation that can be attended by
all the students participating to the project. The project is evaluated based
on the presentation, which may be found unsatisfactory. In that case, the
$present$ation can be $repeat$ed. Otherwise, the project is be evaluated as
completely $fail$ed or successfully $complet$ed. A regular team member (see
Figure 1(a)) $join$s a team as first or second team member. Then, they
participate to the same project-related activities as team leaders do.

Notice these models are basic workflow nets. In Figure 1(a) and Figure 1(b)
black tokens in places represent a student’s state, whereas in Figure 1(c)
tokens account for a project’s state.

These three models show behavior of separate entities participating to the
same scenario. There are a lot of activities performed by several scenario
participants together. For example, activity $submit\ m.$ is performed in all
three workflows: a student submits the work, a team leader approves this
submission, a project changes its (progress) state. Three students (leader and
two members) always need to perform the initial meeting, whereas $discuss$ions
can be performed by two or more students.

$pl_{1}$create$p_{1}$$p_{2}$$p_{3}$$pm_{1}$join1join2$pl_{2}$$p_{4}$$p_{5}$$pm_{2}$start$pl_{3}$attend
i. m.discuss$pm_{d}$$pl_{d}$$pm_{3}$$pl_{4}$back$p_{6}$submit m.present
project$\tau$$pm_{4}$$pl_{5}$$p_{7}$completerepeatfail$pl_{6}$$pm_{5}$$p_{8}$$2$$2$$2$$2$$2$$2$$2$$2$$2$$2$

Figure 2: A Petri net model representing the university project scenario

The question is how to model the whole process with all interactions between
its participants. This can be done using the formalism of object-centric Petri
nets introduced in [4]. Figure 2 shows how student and project workflows can
be merged in the single object-centric worfklow net. To combine separate nets
we merge transitions with same labels from all workflow nets. It is important
that we use one project net, one leader net, and two member nets. This leads
to weights on some of arcs in the merged OC WF-net. Moreover, $discuss$ions
can be started and finished by an arbitrary number of students. We use special
_variable_ arcs111Upon transition firing, a variable arc transfers all the
tokens from the input place it is connected to into the output place of the
same type that is connected with another variable arc. to model this fact. Now
we have a single model which represents the whole learning process with
synchronous communications between process agents. Note that asynchronous
communications can always be modeled via synchronous mechanisms.

In this paper, we address the problem of OC WF-net soundness. It is known how
to define and to check soundness of basic WF-nets. For example, we can state
that separate participants of our learning process from Figure 1 are modeled
by sound WF models. But what can we say about soundness (correctness) of the
OC WF-net that is shown in Figure 2? And how soundness of agent models can be
related to soundness of the OC WF-net obtained by their merge?

##  3 Preliminaries

Multisets, Petri nets. Let us start with fixing some standard notions related
to _multisets_. Given a finite set $B$, a multiset $m$ over $B$ is the mapping
of the form $m:B\rightarrow\mathbb{N}$. Given an element $b\in B$,
$m(b)\in\mathbb{N}$ denotes the number of times $b$ appears in the multiset.
We write $b^{n}$ if $m(b)=n$. Given two multisets $m_{1}$ and $m_{2}$ over
$B$:
(i) $m_{1}\subseteq m_{2}$(resp., $m_{1}\subset m_{2}$) iff $m_{1}(b)\leq
m_{2}(b)$ (resp., $m_{1}(b)<m_{2}(b)$) for each $b\in B$;
(ii) $(m_{1}+m_{2})(b)=m_{1}(b)+m_{2}(b)$;
(iii) if $m_{1}\subseteq m_{2}$, $(m_{2}-m_{1})(b)=m_{2}(b)-m_{1}(b)$;
(iv) $|m|=\sum_{b\in B}m(b)$.
We use $B^{\oplus}$ to denote the set of all finite multisets over $B$.

Given two disjoint sets $P$ and $T$ of places, multiset $F:(P\times
T)\cup(T\times P)\rightarrow\mathbb{N}$ and function $\ell:T\rightarrow
A\cup\\{\tau\\}$, where $A$ is a finite set of activity labels and $\tau$ is a
special symbol denoting silent transitions, we call $N=(P,T,F,\ell,A)$ a
_labeled place/transition net_ (or a labeled P/T-net).

The notions of marking, transition enablement and firing for classical P/T
nets are defined as usual. We do not give precise definitions here, since we
will not use them explicitly in what follows.

Transition systems, bisimulation equivalence. Given a finite set of action
labels $A$ together with a special silent label $\tau$, a _(labeled)
transition system_ (LTS) is a tuple $\Gamma{}=(S,A,s_{0},\to)$, where $S$ is a
set of _states_ , $s_{0}$ is an _initial state_ and $\to\subset(S\times
A\times S)$ is a _transition relation_. In what follows, we shall write
$s\xrightarrow{a}s^{\prime}$ instead of $(s,a,s^{\prime})\in\to$.

######  Definition 1 (Strong bisimulation).

Let $\Gamma_{1}=(S_{1},A,s_{01},\to_{1})$ and
$\Gamma_{2}=(S_{2},A,s_{02},\to_{2})$ be two labeled transition systems. Then
relation $R\subseteq(S_{1}\times S_{2})$ is called a _strong bisimulation_
between $\Gamma_{1}$ and $\Gamma_{2}$ iff for every pair $(p,q)\in R$ and
$a\in A$ the following holds:

  1. (i)

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$;

  2. (ii)

if $q\xrightarrow{a}_{2}q^{\prime}$, then there exists $p^{\prime}\in S_{1}$
such that $p\xrightarrow{a}_{1}p^{\prime}$ and $(p^{\prime},q^{\prime})\in R$.

$\triangleleft$

Given $a\in A$, $p\leavevmode\hbox to20.43pt{\vbox
to8.61pt{\pgfpicture\makeatletter\hbox{\hskip 10.214pt\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}{-4.181pt}{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{$~{}a~{}$}}
}}\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{-6.61401pt}{0.0pt}\pgfsys@lineto{6.13123pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{6.13123pt}{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:

  * $\bullet$

$p\leavevmode\hbox to20.43pt{\vbox
to7.81pt{\pgfpicture\makeatletter\hbox{\hskip 10.214pt\lower-1.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}{-4.181pt}{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{$~{}a~{}$}}
}}\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@setlinewidth{0.32pt}\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{}
{}{}{} {}{}{}
\pgfsys@moveto{-1.19998pt}{1.59998pt}\pgfsys@curveto{-1.09998pt}{0.99998pt}{0.0pt}{0.09999pt}{0.29999pt}{0.0pt}\pgfsys@curveto{0.0pt}{-0.09999pt}{-1.09998pt}{-0.99998pt}{-1.19998pt}{-1.59998pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}{}{}{{}}\pgfsys@moveto{-6.61401pt}{0.0pt}\pgfsys@lineto{6.15402pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{6.15402pt}{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$;

  * $\bullet$

$p\leavevmode\hbox to19.79pt{\vbox
to6.41pt{\pgfpicture\makeatletter\hbox{\hskip 9.89398pt\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}{-3.86098pt}{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{$~{}\tau~{}$}} }}\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{-6.29399pt}{0.0pt}\pgfsys@lineto{5.834pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{5.834pt}{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}$.

######  Definition 2 (Weak bisimulation).

Let $\Gamma_{1}=(S_{1},A,s_{01},\to_{1})$ and
$\Gamma_{2}=(S_{2},A,s_{02},\to_{2})$ be two labeled transition systems. Then
relation $R\subseteq(S_{1}\times S_{2})$ is called a _weak bisimulation_
between $\Gamma_{1}$ and $\Gamma_{2}$ iff for every pair $(p,q)\in R$ and
$a\in A$ the following holds:

  1. (i)

if $p\xrightarrow{a}_{1}p^{\prime}$, then there exists $q^{\prime}\in S_{2}$
such that $q\leavevmode\hbox to20.43pt{\vbox
to6.41pt{\pgfpicture\makeatletter\hbox{\hskip 10.214pt\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}{-4.181pt}{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{$~{}a~{}$}}
}}\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{-6.61401pt}{0.0pt}\pgfsys@lineto{6.13123pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{6.13123pt}{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}q^{\prime}$ and
$(p^{\prime},q^{\prime})\in R$;

  2. (ii)

if $q\xrightarrow{a}_{2}q^{\prime}$, then there exists $p^{\prime}\in S_{1}$
such that $p\leavevmode\hbox to20.43pt{\vbox
to6.41pt{\pgfpicture\makeatletter\hbox{\hskip 10.214pt\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}{-4.181pt}{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{$~{}a~{}$}}
}}\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{-6.61401pt}{0.0pt}\pgfsys@lineto{6.13123pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{6.13123pt}{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}}_{1}p^{\prime}$ and
$(p^{\prime},q^{\prime})\in R$.

$\triangleleft$

We say that a state $p\in S_{1}$ is strongly (weakly) bisimilar to $q\in
S_{2}$, written $p\sim q$ (correspondingly, $p\approx q$), if there exists a
strong (weak) bisimulation $R$ between $\Gamma_{1}$ and $\Gamma_{2}$ such that
$(p,q)\in R$. Finally, $\Gamma_{1}$ is said to be strongly (weakly) bisimilar
to $\Gamma_{2}$ , written $\Gamma_{1}\sim\Gamma_{2}$ (correspondingly,
$\Gamma_{1}\approx\Gamma_{2}$), if $s_{01}\sim s_{02}$ ($s_{01}\approx
s_{02}$).

A _Workflow net_ is a labeled P/T net with two special places: $\mathit{in}$
and $\mathit{out}$. These places are used to mark the beginning and the ending
of the workflow process.

######  Definition 3 (Workflow net).

A labeled P/T net $N=(P,T,F,\ell,A)$ is called a _workflow net_ (_WF-net_)
iff:

  1. 1.

There is one source place $\mathit{in}\in P$ and one sink place
$\mathit{out}\in P$, s. t.
${{}^{\bullet}{\mathit{in}}}={\mathit{out}^{\bullet}}=\emptyset$.

  2. 2.

Every node from $P\cup T$ is on a path from $\mathit{in}$ to $\mathit{out}$.

  3. 3.

The initial marking in $N$ contains the only token in its source place and is
denoted by $[\mathit{in}]$.

$\triangleleft$

The marking with the only token in the sink place $\mathit{out}$ is called
_final_ and is denoted by $[\mathit{out}]$.

##  4 Object-centric Petri nets

In this section, we formally define the class of object-aware workflow Petri
nets, called _Object-Centric Petri nets (OC-nets)_. Specifically, we partially
adopt the formalism of object Petri nets presented in [4], which was
introduced as a target model for multi-perspective process mining.

OC-nets can be thought of as a rather limited version of colored Petri nets
(CPNs), where each color type contains exactly one color. Thus, the color
types coincide with the colors, tokens in the place labeled with the color
type are indistinguishable from each other, in which case we do not need
variables in arc expressions, but only the natural numbers denoting the
multiplicity of the arc, as in P/T-nets.

By analogy with [4], colors in OC-nets are called _object types_. We denote
the set of object types as $\mathbb{O}$, and reserve $\mathcal{E}$ to denote a
special “empty” type. As in [4], OC-nets also allow to use _variable arcs_ — a
special type of arcs for simultaneous transferring of a non-deterministic
amount of tokens from one place to another.

######  Definition 4 (Object-centric net).

An OC-net $ON$ is a tuple $(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$, where:

  1. 1.

$P$ and $T$ are finite sets of places and transitions, s.t. $P\cap
T=\emptyset$;

  2. 2.

$\mathtt{type}:P\rightarrow\mathbb{O}$ is a place typing function;

  3. 3.

$F:E\rightarrow\mathbb{N}\cup\\{\mu\\}$ is a multiset of flow arcs, where
$E=(P\times T)\cup(T\times P)$ and $\mu$ is used to indicate _variable_ arcs;

  4. 4.

for every $p\in P$ and $t\in T$, if $F(t,p)=\mu$, then

     * •

there is _exactly one_ $p^{\prime}\in P$ s.t. $F(p^{\prime},t)=\mu$ and
$\mathtt{type}(p)=\mathtt{type}(p^{\prime})$, and

     * •

there is no $p^{\prime\prime}\in P$ s.t.
$\mathtt{type}(p)=\mathtt{type}(p^{\prime\prime})$, $F(p^{\prime\prime},t)>0$
or $F(t,p^{\prime\prime})>0$;

  5. 5.

$A$ is a finite set of activity names, and $\ell:T\to A\cup\\{\tau\\}$ is a
function which maps transitions to activities with $\tau$ denoting a silent
(invisible) activity.

$\triangleleft$

The meaning of variable arcs in OC-nets remains in line with [4]: they are
meant to model the transfer of multiple objects from one place to another. The
condition 4 in the above definition is similar to the consistent variability
condition from [4] stipulating that for any transition $t$ and any object type
$d$ there can be no more than one pair of ingoing and outgoing for $t$
variable arcs adjacent to places of type $d$. For ease of notation, we denote
with $T_{\mu}$ the set of all transitions $t\in T$ s.t. $F(t,p)=\mu$, for some
$p\in P$.

Since the tokens residing in the same place cannot be distinguished, the OC-
net marking is defined similarly to the marking for P/T-nets. More
specifically, a _marking_ of OC-net $ON=(\mathbb{O},P,T,F,\mathtt{type})$ is a
function $\mathit{M}:P\rightarrow\mathbb{N}$. When $\mathit{M}(p)=n$ and $n>0$
for some $p\in P$, we say that there are $n$ objects of type
$\mathtt{type}(p)$ in state $M$. We write $\langle ON,\mathit{M}\rangle$ to
denote OC-net $ON$ marked with $\mathit{M}$ and use symbol $\mathit{M}_{0}$ to
define the initial marking of the net. For ease of notation, we also denote
with $[p_{1}^{i_{1}},\ldots,\mathrm{p}_{n}^{i_{n}}]$ a concrete multiset
representing a marking in which each place $p_{k}$ contains $i_{k}$ tokens.
Finally, with $\mathbb{M}^{P}$ we denote the countably infinite set of all
possible markings defined on top of $P$.

Let us now specify the net dynamics. As customary, given $x\in P\cup T$, we
use ${{}^{\bullet}{x}}:=\\{x\mid F(\\_,x)>0\text{ or }F(\\_,x)=\mu\\}$ to
denote the _preset_ of $x$ and ${x^{\bullet}}:=\\{x\mid F(x,\\_)>0\text{ or
}F(x,\\_)=\mu\\}$ to denote the _postset_ of $x$.

Since a transition can have multiple incoming and outgoing variable arcs of
different types, we would like to be able to explicitly identify how many
tokens from each place adjacent to the variable arc are transferred by the
transition firing. To this end, we introduce a function
$\alpha:\mathbb{O}\to\mathbb{N}$ specifying the transition’s _transfer mode_.
Note that by Definition 4, a transition $t$ in an OC-net cannot have two
transitions $p_{1},p_{2}\in{{}^{\bullet}{t}}$ s.t.
$F(p_{1},t)=F(p_{2},t)=\mu$. Thus, $\alpha$ does not create ambiguities by
relating to object types only.

We then say that transition $t$ is _enabled_ in marking $M$ with transfer mode
$\alpha$, written $\mathit{M}[t,\alpha\rangle$, iff, for every
$p\in{{}^{\bullet}{t}}$, the following conditions hold:

  1. (i)

$F(p,t)\leq\mathit{M}(p)$, if $F(p,t)\in\mathbb{N}$, and

  2. (ii)

$\mathit{M}(p)\geq\alpha(\mathtt{type}(p))$, if $F(p,t)=\mu$.

When $t$ is enabled in marking $M$ with transfer mode $\alpha$, it may _fire_
, yielding new marking $\mathit{M}^{\prime}$ that is defined for every $p\in
P$ as follows:

$\mathit{M}^{\prime}(p)=\begin{cases}\mathit{M}(p)-\alpha(\mathtt{type}(p)),&\text{if
\,}F(p,t)=\mu\\\ \mathit{M}(p)+\alpha(\mathtt{type}(p)),&\text{if
\,}F(t,p)=\mu\\\ \mathit{M}(p)-F(p,t)+F(t,p),&\text{otherwise}\end{cases}$

We denote this as $\mathit{M}[t,\alpha\rangle\mathit{M}^{\prime}$ and assume
that the definition is inductively extended to sequences
$\sigma\in(T\times\mathbb{O}\to\mathbb{N})^{*}$ of transition firings. We say
that $\mathit{M}^{\prime}$ is _reachable_ from $\mathit{M}$ if there exists
$\sigma\in(T\times\mathbb{O}\to\mathbb{N})^{*}$, s.t.
$\mathit{M}[\sigma\rangle\mathit{M}^{\prime}$. For an OC-net $ON$, we write
$\mathcal{R}(ON,\mathit{M}_{0})$ to denote the set of all markings reachable
from its initial marking $\mathit{M}_{0}$.

The execution semantics of an OC-net can be captured with a possibly infinite-
state LTS that accounts for all possible executions starting from OC-net’s
initial marking. Formally, an OC-net
$ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$ with initial marking $M_{0}$
_induces_ a labeled transition system $\Gamma_{ON}=(S,A,s_{0},\to)$, where:

  * •

$S=\mathcal{R}(ON,\mathit{M}_{0})$ and $s_{0}=M_{0}$,

  * •

for $M,M^{\prime}\in S$ it holds that: $M\xrightarrow{a}M^{\prime}$ iff
$\mathit{M}[t,\alpha\rangle\mathit{M}^{\prime}$, for some $t\in T$ s.t.
$\ell(t)=a$ and some transfer mode $\alpha$.

Algorithm 1 Variable arc elimination

0: $\langle ON,M_{0}\rangle$, where
$ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$, s.t. for some $t\in T$ and $p\in
P$ it holds that $F(t,p)=\mu$

0: $\langle ON^{\prime},M_{0}^{\prime}\rangle$, where
$ON^{\prime}=(\mathbb{O}^{\prime},P^{\prime},T^{\prime},F^{\prime},\mathtt{type}^{\prime},\ell^{\prime},A)$,
s.t. for all $t\in T^{\prime}$ and $p\in P^{\prime}$ it holds that
$F^{\prime}(t,p)\neq\mu$

$\mathbb{O}^{\prime}=\mathbb{O}\cup\\{\mathcal{E}\\}$

$P^{\prime}=P\cup\\{lock\\}$

$T^{\prime}=T$

for all $t\in T_{\mu}$ do

$P^{\prime}=P^{\prime}\cup\\{lock_{t}\\}$

$T^{\prime}=T^{\prime}\cup\\{start_{t},add_{t}\\}$

end for

for all $p,p^{\prime}\in P^{\prime},t\in T^{\prime}$ do

$F^{\prime}(p,t)=\begin{cases}k,&\text{if \,}F(p,t)=k\\\ 1,&\text{if
\,}(p,t)=(lock,t)\\\ 1,&\text{if
\,}F(p,t)=F(t,p^{\prime})=\mu\,\and\,(p,t)\in\\{(p,start_{t}),(lock,start_{t}),\\\
&\phantom{xxxxxxxxxxxxxxxxxxxxxxxxxx}\,(lock_{t},add_{t}),(p,add_{t}),\\\
&\phantom{xxxxxxxxxxxxxxxxxxxxxxxxxx}\,(lock_{t},t),(p^{\prime},t)\\}\end{cases}$

$F^{\prime}(t,p^{\prime})=\begin{cases}k,&\text{if \,}F(t,p^{\prime})=k\\\
1,&\text{if \,}(p,t)=(t,lock)\\\ 1,&\text{if
\,}F(p,t)=F(t,p^{\prime})=\mu\,\and\,(p,t)\in\\{(start_{t},p),(start_{t},lock_{t}),\\\
&\phantom{xxxxxxxxxxxxxxxxxxxxxxxxxx}\,(add_{t},lock_{t}),(add_{t},p^{\prime}),(t,p^{\prime})\\}\end{cases}$

$\mathtt{type}^{\prime}(p)=\begin{cases}\mathtt{type}(p),&\text{if \,}p\in
P\\\ \mathcal{E},&\text{otherwise}\end{cases}$
$\ell^{\prime}=\begin{cases}\ell(t),&\text{if \,}t\in T\\\
\tau,&\text{otherwise}\end{cases}$

$M_{0}^{\prime}=\begin{cases}M_{0}(p),&\text{if \,}p\in P\\\ 1,&\text{if
\,}p=lock\\\ 0,&\text{otherwise}\end{cases}$

end for

Now, after we have defined the syntax and semantics of OC-nets, we would like
to observe that every OC-net $ON$ can be represented with OC-net $ON^{\prime}$
that does not contain variable arcs. To this end, we provide a variable arc
elimination algorithm and show that its output is always weakly bisimilar to
its input. The weak bisimilarity is conditioned by the fact that in order to
correctly represent the behavior of $ON$, $ON^{\prime}$ must include
additional intermediate steps that are, however, invisible and therefore not
relevant to the comparison of net behavior. That is why we need to use a form
of bisimulation allowing to “skip” transitions irrelevant for the behavioral
comparison [Milner89]. Finally, we say that two marked OC-nets $\langle
ON,M_{0}\rangle$ and $\langle ON^{\prime},M^{\prime}_{0}\rangle$ are _weakly
bisimilar_ (and denote it as $\langle ON,M_{0}\rangle\approx\langle
ON^{\prime},M^{\prime}_{0}\rangle$) if for transition systems $\Gamma_{ON}$
and $\Gamma_{ON^{\prime}}$ they respectively induce it holds that
$\Gamma_{ON}\approx\Gamma_{ON^{\prime}}$.

Given a generic OC-net, Algorithm 1 allows to construct from it a behaviorally
equivalent OC-net that has no variable arcs. For example, consider a simple
net in Figure 3(a). By applying the above algorithm to it, we obtain a new OC-
net (see Figure 3(b)) that has no variable arcs. As it has been mentioned
before, the algorithm produces a net that behaves exactly like the input one.
Indeed, the net in Figure 3(b) models removed variable arcs with a sub-net
representing a “lossy” transfer, working under the assumption that at least
one token gets transferred from $\mathit{in}$ to $\mathit{out}$ (this
assumption is in line with Definition 4). First, using $start_{t}$, the net
enters into a critical section that is guarded by the special lock place
$lock$. Notice that this lock is global to the whole net and is used to guard
firing of every transition from the original net. When the net acquires the
lock, it can “transfer” tokens from $p_{1}$ to $p_{2}$ using transition
$add_{t_{1}}$. As soon as at least one token has been generated in $p_{2}$,
the transfer can be finalized by firing $t_{1}$ that releases the global lock.
This example leads us to the following statement.

a$t_{1}$$p_{1}$$p_{2}$$p_{3}$$p_{4}$b$t_{2}$

(a) A simple OC-net

$p_{1}$$\tau$$start_{t_{1}}$$lock_{t_{1}}$$\tau$$add_{t_{1}}$$p_{2}$a$t_{1}$$p_{3}$$p_{4}$$\Large\bullet$$lock$b$t_{2}$

(b) The same net but without variable arcs

Figure 3: Demonstration of Algorithm 1 applied to OC-net 3(a) with OC-net 3(b)
as output

######  Proposition 1.

Let $\langle ON,M_{0}\rangle$ be a marked OC-net, where
$ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$. Then we can effectively
construct a marked OC-net $\langle ON^{\prime},M_{0}^{\prime}\rangle$, such
that $ON^{\prime}$ has no variable arcs and $\langle
ON,M_{0}\rangle\approx\langle ON^{\prime},M^{\prime}_{0}\rangle$.
$\triangleleft$

Recall that OC-nets specify a class of nets that can be used to model the
behavior of multiple, possibly interacting, objects of different types within
one system. Notice that the formalism of OC-nets does not allow you to
distinguish between objects of the same type. However, at the same time, one
can focus on the lifecycle represented by one type of objects. Unlike the
life-cycle of a single object, the lifecycle of an object type can encompass
various possible behaviours for objects of that type. Next, we introduce a
definition of a _projection_ that supports retrieving a subnet based on a
given object type.

Let $ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$ be an OC-net, $M$ be a
marking in $ON$, $d\in\mathbb{O}$. In what follows, we will make use of the
following notations for _$\mathtt{d}$ -based restrictions_ of OC-net
components: $\left.P\right|_{\mathtt{d}}=\\{p\mid p\in
P,\,\mathtt{type}(p)=\mathtt{d}\\}$, $\left.T\right|_{\mathtt{d}}=\\{t\mid
t\in T,\,\text{ there is }p\in{{}^{\bullet}{t}}\cup{t^{\bullet}}\text{ s.t.
}\mathtt{type}(p)=\mathtt{d}\\}$,
$\left.F\right|_{\mathtt{d}}=F\cap((\left.P\right|_{\mathtt{d}}\times\left.T\right|_{\mathtt{d}})\cup(\left.T\right|_{\mathtt{d}}\times\left.P\right|_{\mathtt{d}}))$
$\left.\mathtt{type}\right|_{\mathtt{d}}=\left.\mathtt{type}\right|_{{\left.P\right|_{\mathtt{d}}}}$,
$\left.\ell\right|_{\mathtt{d}}=\left.\ell\right|_{{\left.T\right|_{\mathtt{d}}}}$,
and
$\left.M\right|_{\mathtt{d}}=\left.M\right|_{{\left.P\right|_{\mathtt{d}}}}$.

######  Definition 5 (Object type projection).

A _$\mathtt{d}$ -typed projection_ of an OC-net
$ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$ is the OC-net
$(\\{\mathtt{d}\\},\left.P\right|_{\mathtt{d}},\left.T\right|_{\mathtt{d}},\left.F\right|_{\mathtt{d}},\left.\mathtt{type}\right|_{\mathtt{d}},\left.\ell\right|_{\mathtt{d}},A)$.
We denote the projection as $\left.ON\right|_{\mathtt{d}}$. $\triangleleft$

Since all places in an object-type projection of an OC-net are labeled with
the same and only type, this labeling can be omitted, and the object
projection can be considered as a P/T-net. Then, abusing the notation, we
denote both the $\mathtt{d}$-typed projection of OC-net $ON$ and the
corresponding P/T-net by $\left.ON\right|_{\mathtt{d}}$.

Finally, let $d^{\prime}\not\in\mathbb{O}$ be a ’fresh’ name for a data type.
By $ON_{[\mathtt{d}/\mathtt{d}^{\prime}]}$ we denote the OC-net
$ON^{\prime}=(\mathbb{O}^{\prime},P^{\prime},T^{\prime},F^{\prime},\mathtt{type}^{\prime},\ell^{\prime},A)$
such that:

  * •

graphs $(P,T,F)$ and $(P^{\prime},T^{\prime},F^{\prime})$ are isomorphic via
some isomorphism function $\iota$,

  * •

$\mathbb{O}^{\prime}=(\mathbb{O}\setminus\\{\mathtt{d}\\})\cup\\{\mathtt{d}^{\prime}\\}$,

  * •

for $p\in P$, $\mathtt{type}^{\prime}(\iota(p))=\mathtt{d}^{\prime}$ if
$\mathtt{type}(p)=\mathtt{d}$, otherwise
$\mathtt{type}^{\prime}(\iota(p))=\mathtt{type}(p)$,

  * •

for $t\in T$, $\ell^{\prime}(\iota(t))=\ell(t)$.

In other words, $ON_{[\mathtt{d}/\mathtt{d}^{\prime}]}$ is a copy of $ON$ in
which $\mathtt{d}$ is replaced with $\mathtt{d}^{\prime}$.

##  5 Object-centric Workflows

In this section, we show how object-centric nets can be used to represent
workflows of multiple, possibly interacting, artifacts of different types.

A classical, untyped, workflow net is used to represent workflows or
lifecycles of one single object (or case) in isolation. There are also
generalized workflow nets [16], where the initial state contains several
indistinguishable objects (black dots) in the source place, and the final
state contains all these objects in the sink place, so that a workflow run
terminates when all items initially residing in the source place are processed
and located in the sink place.

Next, we will show how to extend the concept of a workflow net to cover
multiple objects of different types. For this we use OC-nets, in which a typed
place is a location for tokens of one type. In OC workflow nets, tokens of a
specific type will be processed according to a specific workflow, but can
interact with each other and with tokens of other types. Another important
feature is that new objects can appear in source places at any moment. Thus,
while it is assumed that the proper behavior of each object terminates, the
system represented by the OC workflow net can run infinitely long.

######  Definition 6.

An OC-net $ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$ is called an _object-
centric worfklow net_ (or OC WF-net for short), iff:

  1. 1.

for every $\mathtt{d}\in\mathbb{O}$, $\left.ON\right|_{\mathtt{d}}$ is a WF-
net;

  2. 2.

for every transition $t\in T$,
${{}^{\bullet}{t}}\cup{t^{\bullet}}\not=\emptyset$, i.e. there are no isolated
transitions in $ON$.

$\triangleleft$

Thus, a classical WF-net is the OC WF-net with exactly one object type, and OC
WF-nets form true extension of WF-nets.

For OC WF-net $ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$, we use the
notation $\mathit{in}_{\mathtt{d}}\in P$ and $\mathit{out}_{\mathtt{d}}\in P$
for its (only) _source_ and _sink_ places of type $d$, i.e.
$\mathtt{type}(\mathit{in}_{\mathtt{d}})=\mathtt{type}(\mathit{out}_{\mathtt{d}})=\mathtt{d}$
and
${{}^{\bullet}{\mathit{in}_{\mathtt{d}}}}={\mathit{out}_{\mathtt{d}}^{\bullet}}=\emptyset$.
By $P_{\mathit{in}}$ and $P_{\mathit{out}}$, we denote the sets of all source
and sink places, respectively.

For OC WF-nets, we allow several tokens in each of its source places for an
initial marking, not restricting the consideration to a workflow for just one
case and just one initial marking. We also do not suppose that there are some
fixed final markings for OC WF-nets and that reaching a final marking means
termination of the system.

The _synchronous composition_ of two nets $N_{1}$ and $N_{2}$ is a net
obtained by pairwise merging of transitions in $N_{1}$ with transitions with
the same labels in $N_{2}$. Fig. 4 gives an example of a synchronous
composition of two nets. Note that though both components in Fig. 4(a) are
simple and sound WF-nets, their synchronous composition is dead in its initial
marking, provided the initial marking is the “canonical” one (that is, only
input places have tokens assigned to them).

$\mathit{in}_{1}$$a$$p_{1}$$b$$\mathit{out}_{1}$$\mathit{in}_{2}$$b$$p_{2}$$a$$\mathit{out}_{2}$

(a)

$\mathit{in}_{1}$$a$$p_{1}$$b$$\mathit{out}_{1}$$\mathit{out}_{2}$$\mathit{in}_{2}$$p_{2}$

(b)

Figure 4: Two simple WF-nets (Figure 4(a)) and their synchronous composition
(Figure 4(b))

It is easy to note that every OC WF-net
$ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$ is a synchronous composition of
all its $\mathtt{d}$-projections $\left.N\right|_{\mathtt{d}}$, where
$\mathtt{d}\in\mathbb{O}$, and $\mathtt{d}$-projection
$\left.N\right|_{\mathtt{d}}$ represents the lifecycle for objects of type
$\mathbb{O}$.

So far, we have been considering nets allowing to model co-evolution of
multiple objects of various object types. The main limitation of the OC-net
formalism is that the identity of such objects is always hidden: one can only
see how many anonymous objects of the same type are stored in a place. Yet, in
certain scenarios it might be still useful to _track_ a single object. This
tracking can be achieved by, first, isolating the behavior of the object and
then carefully merging the extracted subnet with the original net. To this
end, we first define a new, more restrictive type of projection that, instead
of focusing on all possible behaviors of a single object type, captures
behavior of one object.

######  Definition 7 (1-safe projection).

Let $ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$ be an OC-net,
$\mathtt{d}\in\mathbb{O}$. OC-net $ON^{\prime}$ is called _1-safe
$\mathtt{d}$-typed projection_ of OC-net $ON$ (denoted
$\left.ON\right|_{\mathtt{d}}^{1}$) iff $ON^{\prime}$ coincides with
$\left.ON\right|_{\mathtt{d}}$ except the arc multiplicity function, which
takes the value 1 throughout its domain. Namely,
$\left.ON\right|_{\mathtt{d}}^{1}=(\\{\mathtt{d}\\},\left.P\right|_{\mathtt{d}},\left.T\right|_{\mathtt{d}},\left.F\right|_{\mathtt{d}}^{1},\left.\mathtt{type}\right|_{\mathtt{d}},\left.\ell\right|_{\mathtt{d}},A)$,
where $\left.F\right|_{\mathtt{d}}^{1}(x,y)=1$, if
$\left.F\right|_{\mathtt{d}}(x,y)\not=0$, and
$\left.F\right|_{\mathtt{d}}^{1}(x,y)=0$, otherwise. $\triangleleft$

Now, using 1-safe projection, we can construct a net that can track a single
object evolution as well as its potential interactions with other objects of
the same or any other type in the net.

######  Definition 8 (Tracking OC WF-net).

Let $ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$ be a OC WF-net and
$ON^{\prime}=(\\{\mathtt{d}^{\prime}\\},P^{\prime},T^{\prime},F^{\prime},\mathtt{type}^{\prime},\ell^{\prime},A)$,
such that
$ON^{\prime}=(\left.ON\right|_{\mathtt{d}}^{1})_{[\mathtt{d}/\mathtt{d}^{\prime}]}$.
Then its _$(\mathtt{d},\mathtt{d}^{\prime})$ -typed tracking extension_,
denoted as $ON_{\mathtt{d}+\mathtt{d}^{\prime}}$, is the OC WF-net
$(\mathbb{O}\cup\\{\mathtt{d}^{\prime}\\},P\cup P^{\prime},T\cup
T^{\prime}\cup
T^{\prime\prime},F^{\prime\prime},\mathtt{type}\cup\mathtt{type}^{\prime},\ell^{\prime\prime},A)$222Here,
given two functions $f:X\to A$ and $g:Y\to B$, we write $f\cup g:X\cup Y\to
A\cup B$ iff $\left.f\right|_{X\cap Y}=\left.g\right|_{X\cap Y}$., where:

  * •

$T^{\prime\prime}=\\{t^{\prime\prime}\mid t\in T_{1}\cup T_{2}\\}$, where
$T_{1}=(\bigcup_{p\in P^{\prime}\cap P}{{}^{\bullet}{p}})\setminus T^{\prime}$
and $T_{2}=T^{\prime}\cap T_{\mu}$;

  * •

$F^{\prime\prime}(x,y)=\begin{cases}F(x,y),&\text{if \,}(x,y)\in(P\times
T)\cup(T\times P)\\\ F^{\prime}(x,y),&\text{if \,}(x,y)\in(P^{\prime}\times
T^{\prime})\cup(T^{\prime}\times P^{\prime})\\\ F(x,t)-1,&\text{if
\,}(x,y)\in(P\times T^{\prime})\text{, }t\in T\\\ F(t,x)-1,&\text{if
\,}(x,y)\in(T^{\prime}\times P)\text{, }t\in T\\\ F(x,t),&\text{if
\,}(x,y)\in(P\times(T_{1}\cup T_{2}))\text{, }t\in T\\\ F(t,x),&\text{if
\,}(x,y)\in((T_{1}\cup T_{2})\times P)\text{, }t\in T\\\ \end{cases}$

$\triangleleft$

For $(\mathtt{d},\mathtt{d}^{\prime})$-typed tracking extension of OC WF-net
$ON$, we call $ON$ the _ground component_ , and
$ON^{\prime}=(\left.ON\right|_{\mathtt{d}}^{1})_{[\mathtt{d}/\mathtt{d}^{\prime}]}$
– the _tracking component_.

######  Proposition 2.

Let $ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$ be a OC WF-net,
$M_{\mathit{in}}$ – its initial marking. Let also $\mathtt{d}\in\mathbb{O}$
and $\mathtt{d}^{\prime}\not\in\mathbb{O}$.

Then $ON$ with the initial marking $M_{\mathit{in}}$ is weakly bisimilar to
its $(\mathtt{d},\mathtt{d}^{\prime})$-typed tracking extension
$ON_{\mathtt{d}+\mathtt{d}^{\prime}}$ with the initial marking
$M_{\mathit{in}^{\prime}}$, s.t.

$M_{\mathit{in}^{\prime}}(\mathit{in}_{\mathtt{d}^{\prime}})=1$, if
$M_{\mathit{in}}(\mathit{in}_{\mathtt{d}})\geq 1$,
$M_{\mathit{in}^{\prime}}(\mathit{in}_{\mathtt{d}^{\prime}})=0$, if
$M_{\mathit{in}}(\mathit{in}_{\mathtt{d}})=0$,

$M_{\mathit{in}^{\prime}}(\mathit{in}_{\mathtt{d}})=M_{\mathit{in}^{\prime}}(\mathit{in}_{\mathtt{d}})-1$,
if $M_{\mathit{in}}(\mathit{in}_{\mathtt{d}})\geq 1$,
$M_{\mathit{in}^{\prime}}(\mathit{in}_{\mathtt{d}})=0$, if
$M_{\mathit{in}}(\mathit{in}_{\mathtt{d}})=0$,

for every $p\in P\setminus\\{\mathit{in}_{\mathtt{d}}\\}$,
$M_{\mathit{in}^{\prime}}(p)=M_{\mathit{in}}(p)$. $\triangleleft$

Notice that the tracking extension itself can be used for monitoring concrete
objects. The property below demonstrates that one can essentially monitor a
finite number of objects at once.

######  Proposition 3.

Let $ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$ be a OC WF-net. Let also
$d_{1},d_{2}\in\mathbb{O}$, $d_{1}^{\prime},d_{2}^{\prime}\not\in\mathbb{O}$,
and $d_{1}\not=d_{2}$, $d_{1}^{\prime}\not=d_{2}^{\prime}$.

Then nets
$(ON_{\mathtt{d}_{1}+\mathtt{d}_{1}^{\prime}})_{\mathtt{d}_{2}+\mathtt{d}_{2}^{\prime}}$
and
$(ON_{\mathtt{d}_{2}+\mathtt{d}_{2}^{\prime}})_{\mathtt{d}_{1}+\mathtt{d}_{1}^{\prime}}$
are identical, i.e. the result of the successive application of multiple
tracking extensions does not depend of their order. $\triangleleft$

######  Example 1.

Let us consider an example of _tracking extension_. Figure 5 shows a OC WF-net
$N$ consisting of two nets related to two object types $\mathtt{d}_{1}$ and
$\mathtt{d}_{2}$ that, for simplicity, are respectively depicted with green
and yellow colors.

$in_{1}$$i_{1}$$p_{1}$$t_{1}$$p_{3}$$i_{2}$$in_{2}$$p_{2}$$o_{1}$$out_{1}$$p_{4}$$o_{2}$$out_{2}$

Figure 5: An OC WF-net with two object types $\mathtt{d}_{1}$ (in yellow) and
$\mathtt{d}_{2}$ (in green)

Let us consider tracking extensions for both object types of $N$. By properly
identifying the tracking component for $\mathtt{d}_{1}$, we demonstrate $N$’s
$(\mathtt{d}_{1},\mathtt{d}_{1}^{\prime})$-tracking extension in Figure 6
(here, $\mathtt{d}_{1}^{\prime}$ is represented with indigo color). Similarly
to $\mathtt{d}_{1}$, we present $N$’s
$(\mathtt{d}_{2},\mathtt{d}_{2}^{\prime})$-tracking extension in Figure 7
($\mathtt{d}_{2}^{\prime}$ is in red).

$in_{1}$$i_{1}$$p_{1}$$t_{1}$$p_{3}$$i_{2}$$in_{2}$$p_{2}$$o_{1}$$out_{1}$$p_{4}$$o_{2}$$out_{2}$$t_{1}^{\prime}$$p_{1}^{\prime}$$i_{1}^{\prime}$$in_{1}^{\prime}$$p_{2}^{\prime}$$o_{1}^{\prime}$$out_{1}^{\prime}$$o_{2}^{\prime}$

Figure 6: Tracking OC WF-net for an object of type $\mathtt{d}_{1}$

$in_{1}$$i_{1}$$p_{1}$$t_{1}$$p_{3}$$i_{2}$$in_{2}$$p_{2}$$o_{1}$$out_{1}$$p_{4}$$o_{2}$$out_{2}$$t_{1}^{\prime\prime}$$p_{3}^{\prime}$$i_{2}^{\prime}$$in_{2}^{\prime}$$p_{4}^{\prime}$$o_{2}^{\prime}$$out_{2}^{\prime}$$t_{1}^{\prime}$

Figure 7: Tracking OC WF-net for an object of type $\mathtt{d}_{2}$

$\triangleleft$

##  6 Object-centric Soundness

The most crucial correctness criterion for workflow nets is soundness [5]. For
classical WF-nets, a workflow case execution terminates properly, iff starting
at the initial marking with a single token in its source place it terminates
with a single token in its sink place, i.e. there are no “garbage” tokens
after termination. A WF-net is called sound iff its execution can terminate
properly, starting at any reachable marking.

The soundness definition from above always considers one object (or, more
traditionally, one case) in isolation, or several objects of the same type
executing a common task, so that they start and finish together (generalized
soundness). At the same time, as Definition 6 suggests, OC WF-nets need to
account for multiple objects of different types, when objects of the same type
follow similar tasks, defined by a common for them workflow, and each object
needs to terminate properly. The motivating example in Section 2 illustrates
such a system. To this end, we extend the classical notion of soundness with
object types as well as multiple typed source and sink places.

We start by recalling the classical notion of soundness used for WF-nets and
then show how it can be extended to the object-centric case.

######  Definition 9 (WF-net soundness).

Let $N=(P,T,F)$ be a WF-net, and let $\mathit{in},\mathit{out}\in P$ be its
source and sink places, respectively. The net is called _sound_ iff

  1. 1.

for every $\mathit{M}\in\mathcal{R}(N,[\mathit{in}])$, it holds that
$[\mathit{out}]\in\mathcal{R}(N,\mathit{M})$ (_option to complete_);

  2. 2.

for every $\mathit{M}\in\mathcal{R}(N,[\mathit{in}])$, if
$[\mathit{out}]\subseteq\mathit{M}$, then $\mathit{M}=[\mathit{out}]$ (_proper
completion_);

  3. 3.

for every $t\in T$, there exists $\mathit{M}\in\mathcal{R}(N,[\mathit{in}])$,
s.t. $\mathit{M}[t\rangle$ (_no dead transitions_).

$\triangleleft$

Now we come to defining object-oriented soundness for OC WF-nets.

######  Definition 10 (Object soundness, system soundness).

Let $ON$ be a $\mathbb{O}$-typed OC WF-net, $\mathtt{d}\in\mathbb{O}$ be one
of its types, $\mathtt{d}^{\prime}\not\in\mathbb{O}$, and
$ON_{\mathtt{d}+\mathtt{d}^{\prime}}=(\mathbb{O}^{\prime},P^{\prime},T^{\prime},F^{\prime},\mathtt{type}^{\prime},\ell^{\prime},A)$
be the $(\mathtt{d},\mathtt{d}^{\prime})$-typed tracking extension of $ON$.

$ON$ is called _object-sound for type $\mathtt{d}$_ (_$\mathtt{d}$ -sound_ for
short) iff for every input marking
$\mathit{M}_{\mathit{in}}\in{P^{\prime}}_{\mathit{in}}^{\oplus}$ in
$ON_{\mathtt{d}+\mathtt{d}^{\prime}}$ s.t.
$\mathit{M}_{\mathit{in}}(\mathit{in}_{\mathtt{d}})=1$, it holds that for any
marking $M\in\mathcal{R}(ON,\mathit{M}_{\mathit{in}})$, there exist initial
marking
$\mathit{M}_{\mathit{in}}^{\prime}\in(P^{\prime}_{\mathit{in}})^{\oplus}$ and
target marking $\mathit{M}^{\prime}\in(P^{\prime})^{\oplus}$ s.t. :

  * •

$\mathit{M}^{\prime}\in\mathcal{R}(ON^{\prime},\mathit{M}+\mathit{M}_{\mathit{in}}^{\prime})$,
i.e., target marking $M^{\prime}$ can be reached from $M$, possibly by adding
more tokens to source places;

  * •

$\mathit{M}^{\prime}(\mathit{out}_{\mathtt{d}})=1$, i.e., the (tracked) object
of type $\mathtt{d}$ has reached its final state in target marking
$\mathit{M}^{\prime}$;

  * •

for all $p\in P^{\prime}$ s.t. $\mathtt{type}(p)=\mathtt{d}$ and
$p\not=\mathit{in}_{\mathtt{d}}$, we have $\mathit{M}^{\prime}(p)=0$, i.e.,
the (tracked) object of type $\mathtt{d}$ terminates properly (without leaving
“garbage” behind, i.e. in the tracking component),

  * •

there are no dead transitions in 1-safe $\mathtt{d}$-typed projection
$\left.ON\right|_{\mathtt{d}}^{1}$ of OC-net $ON$ with the initial marking
that contains the only token in source place $\mathit{in}_{\mathtt{d}}$.

The same $ON$ is called _object-centric sound_ (_OC-sound_ , for short) iff it
is $\mathtt{d}$-sound for every $\mathtt{d}\in\mathbb{O}$. $\triangleleft$

As in classical WF-nets, this definition focuses on a “concrete” object and
traces its lifecycle until the end. This is possible due to the relaxed
treatment of object identifiers: the OC WF-net cannot inspect the content of
its tokens, but can always check types of places that carry the tokens. Thus,
it suffices to look into quantities of objects available in a net marking.

However, unlike in classical WF-nets, this single object is not considered in
isolation. Our notion of OC-soundness allows to account for potentially
multiple objects in the source places, but cares only for one single object
when it comes to checking whether the process has been completed or not (that
is, we want to check only whether the “object of interest” has reached the
source place). At the same time, we take no notice of other objects that were
potentially “helping” that very selected object to complete the process. This
means that the net may still contain tokens corresponding to other objects in
some intermediate places.

######  Example 2.

Consider the scenario discussed in Section 2. There, a project can always be
completed regardless “concrete” team members and leaders that are currently
present in the net (i.e., we can always introduce into the net marking
additional students to complete “the selected” project). Likewise, each team
member has an opportunity to complete their task. $\triangleleft$

The following statements follow directly from the definition of OC-soundness.

######  Proposition 4.

Let $N=(P,T,F)$ be a WF-net. If $N$ is sound, then it is also OC-sound as OC
WF-net $ON=(\\{\mathtt{d}\\},P,T,F,\mathtt{type})$, where for all $p\in P$,
$\mathtt{type}(p)=\mathtt{d}$. $\triangleleft$

Let us now come back to the projections. We now show how OC WF-nets and their
1-safe projections can be related.

######  Proposition 5.

Let $ON=(\mathbb{O},P,T,F,\mathtt{type},\ell,A)$ be an OC WF-net. If $ON$ is
OC-sound, then for any $\mathtt{d}\in\mathbb{O}$, its 1-safe
$\mathtt{d}$-typed projection $\left.ON\right|_{\mathtt{d}}^{1}$ is sound as a
WF-net. $\triangleleft$

From this proposition it follows that the reachability set (set of all
reachable markings) of a 1-safe projection $\left.ON\right|_{\mathtt{d}}^{1}$
of sound OC WF-net $ON$ is finite, since the reachability set of sound
(classical) WF-net is always finite.

######  Proposition 6.

Each 1-safe projections of an OC-sound OC WF-net has finitely many reachable
markings. $\triangleleft$

For OC WF-nets we do not fix either input, or output markings. Sound OC WF-
nets have, generally speaking, an infinite number of reachable markings. When
defining OC-soundness, we take care of the possibility to terminate properly
for one selected object. For this object, all other objects play the role of
resources required to complete its task. Unlike to workflow nets with
resources, in OC WF-nets, these resources are dynamic and can be added as
needed. A well-designed system should guarantee “equal rights” to all
participants, i.e. each object has an ability to terminate properly from any
reachable marking. OC-soundness defines this formally. The good news is that
this crucial property is decidable.

######  Theorem 1.

The problem of checking OC-soundness for an OC WF-net is decidable.
$\triangleleft$

##  7 Related Work

###  7.1 Modeling Object-centric and Data-aware Processes using Petri nets

There are multiple Petri net-based approaches used for modeling data- and
object-aware processes. Here we briefly cover only the most recent ones.

The formalism of Petri nets with identifiers (PNIDs) was studied in [17]. In
such nets, tokens carry tuples of object identifiers (or references).
Moreover, transitions can produce globally new data values that are different
from those in a current marking. PNIDs have been also used as the process
modeling language in the Information Systems Modeling Language (ISML)
presented in [22]. In ISML, PNIDs are paired with special CRUD operations
defining operations over relevant data. Such data are structured according to
an ORM model.

A viewpoint on multi-case and data-aware process models is covered by works on
so-called _Proclets_. This concept was first proposed in [2]. Proclets are
essentially quasi-workflows representing lifecycles of particular objects and
allowing for different types of communication between such lifecycles via
dedicated channels. The Proclet notation was applied to model processes with
complex interactions between process objects [10] as well as artifact-centric
processes [9]. Process artifacts here are documents, orders, deliveries, and
other types of data objects which are manipulated within the process.
Artifact-centric process models consider these objects as first-class
citizens. Note that in such models process cases are often related to object
types that leads to inter-case dependencies when more complicated
communication patterns are involved.

In [12] the authors introduced catalog-nets (CLog-nets). Conceptually, the
formalism marries read-only relational databases with a variant of colored
Petri nets [18] which allows for generation of globally fresh data values upon
transition firing. In CLog-nets, transitions are equipped with guards that
simultaneously inspect the content of tokens and query facts stored in the
database.

###  7.2 Soundness for Workflow Nets and their Extensions

The notion of soundness for classical WF-nets was initially discussed in
[1].333This notion coincides with the one presented in the beginning of
Section 6. Since then, many different variants of soundness have been proposed
for WF-nets and their non-high-level extensions. An extensive study on such
variants as well as related decidability results can be found in [5]. In the
following, we briefly touch upon some of the soundness notions. Perhaps one of
the most important generalizations of classical soundness are $k$-soundness
and generalized soundness [16]. A WF-net is $k$\- sound if, starting with $k$
tokens in its source place, it always properly terminates with $k$ tokens in
its sink place. Hence this notion allows handling multiple individual
processes (cases) in a WF-net. The classical soundness then coincides with
1-soundness. Generalized soundness is $k$-soundness for all $k$. It was proved
in [16] that both $k$-soundness and generalized soundness are decidable.

One of the important aspects of workflow development concerns resource
management. In classical Petri nets, one can distinguish places, corresponding
to control flow states, and places, representing different kinds of resources.
There are various works that study different resource-aware extensions of WF-
nets together with related notions of soundness. In [7] the authors studied a
specific class of WFR-nets for which soundness was shown to be decidable. In
[15, 23] a more general class of Resource-Constrained Workflow Nets (RCWF-
nets) was defined. The constraints are imposed on resources and require that
all resources that are initially available are present again after all cases
terminate, and that for any reachable marking, the number of available
resources does not override the number of initially available resources. In
[15] it was proven that for RCWF-nets with a single resource type generalized
soundness can be effectively checked in polynomial time. Decidability of
generalized soundness for RCWF-nets with an arbitrary number of resource
places was shown in [23].

All the above mentioned works assume resources to be permanent, i.e., they are
acquired and released later at the end of a (sub-)process. Since resources are
never created, nor destroyed, the process state space is explicitly bounded.
To study a more general case of arbitrary resource transformations (that can
arise, for example, in open and/or adaptive workflow systems), in [8] WF-nets
with resources (RWF-nets) were defined. RWF-nets extended RCWF-nets from [15]
in such a way that resources can be generated or consumed during a process
execution without any restrictions. Unfortunately, even 1-sound RWF-nets are
not bounded in general, hence existing soundness checking algorithms are no
applicable in that case. The decidability of soundness for RFW-nets was shown
for a restricted case, in which a RWF-net has a single unbounded resource
place.

There are also other works that propose more high-level extensions of
classical WF-nets as well as the related notion(s) of soundness. In [19, 11,
20], the authors investigated data-aware soundness for data Petri nets, in
which a net is extended with guards manipulating a finite set of variables
associated with the net. That type of soundness was shown to be decidable. In
[21], the authors proposed both a workflow variant of $\nu$-Petri nets as well
as its resource-aware extension. The authors also defined a suitable notion of
soundness for such nets and demonstrated that it is decidable by reducing the
soundness checking problem to a verification task over another first order
logic-based formalism. [14, 13] considered the soundness property for BPMN
process models with data objects that can be related to multiple cases. The
approach consists of several transformation steps: from BPMN to a colored
Petri net and then to a resource-constrained workflow net. The authors then
check k-soundness against the latter.

##  8 Conclusions

In this work, we investigated a notion of soundness for a workflow variant of
the recently proposed formalism of object-centric Petri nets, in which each
object type is associated with a dedicated workflow net. Given this structural
characteristic, proposed soundness focuses only on local termination of a
single instance of an object type and assumes that the entire net can have any
number of tokens being assigned to other dedicated workflows. We also
conjectured that checking this new variant of soundness is decidable.

## References

  * [1] van der Aalst, W.M.P.: The application of petri nets to workflow management. J. Circuits Syst. Comput. 8(1), 21–66 (1998). https://doi.org/10.1142/S0218126698000043
  * [2] van der Aalst, W.M.P., Barthelmess, P., Ellis, C.A., Wainer, J.: Workflow modeling using proclets. In: Etzion, O., Scheuermann, P. (eds.) Cooperative Information Systems, 7th International Conference, CoopIS 2000, Eilat, Israel, September 6-8, 2000, Proceedings. Lecture Notes in Computer Science, vol. 1901, pp. 198–209. Springer (2000). https://doi.org/10.1007/10722620_20
  * [3] van der Aalst, W.M.P., Barthelmess, P., Ellis, C.A., Wainer, J.: Proclets: A framework for lightweight interacting workflow processes. Int. J. Cooperative Inf. Syst. 10(4), 443–481 (2001). https://doi.org/10.1142/S0218843001000412
  * [4] van der Aalst, W.M.P., Berti, A.: Discovering object-centric petri nets. Fundam. Informaticae 175(1-4), 1–40 (2020). https://doi.org/10.3233/FI-2020-1946
  * [5] 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)
  * [6] van der Aalst, W.M.P., ter Hofstede, A.H.M., Kiepuszewski, B., Barros, A.P.: Workflow patterns. Distributed Parallel Databases 14(1), 5–51 (2003). https://doi.org/10.1023/A:1022883727209
  * [7] Barkaoui, K., Benayed, R., Sbai, Z.: Workflow Soundness Verification Based on Structure Theory of Petri Nets. International Journal of Computing and Information Sciences (IJCIS) 5, 51–62 (2007)
  * [8] Bashkin, V.A., Lomazova, I.A.: Decidability of k-Soundness for Workflow Nets with an Unbounded Resource, pp. 1–18. Springer (2014)
  * [9] Fahland, D.: Artifact-centric process mining. In: Encyclopedia of Big Data Technologies. Springer (2019)
  * [10] Fahland, D.: Describing behavior of processes with many-to-many interactions. In: Proc. of Petri nets 2019. pp. 3–24. Springer (2019)
  * [11] Felli, P., de Leoni, M., Montali, M.: Soundness verification of decision-aware process models with variable-to-variable conditions. In: ACSD. pp. 82–91. IEEE (2019)
  * [12] Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Petri nets with parameterised data - modelling and verification. In: Fahland, D., Ghidini, C., Becker, J., Dumas, M. (eds.) BPM’20. Lecture Notes in Computer Science, vol. 12168, pp. 55–74. Springer (2020). https://doi.org/10.1007/978-3-030-58666-9_4
  * [13] Haarmann, S., Montali, M., Weske, M.: Technical report: Refining case models using cardinality constraints. CoRR abs/2012.02245 (2020)
  * [14] Haarmann, S., Weske, M.: Cross-case data objects in business processes: Semantics and analysis. In: BPM (Forum). Lecture Notes in Business Information Processing, vol. 392, pp. 3–17. Springer (2020)
  * [15] van Hee, K.M., Serebrenik, A., Sidorova, N., Voorhoeve, M.: Soundness of resource-constrained workflow nets. In: ICATPN. Lecture Notes in Computer Science, vol. 3536, pp. 250–267. Springer (2005)
  * [16] van Hee, K.M., Sidorova, N., Voorhoeve, M.: Generalised soundness of workflow nets is decidable. In: ICATPN. Lecture Notes in Computer Science, vol. 3099, pp. 197–215. Springer (2004)
  * [17] van Hee, K.M., Sidorova, N., Voorhoeve, M., van der Werf, J.M.E.M.: Generation of database transactions with petri nets. Fundam. Inform. 93(1-3), 171–184 (2009)
  * [18] Jensen, K., Kristensen, L.M.: Coloured Petri Nets - Modelling and Validation of Concurrent Systems. Springer (2009)
  * [19] de Leoni, M., Felli, P., Montali, M.: A holistic approach for soundness verification of decision-aware process models. In: ER. Lecture Notes in Computer Science, vol. 11157, pp. 219–235. Springer (2018)
  * [20] de Leoni, M., Felli, P., Montali, M.: Strategy synthesis for data-aware dynamic systems with multiple actors. In: KR. pp. 315–325 (2020)
  * [21] Montali, M., Rivkin, A.: Model checking petri nets with names using data-centric dynamic systems. Formal Aspects Comput. 28(4), 615–641 (2016). https://doi.org/10.1007/s00165-016-0370-6
  * [22] Polyvyanyy, A., van der Werf, J.M.E.M., Overbeek, S., Brouwers, R.: Information systems modeling: Language, verification, and tool support. In: Giorgini, P., Weber, B. (eds.) Advanced Information Systems Engineering - 31st International Conference, CAiSE 2019, Rome, Italy, June 3-7, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11483, pp. 194–212. Springer (2019). https://doi.org/10.1007/978-3-030-21290-2_13
  * [23] Sidorova, N., Stahl, C.: Soundness for resource-constrained workflow nets is decidable. IEEE Trans. Syst. Man Cybern. Syst. 43(3), 724–729 (2013)