22 2162 Methods for Efficient Unfolding of Colored Petri Nets

# Methods for Efficient Unfolding of Colored Petri Nets

Alexander Bilgram  Peter G. Jensen  Thomas Pedersen
Jiří Srba, Peter H. Taankvist
Aalborg University
Department of Computer Science Address for correspondence: Aalborg University,
Department of Computer Science, Aalborg, Denmark.

Received April 2022; accepted January 2023. Aalborg  Denmark
<EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

Colored Petri nets offer a compact and user friendly representation of the
traditional Place/Transition (P/T) nets and colored nets with finite color
ranges can be unfolded into the underlying P/T nets, however, at the expense
of an exponential explosion in size. We present two novel techniques based on
static analysis in order to reduce the size of unfolded colored nets. The
first method identifies colors that behave equivalently and groups them into
equivalence classes, potentially reducing the number of used colors. The
second method overapproximates the sets of colors that can appear in places
and excludes colors that can never be present in a given place. Both methods
are complementary and the combined approach allows us to significantly reduce
the size of multiple colored Petri nets from the Model Checking Contest
benchmark. We compare the performance of our unfolder with state-of-the-art
techniques implemented in the tools MCC, Spike and ITS-Tools, and while our
approach is competitive w.r.t. unfolding time, it also outperforms the
existing approaches both in the size of unfolded nets as well as in the number
of answered model checking queries from the 2021 Model Checking Contest.

††volume: 189††issue: 3-4

##  1 Introduction

Petri nets [1], also known as P/T nets, are a powerful modelling formalism
supported by a rich family of verification techniques [2]. However, P/T nets
often become too large and incomprehensible for humans to read. Therefore,
colored Petri nets (CPN) [3] were introduced to allow for high level modelling
of distributed systems. In CPNs, each place is assigned a color domain and
each token in that place has a color from its domain. Arcs have expressions
that define what colored tokens to consume or produce, and transitions have
guard expressions that restrict transition enabledness.

A CPN can be translated into an equivalent P/T net, provided that every color
domain is finite, through a process called unfolding. This allows us to use
efficient verification tools already developed for P/T nets. When unfolding a
CPN, each place is unfolded into a new place for each color that a token can
take in that place; a naive approach is to create a new place for each color
in the color domain of the place. Transitions are unfolded such that each
binding of variables to colors, satisfying the guard, is unfolded into a new
transition copy in the unfolded net. The size of an unfolded net can be
exponentially larger than the colored net and the unfolding process therefore
requires optimizations in order to finish in realistic time and memory.
Several types of improvements were proposed that analyse transition guards and
arc expressions [4, 5, 6]. However, even with these optimizations, there still
exist CPNs that cannot be unfolded using the existing tools. As an example,
the largest instances of the nets FamilyReunion [7, 8] and DrinkVendingMachine
[9, 10] from the Model Checking Contest [11] have not yet been unfolded in the
competition setup.

We propose two novel methods for statically analysing a CPN to reduce the size
of the unfolded P/T net. The first method called color quotienting uses the
fact that sometimes tokens with different colors can be indistinguishable in
the sense that they generate bisimilar behaviour. If such colors exist in the
net, we can create equivalence classes that represent the colors with similar
behaviour. As such, we can reduce the amount of colors that we need to
consider when unfolding. The second method called color approximation
overapproximates which colors can possibly be present in any given place such
that we only unfold places for the colors that can exist. This method also
allows for invalidating bindings that are dependent on unreachable colors,
thus reducing the amount of transitions that are unfolded.

Our two methods are implemented in the model checker TAPAAL [12, 13] and an
extensive experimental evaluation shows convincing performance compared to the
state-of-the-art tools for CPN unfolding.

#### Related work.

Heiner et al. [5] analyse the arc and guard expressions to reduce the amount
of bindings by collecting patterns. The pattern analysis is implemented in the
tool Snoopy [14] and our color approximation method further extends this
method. In [6] the same authors present a technique for representing the
patterns as Interval Decision Diagrams. This technique is used in the tools
Snoopy [14], MARCIE [15] and Spike [16] and performs better compared to [5];
it also allows to unfold a superset of colored nets compared to the format
adopted by the Model Checking Contest benchmark [11].

In [4] Dal-Zilio describes a method (part of the unfolder MCC) called stable
places. A stable place is a place that never changes from the initial marking,
i.e. every time a token is consumed from this place an equivalent token of the
same color is added to the place. This method is especially efficient on the
net BART from the Model Checking Contest [11], however, it does not detect
places that deviate even a little from the initial marking. Our color
approximation method includes a more general form of the stable places. In the
unfolder MCC [4], a component analysis is introduced and it detects if a net
consists of a number of copies of the same component. MCC is used in the TINA
toolchain [17] and to our knowledge in the latest release of the LoLA tool
[18]. GreatSPN [19] is another tool for unfolding CPNs, however, in [4] it is
demonstrated that MCC is able to greatly outperform GreatSPN and as such we
omit GreatSPN from later experiments.

ITS-Tools [20] has an integrated unfolding engine. The tool uses a technique
of variable symmetry identification, in which it is analyzed whether variables
$x$ and $y$ are permutable in a binding. Furthermore, they use stable places
during the binding and they apply analysis to choose the binding order of
parameters to simplify false guards as soon as possible. After unfolding, ITS-
Tools applies further post-unfolding reductions that remove orphan
places/transitions and behaviourally equivalent transitions [21]. Our
implementation includes a variant of the symmetric variables reduction as
well. In [22] Thierry-Mieg et al. present a technique for automatic detection
of symmetries in high level Petri nets used to construct symbolic reachability
graphs in the GreatSPN tool. This detection of symmetries is reminiscent of
the color quotienting method presented in this paper, although our color
quotienting method is used for unfolding the colored Petri net instead of
symbolic modelchecking.

In [23] Klostergaard presents a simple unfolding method implemented in TAPAAL
[12, 13], which is the base of our implementation. The implementation is
efficient but there are several nets which it cannot unfold. Both unfolding
methods introduced in this paper are advanced static analyses techniques and
we observe that the above mentioned techniques, except symmetric variables and
component analysis, are captured by color approximation and/or color
quotienting.

This paper is an extended version of the conference paper [24] with full
proofs, complete definitions and additional examples and last but not least a
substantial reimplementation of the methods in the tool TAPAAL with improved
experimential results compared to [24].

##  2 Preliminaries

Let $\mathbb{N}^{>0}$ be the set of positive integers and $\mathbb{N}^{0}$ the
set of nonnegative integers. A Labeled Transition System (LTS) is a triple
$(Q,Act,\xrightarrow{})$ where $Q$ is a set of states, $Act$ is a finite,
nonempty set of actions, and $\xrightarrow{}\subseteq Q\times Act\times Q$ is
the transition relation. We write $s\xrightarrow{a}$ if there is
$s^{\prime}\in Q$ such that $s\xrightarrow{a}s^{\prime}$ and
$s\not\xrightarrow{a}$ if there is no such $s^{\prime}$. A binary relation $R$
over the set of states of an LTS is a _bisimulation_ iff for every
$(s_{1},s_{2})\in R$ and $a\in Act$ it holds that if
$s_{1}\xrightarrow{a}s_{1}^{\prime}$ then there is a transition
$s_{2}\xrightarrow{a}s_{2}^{\prime}$ such that
$(s_{1}^{\prime},s_{2}^{\prime})\in R$, and if
$s_{2}\xrightarrow{a}s_{2}^{\prime}$ then there is a transition
$s_{1}\xrightarrow{a}s_{1}^{\prime}$ such that
$(s_{1}^{\prime},s_{2}^{\prime})\in R$. Two states $s$ and $s^{\prime}$ are
_bisimilar_ , written $s\sim s^{\prime}$, iff there is a bisimulation $R$ such
that $(s,s^{\prime})\in R$.

A finite _multiset_ over some nonempty set $A$ is a collection of elements
from $A$ where each element occurs in the multiset a finite amount of times; a
multiset $S$ over a set $A$ can be identified with a function
$S:A\xrightarrow{}\mathbb{N}^{0}$ where $S(a)$ is the number of occurrences of
element $a\in A$ in the multiset $S$. We shall represent multisets by a formal
sum $\sum_{a\in A}S(a)^{\prime}(a)$ such that e.g.
$1^{\prime}(x)+2^{\prime}(y)$ stands for a multiset containing one element $x$
and two elements $y$. We assume the standard multiset operations of membership
($\in$), inclusion ($\subseteq$), equality ($=$), union ($\uplus$),
subtraction ($\setminus$) and by $|S|$ we denote the cardinality of $S$
(including the repetition of elements). By $\mathcal{S}(A)$ we denote the set
of all multisets over the set $A$.

Finally, we also define the function set as a way of reducing multisets of
colors to sets of colors given by
$\textit{set}(S)\mathrel{\stackrel{{\scriptstyle\makebox[0.0pt]{\mbox{\tiny
def}}}}{{=}}}\\{a\ |\ a\in S\\}$ where $\textit{set}(S)$ is the set of all
colors with at least one occurrencein $S$.

###  2.1 Colored Petri nets

Colored Petri nets (CPN) are an extension of traditional P/T nets introduced
by Kurt Jensen [3] in 1981. In CPNs, places are associated with color domains
where colors represent the values of tokens. Arc expressions describe what
colors to consume and add to places depending on a given binding (assignment
of variables to colors). Transitions may contain guards restricting which
bindings are valid. There exist several different definitions of CPNs from the
powerful version defined in [25] that includes the ML language for describing
arcs expressions and guards to less powerful ones such as the one used in the
Model Checking Contest [11]. We shall first give an abstract definition of a
CPN.

###### Definition 2.1

A colored Petri net is a tuple
$\mathcal{N}=(P,T,\mathbb{C},\mathbb{B},C,G,W,W_{I},M_{0})$ where

  1. 1.

$P$ is a finite set of places,

  2. 2.

$T$ is a finite set of transitions such that $P\cap T=\emptyset$,

  3. 3.

$\mathbb{C}$ is a nonempty set of colors,

  4. 4.

$\mathbb{B}$ is a nonempty set of bindings,

  5. 5.

$C:P\xrightarrow{}2^{\mathbb{C}}\setminus\emptyset$ is a place color type
function,

  6. 6.

$G:T\times\mathbb{B}\xrightarrow{}\\{\mathit{true},\mathit{false}\\}$ is a
guard evaluation function,

  7. 7.

$W\\!:((P\times T)\cup(T\times
P))\times\mathbb{B}\xrightarrow{}\mathcal{S}(\mathbb{C})$ is an arc evaluation
function such that $\textit{set}(W((p,t),b))\\!\subseteq C(p)$ and
$\textit{set}(W((t,p),b))\subseteq C(p)$ for all $p\in P$, $t\in T$ and
$b\in\mathbb{B}$,

  8. 8.

$W_{I}:P\times T\xrightarrow{}\mathbb{N}^{>0}\cup\\{\infty\\}$ is an inhibitor
arc weight function, and

  9. 9.

$M_{0}$ is the initial marking where a marking $M$ is a function
$M\\!:\\!P\xrightarrow{}\mathcal{S}(\mathbb{C})$ such that
$\textit{set}(M(p))\\!\subseteq C(p)$ for all $p\in P$.

In this definition, we assume an abstract set of bindings $\mathbb{B}$,
representing the concrete configurations a net can be in. For example, colored
Petri nets often use variables on the arcs and in the guards, and these
variables can be assigned concrete colors. Such a variable assignment is then
referred to as a binding. Notice that $G$ and $W$ are semantic functions which
are in different variants of CPN defined by a concrete syntax. These functions
take as an argument a binding and for this binding return either whether the
guard is true or false, or in case of $W$ the function returns the multiset of
tokens that should be consumed/produced when a transition is fired.

The set of all markings on a CPN $\mathcal{N}$ is denoted by
$\mathbb{M}(\mathcal{N})$. In order to avoid the use of partial functions, we
allow $W((p,t),b)=W((t,p),b)=\emptyset$ and $W_{I}(p,t)=\infty$, meaning that
if the arc evaluation function returns the empty multiset then the arc has no
effect on transition firing and if the inhibitor arc function returns infinity
then it never inhibits the connected transition.

Let $\mathcal{N}=(P,T,\mathbb{C},\mathbb{B},C,G,W,W_{I},M_{0})$ be a fixed CPN
for the rest of this section. Let
$B(t)\mathrel{\stackrel{{\scriptstyle\makebox[0.0pt]{\mbox{\tiny
def}}}}{{=}}}\\{b\in\mathbb{B}\ |\ G(t,b)=\textit{true}\\}$ be the set of all
bindings that satisfy the guard of transition $t\in T$. Let
$\ell:T\xrightarrow{}Act$ be a transition labeling function. The semantics of
a CPN $\mathcal{N}$ is defined as an LTS
$L(\mathcal{N})=(\mathbb{M}(\mathcal{N}),Act,\xrightarrow{})$ where
$\mathbb{M}(\mathcal{N})$ is the set of states defined as all markings on
$\mathcal{N}$, $Act$ is the set of actions, and $M\xrightarrow{a}M^{\prime}$
iff there exists $t\in T$ where $\ell(t)=a$ and there is $b\in B(t)$ such that

$\displaystyle W((p,t),b)\subseteq M(p)\text{ and }W_{I}(p,t)>|M(p)|\text{ for
all }p\in P,\text{ and}$ $\displaystyle M^{\prime}(p)=(M(p)\setminus
W((p,t),b))\uplus W((t,p),b)\text{ for all }p\in P.$

We denote the firing of a transition $t\in T$ in marking $M$ reaching
$M^{\prime}$ as $M\xrightarrow{t}M^{\prime}$. Let
$\xrightarrow{}=\textstyle\bigcup_{t\in T}\xrightarrow{t}$ and let
$\xrightarrow{}^{*}$ be the reflexive and transitive closure of
$\xrightarrow{}$.

###### Remark 2.2

To reason about model checking of CPNs, we need to have a finite
representation of colored nets that can be passed as an input to an algorithm.
One way to enforce such a representation is to assume that all color domains
are finite and the semantic functions $C$, $G$, $W$ and $W_{I}$ are
effectively computable.

Finally, let us define the notion of postset and preset of $p\in P$ as
$p^{\bullet}=\\{t\in T\mid\exists b\in\mathbb{B}.\ W((p,t),b)\neq\emptyset\\}$
and ${}^{\bullet}p=\\{t\in T\mid\exists b\in\mathbb{B}.\
W((t,p),b)\neq\emptyset\\}$. Similarly, for a transition $t\in T$ we define
$t^{\bullet}=\\{p\in P\mid\exists b\in\mathbb{B}.\ W((t,p),b)\neq\emptyset\\}$
and ${}^{\bullet}t=\\{p\in P\mid\exists b\in\mathbb{B}.\
W((p,t),b)\neq\emptyset\\}$. We also define the preset of inhibitor arcs as
${}^{\circ}t=\\{p\in P\ |\ W_{I}(p,t)\neq\infty\\}$.

###  2.2 P/T nets

A Place/Transition (P/T) net is a CPN
$\mathcal{N}=(P,T,\mathbb{C},\mathbb{B},C,G,W,W_{I},M_{0})$ with one color
$\mathbb{C}=\\{\bullet\\}$ and only one binding
$\mathbb{B}=\\{b_{\upepsilon}\\}$ such that every guard evaluates to true i.e.
$G(t,b_{\upepsilon})=\textit{true}$ for all $t\in T$ and every arc evaluates
to a multiset over $\\{\bullet\\}$ i.e.
$W((p,t),b_{\upepsilon})\in\mathcal{S}(\\{\bullet\\})$ and
$W((t,p),b_{\upepsilon})\in\mathcal{S}(\\{\bullet\\})$ for all $p\in P$ and
$t\in T$.

###  2.3 Integer colored Petri nets

An integer CPN (as used for example in the Model Checking Contest [11]) is a
CPN

$\mathcal{N}=(P,T,\mathbb{C},\mathbb{B},C,G,W,W_{I},M_{0})$

where all colors are integer products i.e.
$\mathbb{C}=\textstyle\bigcup_{k\geq 1}(\mathbb{N}^{0})^{k}$. We use interval
ranges to describe sets of colors such that a tuple of ranges
$([a_{1},b_{1}],...,[a_{k},b_{k}])$ where $a_{i},b_{i}\in\mathbb{N}^{0}$ for
$i,1\leq i\leq k$, describes the set of colors $\\{(c_{1},...,c_{k})\ |\
a_{i}\leq c_{i}\leq b_{i}\text{ for all }1\leq i\leq k\\}$. If the interval
upper-bound is smaller than the lower-bound, the interval range denotes the
empty set and by $[a]$ we denote the singleton interval $[a,a]$. As an
example, consider the place color type of some place $p$ as
$C(p)=\llbracket([1,2],[6,7])\rrbracket$ describing the set of colors
$\\{(1,6),(1,7),(2,6),(2,7)\\}$. For notational convenience, we sometimes omit
the semantic paranthesis and simply write $([1,2],[6,7])$ instead of
$\llbracket([1,2],[6,7])\rrbracket$.

We use the set of variables $\mathcal{V}=\\{x_{1},...,x_{n}\\}$ to represent
colors. Variables can be present on arcs and in guards. A binding
$b:\mathcal{V}\xrightarrow{}\mathbb{C}$ assigns colors to variables. We write
$b\equiv\langle x_{1}=c_{1},...,x_{n}=c_{n}\rangle$ for a binding where
$b(x_{i})=c_{i}$ for all $i$, $1\leq i\leq n$. We now introduce the syntax of
arc/guard expressions and its intuitive semantics by an example.

Figure 1(a) shows an integer CPN where places (circles) are associated with
ranges. The initial marking contains five tokens (two of color $0$ and three
of color $2$) in $p_{1}$ and two tokens of color $5$ in place $p_{2}$. There
is a guard on transition $t$ (rectangle) that compares $x$ with the integer
$1$ and restricts the valid bindings. We can see that the arc from $t$ to
$p_{3}$ creates a product of the integers $x$ and $y$, where the value of $x$
is decremented by one. We assume that all ranges are cyclic, meaning that the
predecessor of $0$ in the color set $A$ is $2$. Figure 1(a) also shows an
example of transition firing. Markings are written as formal sums showing how
many tokens of what colors are in the different places. The transition $t$ can
fire only once, as the inhibitor arc (for unlabelled inhibitor arcs we assume
the default weight 1) from place $p_{3}$ to transition $t$ inhibits the second
transition firing.

$1^{\prime}(x-1,y)$$1^{\prime}(x)$$1^{\prime}(y)$$t$$x<1$[$A$][$B$][$AB$]$\begin{array}[]{l}2^{\prime}(0)\\\
3^{\prime}(2)\end{array}$$2^{\prime}(5)$Declarations:color set
$A=([0,2])$color set $B=([4,5])$color set $AB=A\times B$variable $x:A$variable
$y:B$$p_{1}$$p_{2}$$p_{3}$

$p_{1}:(2^{\prime}(0)+3^{\prime}(2))\ +\
p_{2}:2^{\prime}(5)$$\xrightarrow{t}$$p_{1}:(1^{\prime}(0)+3^{\prime}(2))\ +\
p_{2}:1^{\prime}(5)\ +\ p_{3}:(1^{\prime}((2,5)))$

(a) Integer CPN and transition firing under the binding $\langle
x=0,y=5\rangle$

$p_{1}(0)$$p_{1}(1)$$p_{1}(2)$$p_{3}(\mathbf{sum})$$p_{2}(4)$$p_{2}(5)$$p_{3}((0,4))$$p_{3}((0,5))$$p_{3}((1,4))$$p_{3}((1,5))$$p_{3}((2,4))$$p_{3}((2,5))$$t(\langle
x=0,y=4\rangle)$$t(\langle x=0,y=5\rangle)$

(b) Unfolding of CPN from Figure 1(a)

Figure 1: A CPN and its Unfolding to a P/T net

We shall now present the formal syntax of arc expressions and guards. In
integer CPNs, each arc $(P\times T)\cup(T\times P)$ excluding inhibitor arcs
is assigned an arc expression $\alpha$ given by the syntax:

$\displaystyle\alpha::=n^{\prime}(\tau_{1},...,\tau_{k})\ |\
\alpha_{1}\pm\alpha_{2}\ |\ n\cdot\alpha$ $\displaystyle\tau::=c\ |\ x\ |\
x\pm s\ $

where $c\in\mathbb{C}$, $x\in\mathcal{V}$, $s\in\mathbb{N}^{>0}$,
$n\in\mathbb{N}^{>0}$ and $\pm::=+\ |\ -$. The $\alpha$ expressions allow us
to make tuples consisting of $\tau$ expressions that can be combined using
multiset union ($+$) and subtraction ($-$), or multiplied by $n$ (creating $n$
copies of the tuple). The expressions of type $\tau$ are called simple arc
expressions. The semantics of arc expressions is straightforward and
demonstrated by the following example.

###### Example 2.3

Let $a$ be an arc annotated by the arc expression
$1^{\prime}(x-1)+1^{\prime}(y+1)+1^{\prime}(z)$ and let $b_{1}=\langle
x=3,y=3,z=1\rangle$ and $b_{2}=\langle x=1,y=2,z=2\rangle$ be bindings with
integer range $([1,3])$ over the variables $x,y$ and $z$. The CPN semantics of
the arc $a$ is defined as the multiset where
$W(a,b_{1})=1^{\prime}(2)+2^{\prime}(1)$ since the colors are cyclic in nature
such that $3+1=1$ and $W(a,b_{2})=2^{\prime}(3)+1^{\prime}(2)$ because
$1-1=3$.

Guards in integer CPNs are expressed by the following syntax:

$\gamma::=\mathit{true}\ |\ \mathit{false}\ |\ \neg\gamma\ |\
\gamma_{1}\wedge\gamma_{2}\ |\ \gamma_{1}\vee\gamma_{2}\ |\
\alpha_{1}=\alpha_{2}\ |\ \alpha_{1}\neq\alpha_{2}\ |\
\tau_{1}\bowtie\tau_{2}\ $

where $\bowtie\ ::=<\ |\ \leq\ |\ >\ |\ \geq\ |\ =\ |\ \neq$ and where
$\alpha_{1}$ and $\alpha_{2}$ are arc expressions and $\tau_{1}$ and
$\tau_{2}$ are simple arc expressions. The semantics of guards (their
evaluation to true or false in a given binding) is also straightforward and
demonstrated by an example.

###### Example 2.4

Let $g=(x>2\wedge y=2)\vee z+2=3$ be a guard on a transition $t$ and let
$b_{1}=\langle x=3,y=3,z=1\rangle$ and $b_{2}=\langle x=1,y=2,z=2\rangle$ be
bindings with range $([1,3])$ over the variables $x,y$ and $z$. Then
$G(t,b_{1})=\textit{true}$ and $G(t,b_{2})=\textit{false}$.

The Model Checking Contest [11] further includes color types called dots and
cyclic enumerations which are excluded from these definitions as these can be
trivially translated to tuples of integer ranges. The color type dot,
$\\{\bullet\\}$, is represented by the color domain $([1])$ and a cyclic
enumeration with elements $\\{e_{1},e_{2},...,e_{n}\\}$ is encoded as the
integer range $([1,n])$ corresponding to the indices of the cyclic
enumeration. Furthermore, the contest uses the .all expression, which creates
one of each color in the color domain. For example if $A=([0,2])$ then
$A.all=1^{\prime}(1)+1^{\prime}(2)+1^{\prime}(3)$.

All examples in this paper are expressed in integer CPN syntax.

###  2.4 Unfolding of CPNs

CPNs with finite color domains can be unfolded into an equivalent P/T net
[26]. Each place $p$ is unfolded into $|C(p)|$ places, a transition is made
for each legal binding and we translate the multiset of colors on the arc to a
multiset over $\bullet$. We now provide a formal definition of unfolding in
our syntax, following the approach from [23, 27] that also consider inhibitor
arcs.

For each place connected to an inhibitor arc, we create a fresh summation
place that contains the sum of tokens across the rest of the unfolded places.
The summation places are created to ensure that inhibitor arcs work correctly
after unfolding.

######  Definition 2.5 (Unfolding)

Let $\mathcal{N}=(P,T,\mathbb{C},\mathbb{B},C,G,W,W_{I},M_{0})$ be a colored
Petri net. The unfolded P/T net
$\mathcal{N}^{u}=(P^{u},T^{u},\mathbb{C}^{u},\mathbb{B}^{u},C^{u},G^{u},W^{u},W_{I}^{u},M_{0}^{u})$
is given by

  1. 1.

$P^{u}=\\{p(c)\ |\ p\in P\wedge c\in C(p)\\}\cup\\{p({\textbf{sum}})\ |\ t\in
T,p\in{}^{\circ}t\\},$

  2. 2.

$T^{u}=\bigcup_{t\in T}\bigcup_{b\in B(t)}t(b),$

  3. 3.

$\mathbb{C}^{u}=\\{\bullet\\}$,

  4. 4.

$\mathbb{B}^{u}=\\{b_{\upepsilon}\\}$,

  5. 5.

$C^{u}(p(c))=\\{\bullet\\}$ for all $p(c)\in P^{u}$,

  6. 6.

$G^{u}(t(b),b_{\upepsilon})=\textit{true}$ for all $t(b)\in T^{u}$,

  7. 7.

$W^{u}((p(c),t(b)),b_{\upepsilon})=W((p,t),b)(c)^{\prime}(\bullet)\text{ and
}W^{u}((t(b),p(c)),b_{\upepsilon})=\\\ W((t,p),b)(c)^{\prime}(\bullet)$ for
all $p(c)\in P^{u}$ and $t(b)\in T^{u}$, and
$W^{u}((p(\textbf{sum}),t(b)),b_{\upepsilon})=|W((p,t),b)|^{\prime}(\bullet)\text{
and }W^{u}((t(b),p(\textbf{sum})),b_{\upepsilon})=\\\
|W((t,p),b)|^{\prime}(\bullet)$ for all $p(\textbf{sum})\in P^{u}$ and
$t(b)\in T^{u}$,

  8. 8.

$W_{I}^{u}(p(\textbf{sum}),t(b))=W_{I}(p,t)$ for all $p(\textbf{sum})\in
P^{u}$ and $t(b)\in T^{u}$, and

  9. 9.

$M_{0}^{u}(p(c))=M_{0}(p)(c)^{\prime}(\bullet)$ for all $p(c)\in P^{u}$ and
$M_{0}^{u}(p(\textbf{sum}))=|M_{0}(p)|^{\prime}(\bullet)$ for all
$p(\textbf{sum})\in P^{u}$

where $p(\textbf{sum})$ denotes the sum of all tokens regardless of the color
for the place $p$.

Consider the CPN in Figure 1(a). The unfolded version of this can be seen in
Figure 1(b). We notice that each place of the CPN is unfolded to a fresh new
place for every color in the color type of the place as well as a sum place
for $p_{3}$. Additionally, the transition is unfolded to a new transition for
each legal binding.

The theorem showing that the unfolded net is bisimilar to the original CPN was
proved in [23, 27]; we only added a small optimization on the summation
places.

######  Theorem 2.6 ([23, 27])

Given a colored Petri net
$\mathcal{N}=(P,T,\mathbb{C},\mathbb{B},C,G,W,W_{I},M_{0})$ and the unfolded
P/T net
$\mathcal{N}^{u}=(P^{u},T^{u},\mathbb{C}^{u},\mathbb{B}^{u},C^{u},G^{u},W^{u},W_{I}^{u},M_{0}^{u})$,
it holds that $M_{0}\sim M_{0}^{u}$ with the labeling function $\ell(t(b))=t$
for all $t(b)\in T^{u}$.

##  3 Color quotienting

Unfolding a CPN without any further analysis will often lead to many
unnecessary places and transitions. We shall now present our first technique
that allows to group equivalently behaving colors into equivalence classes in
order to reduce the number of colors and hence also to reduce the size of the
unfolded net.

As an example consider the CPN in Figure 2(a), the unfolded version of this
net adds five places for both $p_{1}$ and $p_{2}$. However, we see that in
$p_{1}$ all colors greater than or equal to $3$ behave exactly the same
throughout the net and can thus be represented by a single color. We can thus
quotient the CPN by partitioning the color domain of each place into a number
of equivalence classes of colors such that the colors behaving equivalently
are represented by the same equivalence class. Using this approach, we can
construct a bisimilar CPN seen in Figure 2(b) where the color $3$ now
represents all colors greater than or equal to $3$.

Such a reduction in the number of colors is possible to include already during
the design of a CPN model, however, the models may look less intuitive for
human modeller or the nets can be auto-generated and hence contain
redundant/equivalent colors as observed in the benchmark of CPN models from
the annual Model Checking Contest benchmark [11].

$p_{1}$[$A$]$1^{\prime}(x)$$1^{\prime}(x)$$p_{2}$[$A$]$t_{1}$$x<3$$A.all$$1^{\prime}(x)$$t_{2}$Declarations:Color
set $\displaystyle A=([1,5])$variable $\displaystyle x:A$$x\leq 1$

(a) Example CPN

$p_{1}$[A]$1^{\prime}(x)$$1^{\prime}(x)$$p_{2}$[A]$t_{1}$$x<3$$\begin{array}[]{l}1^{\prime}(1)\\\
1^{\prime}(2)\\\
3^{\prime}(3)\end{array}$$1^{\prime}(x)$$t_{2}$Declarations:Color set
$\displaystyle A=([1,3])$variable $\displaystyle x:A$Color 1 represents
$\displaystyle([1])$Color 2 represents $\displaystyle([2])$Color 3 represents
$\displaystyle([3,5])$$x\leq 1$

(b) Quotiented net from Figure 2(a)

$M_{1}=p_{1}:1^{\prime}(1)$$\xrightarrow{t_{1}}$$M_{2}=p_{1}:1^{\prime}(2)$$M_{1}^{\prime}=p_{2}:1^{\prime}(1)$$M_{2}^{\prime}=p_{2}:1^{\prime}(2)$$\xrightarrow{t_{1}}$$M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}$$M_{1}^{\prime}\centernot{\stackrel{{\scriptstyle\delta}}{{\equiv}}}M_{2}^{\prime}$$\delta(p_{1})=\\{([1,2]),([3,5])\\},\delta(p_{2})=\\{([1]),([2,5])\\}$

(c) Example of an unstable partition $\delta$ and markings showing why it is
unstable

$\delta^{\prime}(p_{1})=\\{([1]),([2]),([3,5])\\},\delta^{\prime}(p_{2})=\\{([1]),([2,5])\\}$

(d) Example of stable partition $\delta^{\prime}$

Figure 2: Quotienting example

We thus introduce color partition on places where all colors with similar
behaviour in a given place are grouped into an equivalence class, denoted by
$\theta$. For the rest of this section, let us assume a fixed CPN
$\mathcal{N}=(P,T,\mathbb{C},\mathbb{B},C,G,W,W_{I},M_{0})$. A partition
$\delta$ is a function
$\delta:P\xrightarrow{}2^{2^{\mathbb{C}}}\setminus\emptyset$ that for a place
$p$ returns the equivalence classes of $C(p)$ such that
$(\textstyle\bigcup_{\theta\in\delta(p)}\theta)=C(p)$ and
$\theta_{1}\cap\theta_{2}=\emptyset$ for all
$\theta_{1},\theta_{2}\in\delta(p)$ where $\theta_{1}\neq\theta_{2}$.

###### Definition 3.1

Given a partition $\delta$ and markings $M$ and $M^{\prime}$, we write
$M(p)\stackrel{{\scriptstyle\delta}}{{\equiv}}M^{\prime}(p)$ for a $p\in P$
iff for all $\theta\in\delta(p)$ it holds that
$\textstyle\sum_{c\in\theta}M(p)(c)=\textstyle\sum_{c\in\theta}M^{\prime}(p)(c)$.
We write $M\stackrel{{\scriptstyle\delta}}{{\equiv}}M^{\prime}$ iff
$M(p)\stackrel{{\scriptstyle\delta}}{{\equiv}}M^{\prime}(p)$ for all $p\in P$.
A partition $\delta$ is _stable_ if the relation
$\stackrel{{\scriptstyle\delta}}{{\equiv}}$ on markings induced by $\delta$ is
a bisimulation.

Consider the CPN in Figure 2(a). The partition shown in the Figure 2(c) is not
stable as demonstrated by the transition firing from $M_{1}$ and $M_{2}$ to
$M_{1}^{\prime}$ resp. $M_{2}^{\prime}$ where
$M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}$ but
$M_{1}^{\prime}\centernot{\stackrel{{\scriptstyle\delta}}{{\equiv}}}M_{2}^{\prime}$.
Figure 2(d) shows an example of a stable partition (here we describe the
partition with integer ranges in the same manner as in integer CPNs).

We now show how a CPN can be quotiented using a stable partition. First, we
define the notion of binding equivalence under a partition.

###### Definition 3.2

Given a partition $\delta$, a transition $t\in T$ and bindings
$b,b^{\prime}\in B(t)$, we write
$b\stackrel{{\scriptstyle\delta,t}}{{\equiv}}b^{\prime}$ iff for all
$p\in{}^{\bullet}t$ and for all $\theta\in\delta(p)$ it holds that

$\textstyle\sum_{c\in\theta}W((p,t),b)(c)=\textstyle\sum_{c\in\theta}W((p,t),b^{\prime})(c)$

and for all $p\in t^{\bullet}$ and for all $\theta\in\delta(p)$ it holds that

$\textstyle\sum_{c\in\theta}W((t,p),b)(c)=\textstyle\sum_{c\in\theta}W((t,p),b^{\prime})(c).$

We can now define classes of equivalent bindings given a partition $\delta$
which are bindings that have the same behaviour for a given transition,
formally
$B^{\delta}(t)\\!\mathrel{\stackrel{{\scriptstyle\makebox[0.0pt]{\mbox{\tiny
def}}}}{{=}}}\\!\\{[b]_{t}\ |\ b\\!\in\\!B(t)\\}\text{ where
}[b]_{t}\\!=\\{b^{\prime}\ |\
b^{\prime}\stackrel{{\scriptstyle\delta,t}}{{\equiv}}~{}b\\}$.

For a given stable partition, we now construct a quotiented CPN where the set
of colors are the equivalence classes of the stable partition and the set of
bindings are the equivalence classes of bindings. As such, we rewrite the arc
and guard evaluation functions to instead consider an equivalence class of
bindings, which is possible since each binding in the equivalence class
behaves equivalently.

###### Definition 3.3

Let $\mathcal{N}=(P,T,\mathbb{C},\mathbb{B},C,G,W,W_{I},M_{0})$ be a CPN and
$\delta$ a stable partition of $\mathcal{N}$. The quotiented CPN
$\mathcal{N}^{\delta}=(P,T,\mathbb{C}^{\delta},\mathbb{B}^{\delta},C^{\delta},G^{\delta},W^{\delta},W_{I}^{\delta},M^{\delta}_{0})$
is defined by

  1. 1.

$\mathbb{C}^{\delta}=\textstyle\bigcup_{p\in P}\delta(p)$

  2. 2.

$\mathbb{B}^{\delta}=\biguplus_{t\in T}B^{\delta}(t)$.

  3. 3.

$G^{\delta}(t,[b]_{t})=G(t,b)$ for all $t\in T$ and $[b]_{t}\in B(t)$,

  4. 4.

$C^{\delta}(p)=\delta(p)$ for all $p\in P$,

  5. 5.

$W^{\delta}((p,t),[b]_{t})=S\text{ where
}S(\theta)=\textstyle\sum_{c\in\theta}W((p,t),b)(c)\text{ for all
}\theta\in\delta(p)$ and
$W^{\delta}((t,p),[b]_{t})=S\text{ where
}S(\theta)=\textstyle\sum_{c\in\theta}W((t,p),b)(c)\text{ for all
}\theta\in\delta(p)$
for all $p\in P$, $t\in T$ and $[b]_{t}\in\mathbb{B}^{\delta}$,

  6. 6.

$W_{I}^{\delta}(p,t)$ = $W_{I}(p,t)$ for all $p\in P$ and $t\in T$, and

  7. 7.

$M^{\delta}_{0}(p)=S\text{ where
}S(\theta)=\textstyle\sum_{c\in\theta}M_{0}(p)(c)$ for all $p\in P$ and
$\theta\in\delta(p)$.

We can now present our main correctness theorem, stating that the original and
quotiented colored nets are bisimilar.

###### Theorem 3.4

Let $\mathcal{N}=(P,T,\mathbb{C},\mathbb{B},C,G,W,W_{I},M_{0})$ be a CPN,
$\delta$ a stable partition and
$\mathcal{N}^{\delta}=(P^{\delta},T^{\delta},\mathbb{C}^{\delta},\mathbb{B}^{\delta},C^{\delta},G^{\delta},W^{\delta},W_{I}^{\delta},M_{0}^{\delta})$
the quotiented CPN. Then $M_{0}\sim M^{\delta}_{0}$.

###### Proof 3.5

We show that $R=\\{(M,M^{\delta})\ |\
\textstyle\sum_{c\in\theta}M(p)(c)=M^{\delta}(p)(\theta)\text{ for all }p\in
P\text{ and all }\theta\in\delta(p)\\}$ is a bisimulation relation. We first
notice that $(M_{0},M^{\delta}_{0})\in R$ by Item 7 in Definition 3.3.

Assume that $(M,M^{\delta})\in R$ and $t\in T$ such that
$M\xrightarrow{t}M^{\prime}$ under binding $b\in B(t)$, we want to show that
$M^{\delta}\xrightarrow{t}M^{\delta\prime}$ under binding $[b]_{t}\in B(t)$
such that $(M^{\prime},M^{\delta\prime})\in R$. As such, we need to prove the
following:

$\displaystyle\bm{(a)}\quad$ $\displaystyle W^{\delta}((p,t),[b]_{t})\subseteq
M^{\delta}(p)\text{ for all }p\in P$ $\displaystyle\bm{(b)}\quad$
$\displaystyle W_{I}^{\delta}(p,t)>|M^{\delta}(p)|\text{ for all }p\in P$
$\displaystyle\bm{(c)}\quad$ $\displaystyle(M^{\prime},M^{\delta\prime})\in
R\text{ where }M^{\delta\prime}(p)=(M^{\delta}(p)\setminus
W^{\delta}((p,t),[b]_{t}))\uplus W^{\delta}((t,p),[b]_{t})$
$\displaystyle\text{for all }p\in P\ .$

$\bm{(a)}$ We start by showing $W^{\delta}((p,t),[b]_{t})\subseteq
M^{\delta}(p)$ for all $p\in P$. First, because $(M,M^{\delta})\in R$, we know
that

$\textstyle\sum_{c\in\theta}M(p)(c)=M^{\delta}(p)(\theta)\text{ for all }p\in
P\text{ and all }\theta\in\delta(p).$ (1)

Since $W((p,t),b)\subseteq M(p)$ we know for all $c\in C(p)$ that
$W((p,t),b))(c)\leq M(p)(c)$ which implies that

$\textstyle\sum_{c\in\theta}W((p,t),b))(c)\leq\textstyle\sum_{c\in\theta}M(p)(c)$
(2)

for all $\theta\in\delta(p)$. We now show that
$W^{\delta}((p,t),[b]_{t})\subseteq M^{\delta}(p)$ for all $p\in P$ i.e.
$W^{\delta}((p,t),[b]_{t})(\theta)\leq M^{\delta}(p)(\theta)$ for all
$\theta\in\delta(p)$:

$W^{\delta}((p,t),[b]_{t})(\theta)$ |  = |  substitute by Def. 3.3 Item 5
---|---|---
$\textstyle\sum_{c\in\theta}W((p,t),b))(c)$ |  $\leq$ |  by Equation (2)
$\textstyle\sum_{c\in\theta}M(p)(c)$ |  = |  by Equation (1)
$M^{\delta}(p)(\theta)$ . |  |

$\bm{(b)}$ Next we show $W_{I}^{\delta}((p,t)>|M^{\delta}(p)|$. We know that

$W_{I}(p,t)>|M(p)|$ (3)

by definition of CPN semantics since $M\xrightarrow{t}M^{\prime}$. We then
observe that for all $p\in P$, it holds

$W^{\delta}_{I}(p,t)$ |  = |  substitute by Def. 3.3 Item 6
---|---|---
$W_{I}(p,t)$ |  > |  by Equation (3)
$|M(p)|$ |  = | multiset definition
$\textstyle\sum_{c\in C(p)}M(p)(c)$ |  = |  since $(\textstyle\bigcup_{\theta\in\delta(p)}\theta)=C(p)$
$\textstyle\sum_{\theta\in\delta(p)}\textstyle\sum_{c\in\theta}M(p)(c)$ |  = |  by Equation (1)
$\textstyle\sum_{\theta\in\delta(p)}M^{\delta}(p)(\theta)$ |  = | multiset definition
$|M^{\delta}(p)|$ . |  |

$\bm{(c)}$ Lastly, we show that $(M^{\prime},M^{\delta\prime})\in R$. Assume
$p\in P$, $b\in B(t)$ and equivalence class $[b]_{t}$. We know that
$M^{\prime}(p)=(M(p)\setminus W((p,t),b))\uplus W((t,p),b)$ and
$M^{\delta\prime}(p)=(M^{\delta}(p)\setminus W^{\delta}((p,t),[b]_{t}))\uplus
W^{\delta}((t,p),[b]_{t})$ and we need to show that
$\textstyle\sum_{c\in\theta}M^{\prime}(p)(c)=M^{\delta\prime}(p)(\theta)$ for
all $\theta\in\delta(p)$:

$\textstyle\sum_{c\in\theta}M^{\prime}(p)(c)$ |  = | by def. of CPN semantics
---|---|---
$\textstyle\sum_{c\in\theta}(M(p)\setminus W((p,t),b)\uplus W((t,p),b))(c)$ |  = |  | substitute by multiset definitions
---
and by enabledness of $t$
|
$\textstyle\sum_{c\in\theta}M(p)(c)-\textstyle\sum_{c\in\theta}W((p,t),b)(c)$
---
$+\textstyle\sum_{c\in\theta}W((t,p),b)(c)$
= |  substitute by Def. 3.3 Item 5
| $\textstyle\sum_{c\in\theta}M(p)(c)-W^{\delta}((p,t),[b]_{t})(\theta)$
---
$+W^{\delta}((t,p),[b]_{t})(\theta)$
= |  since $(M,M^{\delta})\in R$
| $M^{\delta}(p)(\theta)-W^{\delta}((p,t),[b]_{t})(\theta)$
---
$+W^{\delta}((t,p),[b]_{t})(\theta)$
= | by definition of CPN semantics
$M^{\delta\prime}(p)(\theta)$ . |  |

We then have to show that the same is the case for the opposite direction such
that assume $(M,M^{\delta})\in R$ and $t\in T$ such that
$M^{\delta}\xrightarrow{t}M^{\delta\prime}$, we want to show that
$M\xrightarrow{t}M^{\prime}$ for some $b\in B(t)$ such that
$(M^{\prime},M^{\delta\prime})\in R$. As such, we want to show that:

$\displaystyle\bm{(d)}\quad$ $\displaystyle W((p,t),b)\subseteq M(p)\text{ for
all }p\in P$ $\displaystyle\bm{(e)}\quad$ $\displaystyle
W_{I}(p,t)>|M(p)|\text{ for all }p\in P$ $\displaystyle\bm{(f)}\quad$
$\displaystyle(M^{\prime},M^{\delta\prime})\in R\text{ where
}M^{\prime}(p)=(M(p)\setminus W((p,t),b))\uplus W((t,p),b)$
$\displaystyle\text{for all }p\in P\ .$

We first notice that $\bm{(e)}$ and $\bm{(f)}$ can be showed by the same
argumentation as $\bm{(b)}$ and $\bm{(c)}$. For the case $\bm{(d)}$, we show
that $W((p,t),b)\subseteq M(p)\text{ for all }p\in P$. From $\bm{(a)}$ we know
that $W^{\delta}((p,t),[b]_{t})\subseteq M^{\delta}(p)$ which implies
$\textstyle\sum_{c\in\theta}W((p,t),b))(c)\leq\textstyle\sum_{c\in\theta}M(p)(c)$
for all $\theta\in\delta(p)$ and $p\in P$.

Hence observe that there exists a marking $M_{1}$ such that
$\textstyle\sum_{c\in\theta}M_{1}(p)(c)=M^{\delta}(p)(\theta)$ and where
$\textstyle\sum_{c\in\theta}W((p,t),b)(c)\leq\textstyle\sum_{c\in\theta}M_{1}(p)(c)$
for all $\theta\in\delta(p)$ and $p\in P$. Clearly $t$ is enabled in $M_{1}$
since $W((p,t),b)\subseteq M_{1}(p)$ for all $p\in P$ by the multiset
definition of $\subseteq$ and we know that the inhibitor arcs do not inhibit
the transition by $\bm{(e)}$.

We then want to show that $M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M$,
i.e.
$\textstyle\sum_{c\in\theta}M_{1}(p)(c)=\textstyle\sum_{c\in\theta}M(p)(c)$
for all $\theta\in\delta(p)$ and $p\in P$. Since $(M,M^{\delta})\in R$ we know
that
$\textstyle\sum_{c\in\theta}M(p)(c)=M^{\delta}(p)(\theta)=\textstyle\sum_{c\in\theta}M_{1}(p)(c)$
for all $\theta\in\delta(p)$ and $p\in P$ and thus
$M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M$. Since $\delta$ is stable we
know that $t$ is enabled in $M$.

Thus we know that the opposite direction also holds meaning that $R$ is a
bisimulation.

###  3.1 Computing stable partitions

Our main challenge is how to efficiently compute a stable partition in order
to apply the quotienting technique. To do so, we first define a partition
refinement.

###### Definition 3.6

Given two partitions $\delta$ and $\delta^{\prime}$ we write
$\delta\geq\delta^{\prime}$ if for all $p\in P$ and all
$\theta^{\prime}\in\delta^{\prime}(p)$ there exists $\theta\in\delta(p)$ such
that $\theta^{\prime}\subseteq\theta$. Additionally, we write
$\delta>\delta^{\prime}$ if $\delta\geq\delta^{\prime}$ and
$\delta^{\prime}\neq\delta$.

Note that for any finite CPN as assumed in Remark 2.2, the refinement relation
$>$ is well-founded as for any $\delta>\delta^{\prime}$ the partition
$\delta^{\prime}$ has strictly more equivalence classes for at least one place
$p\in P$. We now define also the union of two partitions as the smallest
partition that has both of the partitions as refinements.

###### Definition 3.7

Given two partitions $\delta_{1}$, $\delta_{2}$ and $p\in P$, let
$\xleftrightarrow{}$ be a relation over $\delta_{1}(p)\cup\delta_{2}(p)$ such
that $\theta\xleftrightarrow{}\theta^{\prime}\textit{ iff
}\theta\cap\theta^{\prime}\neq\emptyset$ where
$\theta,\theta^{\prime}\in\delta_{1}(p)\cup\delta_{2}(p)$. Let
$\xleftrightarrow{}^{*}$ be the reflexive, transitive closure of
$\xleftrightarrow{}$ and let
$[\theta]\mathrel{\stackrel{{\scriptstyle\makebox[0.0pt]{\mbox{\tiny
def}}}}{{=}}}\textstyle\bigcup_{\theta^{\prime}\in\delta_{1}(p)\cup\delta_{2}(p),\theta\xleftrightarrow{}^{*}\theta^{\prime}}\theta^{\prime}$
where $\theta\in\delta_{1}(p)\cup\delta_{2}(p)$. Finally, we define the
partition union operator $\sqcup$ by
$(\delta_{1}\sqcup\delta_{2})(p)=\textstyle\bigcup_{\theta\in\delta_{1}(p)\cup\delta_{2}(p)}\\{[\theta]\\}\text{
for all }p\in P$.

For example, assume some place $p$ such that $C(p)=\\{([1,5])\\}$ and
partitions $\delta_{1}$ and $\delta_{2}$ such that
$\delta_{1}(p)=\\{([1,2]),([3,4]),([5])\\}$ and
$\delta_{2}(p)=\\{([1]),([2,3]),([4]),([5])\\}$ then
$(\delta_{1}\sqcup\delta_{2})(p)=\\{([1,4]),([5])\\}$.

###### Lemma 3.8

Let $\delta_{1}$ and $\delta_{2}$ be two partitions. Then (i)
$\delta_{1}\sqcup\delta_{2}\geq\delta_{1}$ and
$\delta_{1}\sqcup\delta_{2}\geq\delta_{2}$, and (ii) if $\delta_{1}$ and
$\delta_{2}$ are stable partitions then so is $\delta_{1}\sqcup\delta_{2}$.

###### Proof 3.9

For the first part of the claim, from definition of partition union, we see
that $[\theta]$ is the union of any $\theta^{\prime}$ that overlaps with
$\theta$ and $\delta_{1}\sqcup\delta_{2}$ just collects all such unions for
every $\theta$. As such, it is trivial that for any $\theta\in\delta_{1}(p)$
there exists $\theta^{\prime}\in\delta_{1}(p)\sqcup\delta_{2}(p)$ such that
$\theta\subseteq\theta^{\prime}$ for all $p\in P$, in other words
$\delta_{1}\sqcup\delta_{2}\geq\delta_{1}$. The same is the case for
$\delta_{2}$.

For the second part of the claim, let $\delta=\delta_{1}\sqcup\delta_{2}$.
Assume $M$ and $M^{\prime}$ such that
$M\stackrel{{\scriptstyle\delta}}{{\equiv}}M^{\prime}$ i.e. for all $p\in P$
and all $[\theta]\in\delta(p)$ it holds that
$\textstyle\sum_{c\in[\theta]}M(p)(c)=\textstyle\sum_{c\in[\theta]}M^{\prime}(p)(c)$.
We want to show that $\delta$ is stable, i.e that
$\stackrel{{\scriptstyle\delta}}{{\equiv}}$ is a bisimulation relation, while
assuming that $\stackrel{{\scriptstyle\delta_{1}}}{{\equiv}}$ and
$\stackrel{{\scriptstyle\delta_{2}}}{{\equiv}}$ are bisimulation relations.
Assume a fixed $p\in P$. From definition of partition union, we get that for
every fixed $[\theta]\in\delta(p)$ and for all $c,c^{\prime}\in[\theta]$ there
exist $c_{1},...,c_{k}\in[\theta]$ such that $c,c_{1}\in\theta_{1}$,
$c_{1},c_{2}\in\theta_{2}$, $c_{2},c_{3}\in\theta_{3}$, …,
$c_{k},c^{\prime}\in\theta_{k}$, where
$\theta_{i}\in\delta_{1}(p)\cup\delta_{2}(p)$ for all $i,1\leq i\leq k$. Let
us define markings $M_{i}$, for $1\leq i\leq k$, such that
$M_{i}(p)(c_{i})=\textstyle\sum_{c\in[\theta]}M(p)(c)$ and $M_{i}(p)(c)=0$ if
$c\neq c_{i}$ and $c\in[\theta]$, otherwise $M_{i}(p)(c)=M(p)(c)$. In other
words, in order to obtain $M_{i}$, we replace in $M$ all colors in the
equivalence class $[\theta]$ with the color $c_{i}$ and obtain the chain
$M(p)\stackrel{{\scriptstyle\delta_{j_{1}}}}{{\equiv}}M_{1}(p)\stackrel{{\scriptstyle\delta_{j_{2}}}}{{\equiv}}M_{2}(p)\stackrel{{\scriptstyle\delta_{j_{3}}}}{{\equiv}}...\stackrel{{\scriptstyle\delta_{j_{k}}}}{{\equiv}}M_{k}(p)$
where $j_{i}\in\\{1,2\\}$, i.e. $M_{i}$ and $M_{i+1}$ are related either by
$\stackrel{{\scriptstyle\delta_{1}}}{{\equiv}}$ or
$\stackrel{{\scriptstyle\delta_{2}}}{{\equiv}}$, both of them being
bisimulation relations. We can also observe that
$M(p)\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{k}(p)$. We can then repeat
this process for all other equivalence classes in $\delta(p)$ in order to
conclude that $M(p)\stackrel{{\scriptstyle\delta}}{{\equiv}}M^{\prime}(p)$.
The same process can then be applied to all $p\in P$, implying that
$M\stackrel{{\scriptstyle\delta}}{{\equiv}}M^{\prime}$. Hence there is a chain
of markings as above starting from $M$ and ending in $M^{\prime}$. Since
$\delta_{1}$ and $\delta_{2}$ are stable, meaning that both
$\stackrel{{\scriptstyle\delta_{1}}}{{\equiv}}$ and
$\stackrel{{\scriptstyle\delta_{2}}}{{\equiv}}$ are bisimulation relations,
this implies that every transition from $M$ can be (by transitivity) matched
by a transition from $M^{\prime}$ and vice versa, implying that
$\stackrel{{\scriptstyle\delta}}{{\equiv}}$ is a bisimulation relation and
$\delta$ is so stable.

The lemma above implies the existence of a unique maximum stable partition.

###### Theorem 3.10

There is a unique maximum stable partition $\delta$ such that
$\delta\geq\delta^{\prime}$ for all stable partitions $\delta^{\prime}$.

###### Proof 3.11

We prove this by contradiction. Assume two maximum stable partitions
$\delta_{1}$ and $\delta_{2}$ where $\delta_{1}\neq\delta_{2}$. By Lemma 3.8
(ii) we know that $\delta_{1}\sqcup\delta_{2}$ is stable and by Lemma 3.8 (i)
we know that $\delta_{1}\sqcup\delta_{2}\geq\delta_{1}$ and
$\delta_{1}\sqcup\delta_{2}\geq\delta_{2}$. Thus $\delta_{1}$ and $\delta_{2}$
cannot both be maximum stable partitions.

In order to provide an algorithm for computing a stable partition, we define
the maximum arc size for a given CPN $\mathcal{N}$ as the function
$\textit{max}(\mathcal{N})=\max_{p\in P,t\in
T,b\in\mathbb{B}}(|W((p,t),b)|,|W((t,p),b)|)$. The set of all markings smaller
than the max arc size over $\mathcal{N}$ is defined by
$\mathbb{M}^{bounded}(\mathcal{N})=\\{M\in\mathbb{M}(\mathcal{N})\ |\
|M(p)|\leq\textit{max}(\mathcal{N})\text{ for all }p\in P\\}$. As such,
$\mathbb{M}^{bounded}(\mathcal{N})$ is a finite set of all bounded markings of
$\mathcal{N}$ with cardinality less than or equal to
$\textit{max}(\mathcal{N})$.

In order to compute stable partitions we need to show some properties for
markings in $\mathbb{M}^{bounded}(\mathcal{N})$. The following lemma shows
that if there are two non-bisimilar markings that break the fact that the
relation $\stackrel{{\scriptstyle\delta}}{{\equiv}}$ is a bisimulation, then
there are also two markings that are bounded and that also break the
bisimulation property.

###### Lemma 3.12

Let $\mathcal{N}$ be a CPN and $\delta$ a partition. Then for all $t\in T$ it
holds that

  1. $\bm{(a)}$

if there exist $M_{1},M_{2}\in\mathbb{M}(\mathcal{N})$ such that
$M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}$,
$M_{1}\xrightarrow{t}\text{ and }\ M_{2}\centernot{\xrightarrow{t}}$ then
there exist $M_{3},M_{4}\in\mathbb{M}^{bounded}$ such that
$M_{3}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{4}$,
$M_{3}\xrightarrow{t}\text{ and }\ M_{4}\centernot{\xrightarrow{t}}$, and

  2. $\bm{(b)}$

if there exist $M_{1},M_{2}\in\mathbb{M}(\mathcal{N})$ where
$M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}$ and there exists
$M_{1}^{\prime}\in\mathbb{M}(\mathcal{N})$ such that
$M_{1}\xrightarrow{t}M_{1}^{\prime}$ and for all
$M_{2}^{\prime}\in\mathbb{M}(\mathcal{N})$ where
$M_{2}\xrightarrow{t}M_{2}^{\prime}$ it holds that
$M_{1}^{\prime}\centernot{\stackrel{{\scriptstyle\delta}}{{\equiv}}}M_{2}^{\prime}$
then there exists $M_{3},M_{4}\in\mathbb{M}^{bounded}(\mathcal{N})$ where
$M_{3}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{4}$ and there exists
$M_{3}^{\prime}\in\mathbb{M}^{bounded}(\mathcal{N})$ such that
$M_{3}\xrightarrow{t}M_{3}^{\prime}$ and for all
$M_{4}^{\prime}\in\mathbb{M}^{bounded}(\mathcal{N})$ where
$M_{4}\xrightarrow{t}M_{4}^{\prime}$ it holds that
$M_{3}^{\prime}\centernot{\stackrel{{\scriptstyle\delta}}{{\equiv}}}M_{4}^{\prime}$.

###### Proof 3.13

Recall that $\textit{max}(\mathcal{N})$ is defined as the largest cardinality
of all arc multisets in $\mathcal{N}$, i.e.
$|W((p,t),b)|\leq\textit{max}(\mathcal{N})$ for all $p\in P$ and $b\in B(t)$.

  1. $\bm{(a)}$

Let $M_{1},M_{2}\in\mathbb{M}(\mathcal{N})$ such that
$M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}$,
$M_{1}\xrightarrow{t}\text{ and }\ M_{2}\centernot{\xrightarrow{t}}$. We
construct a marking $M_{3}$ such that $M_{3}(p)=W((p,t),b)$ for all $p\in P$
and some $b\in B(t)$. It clearly follows that
$|M_{3}(p)|\leq\textit{max}(\mathcal{N})$ for all $p\in P$, hence
$M_{3}\in\mathbb{M}^{bounded}(\mathcal{N})$. We see that
$M_{1}(p)=M_{3}(p)\uplus\overline{M}_{3}(p)$ since $M_{3}(p)\subseteq
M_{1}(p)$ for all $p\in P$ where $\overline{M}_{3}(p)$ describes the remaining
tokens in $M_{1}(p)$ that are not in $M_{3}(p)$. We know that no inhibitor arc
can be the reason that $M_{2}$ is not enabled because
$M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}$. We also know that
$M_{2}(p)\centernot{\subseteq}W((p,t),b)$ for at least one $p\in P$ for all
$b\in B(t)$.

We pick a marking $M_{4}$ where
$M_{4}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{3}$,
$M_{4}(p)\centernot{\subseteq}W((p,t),b)$ for at least one $p\in P$ and
$M_{2}(p)=M_{4}(p)\uplus\overline{M}_{4}(p)$ for all $p\in P$ such that
$\overline{M}_{4}\stackrel{{\scriptstyle\delta}}{{\equiv}}\overline{M}_{3}$.
Notice that $M_{4}\in\mathbb{M}^{bounded}(\mathcal{N})$. We know that $M_{4}$
exists because $M_{2}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{1}$ and
$M_{2}(p)\centernot{\subseteq}W((p,t),b)$ meaning that
$M_{4}(p)\uplus\overline{M}_{4}(p)\centernot{\subseteq}W((p,t),b)$ and thus
$M_{4}(p)\centernot{\subseteq}W((p,t),b)$ for some $p\in P$.

  2. $\bm{(b)}$

Let $M_{1},M_{2}\in\mathbb{M}(\mathcal{N})$ such that
$M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}$ and
$M_{1}^{\prime}\in\mathbb{M}(\mathcal{N})$ such that
$M_{1}\xrightarrow{t}M_{1}^{\prime}$ while for all
$M_{2}^{\prime}\in\mathbb{M}(\mathcal{N})$ where
$M_{2}\xrightarrow{t}M_{2}^{\prime}$ we know that
$M_{1}^{\prime}\centernot{\stackrel{{\scriptstyle\delta}}{{\equiv}}}M_{2}^{\prime}$.
We construct a marking $M_{3}$ exactly as before such that
$M_{3}(p)=W((p,t),b)$ for all $p\in P$ and some $b\in B(t)$ and
$M_{1}(p)=M_{3}(p)\uplus\overline{M}_{3}(p)$ for all $p\in P$.

We then pick a marking $M_{4}$ such that
$M_{4}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{3}$ and
$M_{2}(p)=M_{4}(p)\uplus\overline{M}_{4}(p)$ for all $p\in P$ and $b\in B(t)$
such that
$\overline{M}_{4}\stackrel{{\scriptstyle\delta}}{{\equiv}}\overline{M}_{3}$.
We know that $M_{4}\in\mathbb{M}^{bounded}(\mathcal{N})$ since
$M_{4}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{3}$. Let
$M_{3}^{\prime}\in\mathbb{M}^{bounded}(\mathcal{N})$ such that
$M_{3}\xrightarrow{t}M_{3}^{\prime}$, which is possible because
$M_{3}(p)\subseteq M_{1}(p)$ for all $p\in P$ such that no inhibitor arc can
inhibit $M_{3}$. For the sake of contradiction now assume there exists a
marking $M_{4}^{\prime}\in\mathbb{M}^{bounded}(\mathcal{N})$ such that
$M_{4}\xrightarrow{t}M_{4}^{\prime}$ and
$M_{3}^{\prime}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{4}^{\prime}$. Then
notice that we can let
$M_{1}^{\prime}(p)=M_{3}^{\prime}(p)\uplus\overline{M}_{3}(p)$ where
$M_{1}\xrightarrow{t}M_{1}^{\prime}$ since $M_{3}(p)\subseteq M_{1}(p)$ for
all $p\in P$ and let
$M_{2}^{\prime}(p)=M_{4}^{\prime}(p)\uplus\overline{M_{4}}(p)$ where
$M_{2}\xrightarrow{t}M_{2}^{\prime}$ since $M_{4}(p)\subseteq M_{2}(p)$ for
all $p\in P$. But since
$M_{3}^{\prime}(p)\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{4}^{\prime}(p)$
and
$\overline{M}_{3}(p)\stackrel{{\scriptstyle\delta}}{{\equiv}}\overline{M}_{4}(p)$
it means that
$M_{3}^{\prime}(p)\uplus\overline{M}_{3}(p)\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{4}^{\prime}(p)\uplus\overline{M_{4}}(p)$
for all $p\in P$, i.e.
$M_{1}^{\prime}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}^{\prime}$.
However, this contradicts the conditions of $\bm{(b)}$, and as such
$M_{3}^{\prime}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{4}^{\prime}$ cannot
hold.

1 Input: $\mathcal{N}=(P,T,\mathbb{C},\mathbb{B},C,G,W,W_{I},M_{0})$

2 Output: Stable partition $\delta$

3 let $\delta(p):=\\{C(p)\\}$ for all $p\in P$

4 for  _$t\in T$_ do

5 while  _$\exists
M_{1},M_{2}\in\mathbb{M}^{bounded}(\mathcal{N}).M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}\wedge
M_{1}\centernot{\xrightarrow{t}}\wedge M_{2}\xrightarrow{t}$_ do

6 pick $\delta^{\prime}<\delta$ such that
$M_{1}\centernot{\stackrel{{\scriptstyle\delta^{\prime}}}{{\equiv}}}M_{2}$

7 $\delta:=\delta^{\prime}$

8

9 end while

10

11 end for

12let $\mathcal{Q}:=P$ //Waiting list of places

13 while  _$\mathcal{Q}\neq\emptyset$_ do

14 let $p\in\mathcal{Q}$; $\mathcal{Q}:=\mathcal{Q}\setminus\\{p\\}$

15

16 for  _$t\in{}^{\bullet}p$_ do

17 if  _$\exists
M_{1},M_{2}\in\mathbb{M}^{bounded}(\mathcal{N}).M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}.\exists
M_{1}^{\prime}\in\mathbb{M}^{bounded}(\mathcal{N}).M_{1}\xrightarrow{t}M_{1}^{\prime}\wedge\forall
M_{2}^{\prime}\in\mathbb{M}^{bounded}(\mathcal{N}).M_{2}\xrightarrow{t}M_{2}^{\prime}\wedge
M_{1}^{\prime}(p)\centernot{\stackrel{{\scriptstyle\delta}}{{\equiv}}}M_{2}^{\prime}(p)$_
then

18 pick $\delta^{\prime}<\delta$ such that
$M_{1}\centernot{\stackrel{{\scriptstyle\delta^{\prime}}}{{\equiv}}}M_{2}$ and
$\delta^{\prime}(p^{\prime})=\delta(p^{\prime})$ for all $p^{\prime}\in
P\setminus{}^{\bullet}t$

19 $\mathcal{Q}:=\mathcal{Q}\cup\\{p^{\prime}\ |\
\delta^{\prime}(p^{\prime})\neq\delta(p^{\prime})\\}$

20 $\delta:=\delta^{\prime}$

21 end if

22

23 end for

24

25 end while

return $\delta$

Algorithm 1 $\textit{Stabilize}(\mathcal{N})$

Algorithm 1 now gives a procedure for computing a stable partition over a
given CPN. It starts with an initial partition where every color in the color
domain is in the same equivalence class for each place. The algorithm is then
split into two parts. The first part from line 4 to 9 creates an initial
partition applying the guard restrictions to the input places of the
transitions. The second part from line 11 to 20 back propagates the guard
restrictions throughout the net such that only colors that behave the same are
quotiented together. Depending on the choices in lines 6 and 15, the algorithm
may return the maximum stable partition, however in the practical
implementation this is not guaranteed due to an approximation of the guard/arc
expression analysis.

###### Theorem 3.14

Given a CPN $\mathcal{N}$, the algorithm $\textit{Stabilize}(\mathcal{N})$
terminates and returns a stable partition of $\mathcal{N}$.

###### Proof 3.15

We first prove that $\textit{Stabilize}(\mathcal{N})$ terminates. Notice that
each iteration produces a new $\delta$ according to the $>$ operator, and
since the operator is well-founded we know that the algorithm terminates. We
then show that for $\delta=\textit{Stabilize}(\mathcal{N})$, $\delta$ is a
stable partition of $\mathcal{N}$. Recall, a partition $\delta$ is stable iff
for any markings $M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}$
whenever $M_{1}\xrightarrow{t}M_{1}^{\prime}$ for some $t$ and
$M_{1}^{\prime}$ then $M_{2}\xrightarrow{t}M_{2}^{\prime}$ for some
$M_{2}^{\prime}$ such that
$M_{1}^{\prime}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}^{\prime}$. We
prove this by contradiction. Assume that $\delta$ is not a stable partition.
As such there must exists markings $M_{1},M_{2}\in\mathbb{M}(\mathcal{N})$
such that $M_{1}\stackrel{{\scriptstyle\delta}}{{\equiv}}M_{2}$ and there
exists a marking $M_{1}^{\prime}\in\mathbb{M}(\mathcal{N})$ such that
$M_{1}\xrightarrow{t}M_{1}^{\prime}$ for some transition $t$ where for all
$M_{2}^{\prime}\in\mathbb{M}(\mathcal{N})$ such that
$M_{2}\xrightarrow{t}M_{2}^{\prime}$ then
$M_{1}^{\prime}\centernot{\stackrel{{\scriptstyle\delta}}{{\equiv}}}M_{2}^{\prime}$.
This is exactly the property stated in the if statement on line 17 and we know
from Lemma 3.12 that if the property is satisfied with two markings from
$\mathbb{M}(\mathcal{N})$ then there exists two markings from
$\mathbb{M}^{bounded}(\mathcal{N})$ that also satisfy the property.

###  3.2 Stable partition Algorithm for integer CPNs

The Stabilize computation presented in Algorithm 1 can be used to find a
stable partition for any finite CPN. However, implementation-wise it is
inefficient to represent every color in a given equivalence class
individually. Hence, for integer CPN we represent an equivalence class as a
tuple of ranges. As an example of computing stable partitions with Algorithm
1, consider the integer CPN in Figure 2. Table 2 shows the different stages
that $\delta$ undergoes in order to become stable. In iteration 0, the guard
restrictions from the first for-loop are applied, followed by the iterations
of the main while-loop. In our implementation, we do not iterate through every
bounded marking and we instead (for efficiency reasons) statically analyze the
places, arcs and guards in order to partition the color sets. For example, in
iteration number 1, we consider the place $p_{3}$ and we can see that the
colors in the range $[1,3]$ must be distinguished from the color $4$. This
partitioning propagates back to the place $p_{1}$ as firing the transition
$t_{1}$ moves tokens from $p_{1}$ to $p_{3}$ without changing its color.

$p_{1}$$t_{1}$$t_{2}$$1^{\prime}(x)$$1^{\prime}(y)$$1^{\prime}(x,y)$$1^{\prime}(x,y)$$1^{\prime}(y+1)$$t_{3}$$2^{\prime}(x)$$1^{\prime}(x)$$x\
\leq\ 3$$y\ \geq\ 3$$t_{4}$$1^{\prime}(x,y)$$y\ <\ 2$Declarations:Color set
$\displaystyle A=([1,4])$Color set $\displaystyle AA=A\ \times A$variable
$\displaystyle x:A$variable $\displaystyle
y:A$[A][A][A][AA]$1^{\prime}(1)$$1^{\prime}(3)$$p_{2}$$p_{3}$$p_{4}$

Figure 3: Example CPN Table 1: Stages of $\delta$ throughout Algorithm 1 for
CPN in Figure 2. The 0’th iteration is the state of $\delta$ just before the
while loop begins. The symbol ’-’ indicates that the value is the same as in
the previous row.

Iteration | $p_{1}$ | $p_{2}$ | $p_{3}$ | $p_{4}$ | $\mathcal{Q}$
---|---|---|---|---|---
0 | $\\{([1,4])\\}$ | $\\{([1,4])\\}$ | $\\{([1,3]),([4])\\}$ |  | $\\{([1,4],[1]),([1,4],[2]),([1,4],[3,4])\\}$
---
$\\{p_{1},p_{2},p_{3},p_{4}\\}$
1, $p=p_{3}$ | $\\{([1,3]),([4])\\}$ | - | - | - | $\\{p_{1},p_{2},p_{4}\\}$
2, $p=p_{4}$ | - |  |  $\\{([1]),$ $([2]),([3,4])\\}$
---
- | - | $\\{p_{1},p_{2}\\}$
3, $p=p_{2}$ | - | - | - |  | $\\{([1,4],[1]),([1,4],[2]),$
---
$([1,4],[3]),([1,4],[4])\\}$
$\\{p_{1},p_{4}\\}$
4, $p=p_{4}$ | - |  |  $\\{([1]),$ $([2]),([3]),([4])\\}$
---
- | - | $\\{p_{1},p_{2}\\}$
5, $p=p_{2}$ | - | - | - | - | $\\{p_{1}\\}$
6, $p=p_{1}$ | - | - | - | - | $\\{\\}$

Table 2: Stages of $\alpha$ when computing the fixed point of $E$ for the CPN
in Figure 2. The symbol ’-’ indicates that the value is the same as in the
previous row.

Iteration | $p_{1}$ | $p_{2}$ | $p_{3}$ | $p_{4}$
---|---|---|---|---
0, $\alpha=\alpha_{0}$ | $\\{([1])\\}$ | $\\{([3])\\}$ | $\\{\\}$ |  | $\\{\\}$
---
1, $t=t_{1}$ | - | - | $\\{([1])\\}$ | $\\{([1],[3])\\}$
2, $t=t_{2}$ | - | $\\{([3,4])\\}$ | - | -
3, $t=t_{1}$ | - | - | - | $\\{([1],[3,4])\\}$
4, $t=t_{2}$ | - | $\\{([3,4]),([1])\\}$ | - | -
5, $t=t_{1}$ | - | - | - | $\\{([1],[3,4]),([1],[1])\\}$

##  4 Color approximation

We now introduce another technique for safely overapproximating what colors
can be present in each place of a CPN. Let
$\mathcal{N}=(P,T,\mathbb{C},\mathbb{B},C,G,W,W_{I},M_{0})$ be a fixed CPN for
the rest of this section. A _color approximation_ is a function
$\alpha:P\xrightarrow{}2^{\mathbb{C}}$ where $\alpha(p)$ approximates the
possible colors in place $p\in P$ such that $\alpha(p)\subseteq C(p)$. Let
$\mathbb{A}$ be the set of all color approximations. For a marking $M$ and
color approximation $\alpha$, we write $M\subseteq\alpha$ iff
$\textit{set}(M(p))\subseteq\alpha(p)$ for all $p\in P$. A _color expansion_
is a function $E:\mathbb{A}\xrightarrow{}\mathbb{A}$ defined by

$\displaystyle
E(\alpha)(p)=\left\\{\begin{array}[]{lll}&\alpha(p)\cup\textit{set}(W((t,p),b))\textit{
}&\text{if }\exists t\in T.\exists b\in B(t).\\\
&&\textit{set}(W((q,t),b))\subseteq\alpha(q)\text{ for all }q\in P\\\
&\alpha(p)\textit{ }&\text{otherwise.}\end{array}\right.$

A color expansion iteratively expands the possible colors that exist in each
place but without keeping a count of how many tokens of each color are present
(if a color is present in a place, we assume that arbitrary many copies of the
color are present). The expansion function obviously preserves the following
property.

###### Lemma 4.1

Let $\alpha$ be a color approximation then $\alpha(p)\subseteq E(\alpha)(p)$
for all $p\in P$.

Let $\alpha_{0}$ be the initial approximation such that
$\alpha_{0}(p)\mathrel{\stackrel{{\scriptstyle\makebox[0.0pt]{\mbox{\tiny
def}}}}{{=}}}\textit{set}(M_{0}(p))$ for all $p\in P$. Since $E$ is a
monotonic function on a complete lattice, we can compute its minimum fixed
point and formulate the following key lemma.

###### Lemma 4.2

Let $\alpha$ be a minimum fixed point of $E$ such that
$\alpha_{0}(p)\subseteq\alpha(p)$ for all $p\in P$. If
$M_{0}\xrightarrow{}^{*}M$ then $M\subseteq\alpha$.

###### Proof 4.3

By induction on $k$ we prove if $M_{0}\xrightarrow{}^{k}M$ then
$M\subseteq\alpha$. Base step. If $k=0$, we know that $M_{0}\subseteq\alpha$
by the assumption of the lemma. Induction step. Let
$M_{0}\xrightarrow{}^{k}M\xrightarrow{t}M^{\prime}$ by some transition $t$
with some binding $b\in B(t)$. We want to show that
$M^{\prime}\subseteq\alpha$. By induction hypothesis we know that
$M\subseteq\alpha$. If $M\xrightarrow{t}M^{\prime}$ for some $b\in B(t)$, then
$M^{\prime}(p)=(M(p)\setminus W((p,t),b))\uplus W((t,p),b)$ for all $p\in P$.
Since $E(\alpha)$ is a fixed point then
$\alpha(p)=\alpha(p)\cup\textit{set}(W((t,p),b))$ for transition $t$ under
binding $b$ for all $p\in P$ i.e. $\textit{set}(W((q,t),b))\subseteq\alpha(q)$
for all $q\in P$. Thus we get $M^{\prime}\subseteq\alpha$.

Given a color approximation $\alpha$ satisfying the preconditions of Lemma
4.2, we can now construct a reduced CPN
$\mathcal{N}^{\alpha}=(P,T,\mathbb{C},\mathbb{B},C^{\alpha},G,W,W_{I},M_{0})$
where $C^{\alpha}(p)=\alpha(p)$ for all $p\in P$. The net
$\mathcal{N}^{\alpha}$ can hence have possibly smaller set of colors in its
color domains and it satisfies the following theorem.

###### Theorem 4.4

The reachable fragments from the initial marking $M_{0}$ of the LTSs generated
by $\mathcal{N}$ and $\mathcal{N}^{\alpha}$ are isomorphic.

###### Proof 4.5

By Lemma 4.2 we know that $M\subseteq\alpha$ for any marking
$M\in\mathbb{M}(\mathcal{N})$ reachable from $M_{0}$. Since the reachable
fragments of $\mathcal{N}$ and $\mathcal{N}^{\alpha}$ are exactly the
reachable markings, we know that the reachable fragments are isomorphic.

###  4.1 Computing color approximation on integer CPNs

As with color quotienting, representing each color individually becomes
inefficient. We thus employ integer ranges to represent color approximations.
Consider the approximation $\alpha$ where
$\alpha(p)=\\{(1,2),(2,2),(3,2),(5,6),(5,7)\\}$ are possible colors (pairs of
integers) in the place $p$; this can be more compactly represented as a set of
tuples of ranges $\\{([1,3],[2]),([5],[6,7])\\}$.

However, computing the minimum fixed point of $E$ using ranges is not as
trivial as using complete color sets. To do so, we need to compute new ranges
depending on arcs and guards. We demonstrate this on the CPN in Figure 2.
Table 2 shows the computation of the minimum fixed point of $E$, starting from
the initial approximation $\alpha_{0}$. For example, in iteration number 5, we
check if firing transition $t_{1}$ can produce any additional tokens to the
places $p_{3}$ and $p_{4}$. Clearly, there is no change to the possible token
colors in $p_{3}$ as $\alpha(p_{1})$ did not change, however the addition of
the integer range $[1]$ to $\alpha(p_{2})$ in the previous iteration now
allows us to produce a new token color $(1,1)$ into $p_{4}$ and hence we add
the singleton range $([1],[1])$ to $\alpha(p_{4})$. Due to the guard $y\geq 3$
on the transition $t_{2}$, we know that the added token $(1,1)$ does not
generate any further behaviour and hence we reached a fixed point.

##  5 Experiments

We implemented the quotienting method from Section 3 as well as the color
approximation method from Section 4 in C++ as an extension to the verification
engine verifypn [13] from the TAPAAL toolchain [12].

We perform experiments by comparing several different approaches; the
quotienting approach (method A), the color approximation approach (method B)
and the combination of both (method A+B) against

  * •

the unfolder MCC [4] (used also by TINA [17] and LoLA [18]),

  * •

ITS-Tools unfolder [20],

  * •

the Spike unfolder [16] (also used by MARCIE [15] and Snoopy [14]),

  * •

and verifypn TAPAAL unfolder with methods A and B disabled, referred to as
Tapaal.

We compare the tools on the complete set of CPN nets and queries from 2021
Model Checking Contest [11]111We omit the _UtilityControlRoom_ family of
models as they contain operators not supported by ITS-Tools.. The experiments
are conducted on a compute cluster running Linux version 5.4.0, where each
experiment is conducted on a AMD Epyc 7642 processor with a 15 GB memory limit
and 5 minute timeout. To reduce noise in the experiments, we read and write
models to a RAM-disk (not included in the 15 GB). A repeatability package is
available in [28].

We conduct two series of experiments: in Section 5.1 we study the unfolding
performance of the tools; i.e. how fast and how many models can be unfolded by
each tool and how large are the unfolded models, and in Section 5.2 we study
the impact of this unfolding on the ability to answer the queries from the
Model Checking Contest 2021.

###  5.1 Unfolding experiments

Table 3 shows for each of the unfolders the number of unfolded nets within the
memory/time limit. The last column shows the total number of unfolded nets by
all tools combined, and we notice that the combination of methods A$+$B allows
us to unfold a superset of models unfolded by the other tools. Our method
A$+$B can unfold 3 nets that no other tool can unfold; DrinkVendingMachine48,
76, 98. This is directly attributed to method A.

Table 3: Number of unfolded nets for each unfolder |  Spike |  Tapaal |  ITS-Tools |  A |  B |  MCC |  A$+$B |  Total
---|---|---|---|---|---|---|---|---
Unfolded nets |  170 |  192 |  193 |  195 |  200 |  200 |  203 |  203

The comparison of the sizes (total number of transitions and places) of
unfolded nets is done by plotting the ratios between the size produced by our
A+B method and the competing unfolder. Figure 4(a) shows the size ratios where
at least one comparison is not equal to 1. We see that our method has a size
ratio always smaller or equal to 1 (no other method unfolds any of the nets to
a smaller size compared to our method A+B) and the size ratio is strictly
smaller than 1 for 144 colored nets (out of 213 nets in the database).
Moreover, we can reduce 45 nets by at least one order of magnitute, compared
to all other unfolders.

(a) Size-ratios (nondecreasingly ordered)

(b) Worst 80 unfolding times

Figure 4: Unfolding size and unfolding time comparison

As our method outperforms the state-of-the-art unfolders w.r.t. the size of
the unfolded nets, the question is whether the overhead of the advanced static
analysis does not kill the benefits. Fortunately, this is not the case as
shown in Figure 4(b) where the 80 slowest unfolding times (independently
sorted in nondecreasing order for each tool) are depicted. The plots show that
our method has almost a magnitude reduction in running-time compared to ITS-
Tools and MCC (which are close in performance), while Spike is significantly
slower. ITS-Tools is generally fast on the nets that are unfolded in less than
10 seconds, however it becomes gradually slower and has problems unfolding the
larger nets. Our unfolder and the MCC unfolder demonstrate a similar
degradation trend in performance.

The overall conclusion is that our advanced analyses requires less overhead
compared to other existing unfolders, while at the same time it significantly
decreases the size of the unfolded nets.

###  5.2 Query verification experiments

In these experiments, we examine which unfolding engine allows for most query
answers verified on the unfolded nets. To allow for a fair comparison, we let
each tool unfold and output the net to a PNML file. Regarding queries, both
method A$+$B and ITS-Tools can already output the unfolded queries. For MCC,
we implement our own translation from the colored queries to the unfolded
queries for the given nets. For Spike, we were not able to construct a query
unfolder that worked consistently and for this reason Spike is excluded from
the query verification experiments.

Table 4: Number of queries answered for the unfolded nets of each tool. The %
column describes how many percent of the total available queries in each
category were answered. Each category counts $213\cdot 16=3408$ queries.

Cardinality Queries
---
| A+B | MCC | ITS-Tools
| Solved | % | Solved | % | Solved | %
ReachabilityCardinality | 2909 | 85.4 | 2793 | 82.0 | 2759 | 81.0
CTLCardinality | 2651 | 77.8 | 2490 | 73.1 | 2443 | 73.8
LTLCardinality | 2952 | 86.6 | 2818 | 82.7 | 2785 | 81.7
Total | 8512 | 83.3 | 8101 | 79.2 | 7987 | 78.1
Fireability Queries
ReachabilityFireability | 2567 | 75.3 | 2484 | 72.9 | 2513 | 73.7
CTLFireability | 2047 | 60.1 | 1878 | 55.1 | 1695 | 49.7
LTLFireability | 2798 | 82.1 | 2639 | 77.4 | 2520 | 73.9
Total | 7412 | 72.5 | 7001 | 68.5 | 6728 | 65.8
Total query answers | 15924 | 77.9 | 15102 | 73.9 | 14715 | 72.0

Since we are testing the effect of the unfolding and not the verification
engine, we use verifypn (revision 507c8ee0) to verify the queries on the nets
unfolded by the different unfolders. There is a total of 20,448 queries to be
answered. The results can be seen in Table 4.

We see that using the method A$+$B to unfold nets allows us to answer more
queries in every category due to the generally smaller nets it unfolds to. In
total, we are able to answer $4$ percentage points more queries using the
unfolded nets of method A$+$B compared to using the unfolded nets of MCC and
$5.9$ percentage points more compared to ITS-Tools.

##  6 Conclusion

We presented two complementary methods for reducing the unfolding size of
colored Petri nets (CPN). Both methods are proved correct and implemented in
an open-source verification engine of the tool TAPAAL. Experimental results
show a significant improvement in the size of unfolded nets, compared to
state-of-the-art tools, without compromising the unfolding speed. The actual
verification on the models and queries from the 2021 Model Checking Contest
shows that our unfolding technique allows us to solve 4% more queries compared
to the second best competing tool. In future work, we plan to combine our
approach with structural reduction techniques applied directly to the colored
nets.

#### Acknowledgments.

We would like to thank Yann Thierry-Mieg for his answers and modifications to
the ITS-Tools, Silvano Dal Zilio for his answers/additions concerning the MCC
unfolder and Monika Heiner and Christian Rohr for their answers concerning the
tools Snoopie, Marcie and Spike.

## References

  * [1] Petri C.  Kommunikation mit Automaten.  Ph.D. thesis, Institut für instrumentelle Mathematik, Bonn, 1962.
  * [2] Murata T.  Petri nets: Properties, analysis and applications.  _Proceedings of the IEEE_ , 1989.  77(4):541–580.  10.1109/5.24143.
  * [3] Jensen K.  Coloured Petri Nets and the Invariant-Method.  _Theoretical Computer Science_ , 1981.  14:317–336.  10.1016/0304-3975(81)90049-9.
  * [4] Dal Zilio S.  MCC: A Tool for Unfolding Colored Petri Nets in PNML Format.  In: Application and Theory of Petri Nets and Concurrency. Springer International Publishing, Cham, 2020 pp. 426–435.  10.1007/978-3-030-51831-8_23.
  * [5] Liu F, Heiner M, Yang M.  An efficient method for unfolding colored Petri nets.  In: Proceedings of the 2012 Winter Simulation Conference (WSC).  ISBN 978-1-4673-4779-2, 2012 pp. 1–12.  10.1109/WSC.2012.6465203.
  * [6] Schwarick M, Rohr C, Liu F, Assaf G, Chodak J, Heiner M.  Efficient Unfolding of Coloured Petri Nets Using Interval Decision Diagrams, pp. 324–344.  Application and Theory of Petri Nets and Concurrency.  ISBN 978-3-030-51830-1, 2020.  10.1007/978-3-030-51831-8_16.
  * [7] Hillah L.  Family Reunion.  https://mcc.lip6.fr/pdf/FamilyReunion-form.pdf, 2021.
  * [8] Ciaghi A, Weldemariam K, Villafiorita A, Kessler F.  Law Modeling with Ontological Support and BPMN: a Case Study.  _In CYBERLAWS 2011, The Second International Conference on Technical and Legal Aspects of the e-Society_ , 2011.  pp. 29–34.
  * [9] Hillah L.  A hot drink vending machine.  https://mcc.lip6.fr/pdf/DrinkVendingMachine-form.pdf, 2021.
  * [10] Muschevici R, Proença J, Clarke D.  Modular Modelling of Software Product Lines with Feature Nets.  In: Software Engineering and Formal Methods. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011 pp. 318–333.  10.1007/978-3-642-24690-6_22.
  * [11] Kordon F, Bouvier P, Garavel H, Hillah LM, Hulin-Hubard F, Amat N, Amparore E, Berthomieu B, Biswal S, Donatelli D, Galla F, , Dal Zilio S, Jensen P, He C, Le Botlan D, Li S, , Srba J, Thierry-Mieg, Walner A, Wolf K.  Complete Results for the 2021 Edition of the Model Checking Contest.  http://mcc.lip6.fr/2021/results.php, 2021.
  * [12] David A, Jacobsen L, Jacobsen M, Jørgensen K, Møller M, Srba J.  TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets.  In: Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12), volume 7214 of _LNCS_. Springer-Verlag, 2012 pp. 492–497.  10.1007/978-3-642-28756-5_36.
  * [13] Jensen J, Nielsen T, Oestergaard L, Srba J.  TAPAAL and Reachability Analysis of P/T Nets.  _LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC)_ , 2016.  9930:307–318.  10.1007/978-3-662-53401-4_16.
  * [14] Heiner M, Herajy M, Liu F, Rohr C, Schwarick M.  Snoopy – A Unifying Petri Net Tool.  In: Application and Theory of Petri Nets. Springer Berlin Heidelberg, Berlin, Heidelberg.  ISBN 978-3-642-31131-4, 2012 pp. 398–407.  10.1007/978-3-642-31131-4_22.
  * [15] Heiner M, Rohr C, Schwarick M.  MARCIE - Model Checking and Reachability Analysis Done Efficiently.  In: Application and Theory of Petri Nets and Concurrency. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013 pp. 389–399.  10.1007/978-3-642-38697-8_21.
  * [16] Chodak J, Heiner M.  Spike - Reproducible Simulation Experiments with Configuration File Branching.  In: Computational Methods in Systems Biology. Springer International Publishing, Cham.  ISBN 978-3-030-31304-3, 2019 pp. 315–321.  10.1007/978-3-030-31304-3_19.
  * [17] Berthomieu B, Ribet PO, Vernadat F.  The tool TINA — construction of abstract state spaces for Petri nets and time Petri nets.  _International Journal of Production Research_ , 2004.  42:2741–2756.  10.1080/00207540412331312688.
  * [18] Wolf K.  Petri Net Model Checking with LoLA 2.  In: Application and Theory of Petri Nets and Concurrency. Springer International Publishing, Cham.  ISBN 978-3-319-91268-4, 2018 pp. 351–362.  10.1007/978-3-319-91268-4_18.
  * [19] Amparore EG, Balbo G, Beccuti M, Donatelli S, Franceschinis G.  30 Years of GreatSPN.  In: Fiondella L, Puliafito A (eds.), Principles of Performance and Reliability Modeling and Evaluation: Essays in Honor of Kishor Trivedi on his 70th Birthday. Springer International Publishing, Cham.  ISBN 978-3-319-30599-8, 2016 pp. 227–254.  10.1007/978-3-319-30599-8_9.
  * [20] Thierry-Mieg Y.  Symbolic Model-Checking Using ITS-Tools.  In: Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg.  ISBN 978-3-662-46681-0, 2015 pp. 231–237.  10.1007/978-3-662-46681-0_20.
  * [21] Thierry-Mieg Y.  Personal Correspondence with Y. Thierry-Mieg, 2021.
  * [22] Thierry-Mieg Y, Dutheillet C, Mounier I.  Automatic Symmetry Detection in Well-Formed Nets.  In: van der Aalst W, Best E (eds.), Applications and Theory of Petri Nets 2003. Springer Berlin Heidelberg, Berlin, Heidelberg.  ISBN 978-3-540-44919-5, 2003 pp. 82–101.
  * [23] Klostergaard A.  Efficient Unfolding and Approximation of Colored Petri Nets with Inhibitor Arcs.  Master’s thesis, Department of Computer Science, Aalborg University, 2018\.  URL https://projekter.aau.dk/projekter/files/281079031/main.pdf.
  * [24] Bilgram A, Jensen P, Pedersen T, Srba J, Taankvist P.  Improvements in Unfolding of Colored Petri Nets.  In: Proceedings of the 15th International Conference on Reachability Problems (RP’21), volume 13035 of _LNCS_. Springer-Verlag, 2021 pp. 69–84.  10.1007/978-3-030-89716-1_5.
  * [25] Jensen K, Kristensen LM.  Coloured Petri Nets, Modelling and Validation of Concurrent Systems.  Springer-Verlag Berlin Heidelberg, 1 edition, 2009.  10.1007/b95112.
  * [26] Jensen K.  Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. Volume 1, volume 1.  Springer-Verlag Berlin Heidelberg, 2 edition, 1996.  10.1007/978-3-662-03241-1.
  * [27] Christensen N, Glavind M, Schmid S, Srba J.  Latte: Improving the Latency of Transiently Consistent Network Update Schedules.  _SIGMETRICS Perform. Eval. Rev._ , 2021.  48(3):14–26.  10.1145/3453953.3453957.
  * [28] Bilgram A, Peter G J, Pedersen T, Srba J, Taankvist PH.  Repeatability package for: Methods for Efficient Unfolding of Colored Petri Nets, 2022.  URL https://doi.org/10.5281/zenodo.6417272.