22 2102

# Taking Complete Finite Prefixes To High Level, Symbolically111 This is a
revised and extended version of the article [1] that is published in the
Proceedings of PETRI NETS 2023.

Nick Würdemann
Department of Computing Science
University of Oldenburg  Oldenburg  Germany
<EMAIL_ADDRESS>Thomas Chatain
Université Paris-Saclay  INRIA and LMF  CNRS and
ENS Paris-Saclay  Gif-sur-Yvette  France
<EMAIL_ADDRESS>Stefan Haar
Université Paris-Saclay  INRIA and LMF  CNRS and
ENS Paris-Saclay  Gif-sur-Yvette  France
<EMAIL_ADDRESS>Lukas Panneke
Department of Computing Science
University of Oldenburg  Oldenburg  Germany
<EMAIL_ADDRESS>
###### Abstract

Unfoldings are a well known partial-order semantics of P/T Petri nets that can
be applied to various model checking or verification problems. For _high-
level_ Petri nets, the so-called _symbolic_ unfolding generalizes this notion.
A complete finite prefix of a P/T Petri net’s unfolding contains all
information to verify, e.g., reachability of markings. We unite these two
concepts and define complete finite prefixes of the symbolic unfolding of
high-level Petri nets. For a class of safe high-level Petri nets, we
generalize the well-known algorithm by Esparza et al. for constructing small
such prefixes. We evaluate this extended algorithm through a prototype
implementation on four novel benchmark families. Additionally, we identify a
more general class of nets with infinitely many reachable markings, for which
an approach with an adapted cut-off criterion extends the complete prefix
methodology, in the sense that the original algorithm cannot be applied to the
P/T net represented by a high-level net.

###### keywords:

Petri Nets, High-level Petri Nets, Unfoldings, Concurrency Theory

††volume: 185††issue: 1

Taking Complete Finite Prefixes To High Level, Symbolically

## Introduction

Petri nets [2], also called P/T (for Place/Transition) Petri nets or low-level
Petri nets, are a well-established formalism for describing distributed
systems. _High-level Petri nets_ [3] (also called _colored Petri nets_) are a
concise representation of P/T Petri nets, allowing the places to carry tokens
of different colors. Every high-level Petri net represents a P/T Petri net,
here called its _expansion_ 111 The Petri net being represented is commonly
referred to as the _unfolding_ of the high-level Petri net in the literature.
To prevent any potential confusion, we opt for the term _expansion_ , as, for
instance, in [4]., where the process of constructing this P/T net is called
_expanding_ the high-level net.

_Unfoldings_ of P/T Petri nets are introduced by Nielsen et al. in [5].
Engelfriet generalizes this concept in [6] by introducing the notion of
_branching processes_ , and shows that the unfolding of a net is its maximal
branching process. In [7], McMillan gives an algorithm to compute a complete
finite prefix of the unfolding of a given Petri net. In a well-known paper
[8], Esparza, Römer, and Vogler improve this algorithm by defining and
exploiting a total order on the set of configurations in the unfolding. We
call the improved algorithm the “ERV-algorithm”. It leads to a comparably
small complete finite prefix of the unfolding. In [9], Khomenko and Koutny
describe how to construct the unfolding of the expansion of a high-level Petri
net without first expanding it.

High-level representations on the one hand and processes (resp. unfoldings) of
P/T Petri nets on the other, at first glance seem to be conflicting concepts;
one being a more concise, the other a more detailed description of the net(’s
behavior). However, in [10], Ehrig et al. define processes of high-level Petri
nets, and in [11], Chatain and Jard define _symbolic branching processes_ and
_unfoldings_ of high-level Petri nets. The work on the latter is built upon in
[4] by Chatain and Fabre, where they consider so-called “puzzle nets”. Based
on the construction of a symbolic unfolding, in [12], complete finite prefixes
of safe time Petri nets are constructed, using time constraints associated
with timed processes. In [13], using a simple example, Chatain argues that in
general there exists no complete finite prefix of the symbolic unfolding of a
high-level Petri net. However, this is only true for high-level Petri nets
with infinitely many reachable markings such that the number of steps needed
to reach them is unbounded, in which case the same arguments work for P/T
Petri nets.

In this paper, we lift the concepts of complete prefixes and adequate orders
to the level of symbolic unfoldings of high-level Petri nets. We consider the
class of _safe_ high-level Petri nets (i.e., in all reachable markings, every
place carries at most one token) that have decidable guards and finitely many
reachable markings. This class generalizes safe P/T Petri nets, and we obtain
a generalized version of the ERV-algorithm creating a complete finite prefix
of the symbolic unfolding of such a given high-level Petri net. Our results
are a generalization of [8] in the sense that if a P/T Petri net is viewed as
a high-level Petri net, the new definitions of adequate orders and
completeness of prefixes on the symbolic level, as well as the algorithm
producing them, all coincide with their P/T counterparts.

We proceed to identify an even more general class of so-called _symbolically
compact_ high-level Petri nets; we drop the assumption of finitely many
reachable markings, and instead assume the existence of a bound on the number
of steps needed to reach all reachable markings. In such a case, the expansion
is possibly not finite, and the original ERV-algorithm from [8] therefore not
applicable. We adapt the generalized ERV-algorithm by weakening the cut-off
criterion to ensure finiteness of the resulting prefix. Still, in this cut-off
criterion we have to compare infinite sets of markings. We overcome this
obstacle by symbolically representing these sets, using the decidability of
the guards to decide cut-offs. Finally, we present four new benchmark families
for which we report on the results of applying a prototype implementation of
the generalized ERV-algorithm.

### Distinctions from the Conference Version

This extended version incorporates numerous textual enhancements compared to
our original work in [1]. Apart from that, we made the following changes and
additions:

  * •

The proofs that were excluded in the conference version have now been
integrated into the main body of the paper.

  * •

We substituted the running example with a more intricate and compelling one,
and discuss it in greater detail. Additionally, we present an example for the
central concept “color conflict”.

  * •

Sec. 3 has been completely revised.

  * •

We introduced a new subsection, found in Sec. 4.2, where we demonstrate that
the generalized ERV-algorithm may not terminate when applied to input nets
from $\mathbf{N}_{\mathbf{SC}}$. This further motivates the work from the
conference version of finding a new cut-off criterion (Sec. 4.3). In another
new subsection, found in Sec. 4.4 we discuss the feasibility of symbolically
compact nets and provide an outlook into the potential development of a
symbolic reachability graph.

  * •

We changed the definition of $\mathit{pred}^{\odot}$ in Sec. 5 (formerly
Section 4.3). This allows for a better presentation of Theorem 5.4, and an
easier proof.

  * •

In a new section, found in Sec. 6, we report in Sec. 6.1 on a new prototype
implementation of the generalized ERV-algorithm from Sec. 2.2. In Sec. 6.2 we
present four new benchmark families of high-level Petri nets. In Sec. 6.3 we
discuss a property of high-level Petri nets which we call _mode determinism_ ,
leading to a heuristic for whether the symbolic unfolding is faster to
construct than the low-level unfolding. In Sec. 6.4, we present the results of
applying the implementation to the benchmarks from Sec. 6.2.

##  1 High-level Petri Nets & Symbolic Unfoldings

In [11], symbolic unfoldings for high-level Petri nets are introduced. We
recall the definitions and formalism for high-level Petri nets and symbolic
unfoldings.

_Multi-sets._ For a set $X$, we call a function $A:X\to\mathbb{N}$ a _multi-
set over_ $X$. We denote $x\in A$ if $A(x)\geq 1$. For two multi-sets
$A,A^{\prime}$ over the same set $X$, we write $A\leq A^{\prime}$ iff $\forall
x\in X:A(x)\leq A^{\prime}(x)$, and denote by $A+A^{\prime}$ and
$A-A^{\prime}$ the multi-sets over $X$ given by
$(A+A^{\prime})(x)=A(x)+A^{\prime}(x)$ and
$(A-A^{\prime})(x)=\max(A(x)-A^{\prime}(x),0)$. We use the notation
$\mathopen{{\\{}\;\\!\\!\\!{|}\,}\dots\mathclose{\,{|}\;\\!\\!\\!{\\}}}$ as
introduced in [9]: elements in a multi-set can be listed explicitly as in
$\mathopen{{\\{}\;\\!\\!\\!{|}\,}x_{1},x_{1},x_{2}\mathclose{\,{|}\;\\!\\!\\!{\\}}}$,
which describes the multi-set $A$ with $A(x_{1})=2$, $A(x_{2})=1$, and
$A(x)=0$ for all $x\in X\setminus\\{x_{1},x_{2}\\}$. A multi-set $A$ is finite
if there are finitely many $x\in X$ such that $x\in A$. In such a case,
$\mathopen{{\\{}\;\\!\\!\\!{|}\,}f(x)\,\mid\,x\in
A\mathclose{\,{|}\;\\!\\!\\!{\\}}}$, with $f(x)$ being an object constructed
from $x\in X$, denotes the multi-set $A^{\prime}$ such that
$A^{\prime}=\sum_{x\in X}A(x)\cdot f(x)$, where the $A(x)\cdot y$ is the
multi-set containing exactly $A(x)$ copies of $y$.

###  1.1 High-level Petri Nets

A _(high-level) net structure_ is a tuple
$\mathcal{N}=(\mathit{Col},\mathit{Var},P,T,F,\iota)$ with the following
components: $\mathit{Col}$ and $\mathit{Var}$ are the sets of _colors_ and
_variables_ , and $P$ and $T$ are sets of _places_ and _transitions_ such that
the four sets are pairwise disjoint. The _flow function_ is given by
$F:(P\times\mathit{Var}\times T)\cup(T\times\mathit{Var}\times
P)\to\mathbb{N}$. Let $\mathit{Var}(t)=\\{v\in\mathit{Var}\,\mid\,\exists p\in
P:(p,v,t)\in F\lor(t,v,p)\in F\\}$. The function $\iota$ maps each $t\in T$ to
a predicate $\iota(t)$ on $\mathit{Var}(t)$, called the _guard_ of $t$. By
this, $\iota(t)$ can contain other (bounded) variables, but all free variables
in $\iota(t)$ must appear on arcs to or from $t$. A _marking_ in $\mathcal{N}$
is a multi-set $M$ over $P\times\mathit{Col}$, describing how often each color
$c\in\mathit{Col}$ currently resides on each place $p\in P$. A _high-level
Petri net_ $N=(\mathcal{N},\mathcal{M}_{0})$ is a net structure $\mathcal{N}$
together with a nonempty set $\mathcal{M}_{0}$ of _initial markings_ , where
we assume $\forall
M_{0},M_{0}^{\prime}\in\mathcal{M}_{0}:\mathopen{{\\{}\;\\!\\!\\!{|}\,}p\,\mid\,(p,c)\in
M_{0}\mathclose{\,{|}\;\\!\\!\\!{\\}}}=\mathopen{{\\{}\;\\!\\!\\!{|}\,}p\,\mid\,(p,c)\in
M_{0}^{\prime}\mathclose{\,{|}\;\\!\\!\\!{\\}}}$, i.e., in all initial
markings, the same places are marked with _the same number of colors_. We
often assume the two sets $\mathit{Col}$ of colors and $\mathit{Var}$ of
variables to be given. In this case, we denote a high-level net structure
(resp. high-level Petri net) by $\mathcal{N}=(P,T,F,\iota)$ (resp.
$N=(P,T,F,\iota,\mathcal{M}_{0})$).

For two nodes $x,y\in P\cup T$, we write $x\rightarrow y$, if there exists a
variable $v$ such that $(x,v,y)\in F$. The reflexive and irreflexive
transitive closures of $\rightarrow$ are denoted respectively by $\leq$ and
$<$. For a transition $t\in T$, we denote by
$\mathit{pre}(t)=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(p,v)\,\mid\,(p,v,t)\in
F\mathclose{\,{|}\;\\!\\!\\!{\\}}}$ and
$\mathit{post}(t)=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(p,v)\,\mid\,(t,v,p)\in
F\mathclose{\,{|}\;\\!\\!\\!{\\}}}$ the _preset_ and _postset_ of $t$. A
_firing mode_ of $t$ is a mapping $\sigma:\mathit{Var}(t)\to\mathit{Col}$ such
that $\iota(t)$ evaluates to $\mathit{true}$ under the substitution given by
$\sigma$, denoted by $\iota(t)[\sigma]\equiv\mathit{true}$. We then denote
$\mathit{pre}(t,\sigma)=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(p,\sigma(v))\,\mid\,(p,v)\in\mathit{pre}(t)\mathclose{\,{|}\;\\!\\!\\!{\\}}}$
and
$\mathit{post}(t,\sigma)=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(p,\sigma(v))\,\mid\,(p,v)\in\mathit{post}(t)\mathclose{\,{|}\;\\!\\!\\!{\\}}}$.
The set of modes of $t$ is denoted by $\Sigma(t)$. Note that such a “binding”
of variables to colors is always only local, when firing the respective
transition. $t$ can _fire_ in such a mode $\sigma$ from a marking $M$ if
$M\geq\mathit{pre}(t,\sigma)$, denoted by $M[t,\sigma\rangle$. This firing
leads to a new marking
$M^{\prime}=(M-\mathit{pre}(t,\sigma))+\mathit{post}(t,\sigma)$, which is
denoted by $M[t,\sigma\rangle M^{\prime}$. We collect in the set
$\mathcal{R}(\mathcal{N},\mathcal{M})$ the markings reachable by firing a
sequence of transitions in $\mathcal{N}$ from any marking in a set of markings
$\mathcal{M}$. We say $\mathcal{N}$ resp. $N$ is _finite_ if $P$, $T$ and $F$
are finite. In this paper, we in particular aim to analyze the _behavior_ of
high-level Petri nets. To avoid any issues concerning undecidability regarding
the firing relation, we assume that guards are expressed in a decidable logic,
with $\mathit{Col}$ as its domain of discourse.

Let $\mathcal{N}=(P,T,F,\iota)$ and
$\mathcal{N}^{\prime}=(P^{\prime},T^{\prime},F^{\prime},\iota^{\prime})$ be
two net structures with the same sets of colors and variables. A function
$h:P\cup T\to P^{\prime}\cup T^{\prime}$ is called a _(high-level Petri net)
homomorphism_ , if:

  1. i)

it maps places and transitions in $\mathcal{N}$ into the corresponding sets in
$\mathcal{N}^{\prime}$, i.e.,
${h(P)\subseteq P^{\prime}}$ and $h(T)\subseteq T^{\prime}$;

  2. ii)

it is “compatible” with the guard, preset, and postset, of transitions, i.e.,
for all ${t\in T}$ we have $\iota(t)=\iota^{\prime}(h(t))$ and
$\mathit{pre}(h(t))=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(h(p),v)\,\mid\,(p,v)\in\mathit{pre}(t)\mathclose{\,{|}\;\\!\\!\\!{\\}}}$
and
$\mathit{post}(h(t))=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(h(p),v)\,\mid\,(p,v)\in\mathit{post}(t)\mathclose{\,{|}\;\\!\\!\\!{\\}}}$.

For $N=(\mathcal{N},\mathcal{M}_{0})$ and
$N^{\prime}=(\mathcal{N}^{\prime},\mathcal{M}_{0}^{\prime})$, the
homomorphisms between $N$ and $N^{\prime}$ are the homomorphisms between
$\mathcal{N}$ and $\mathcal{N}^{\prime}$. Such a homomorphism $h$ is called
_initial_ if additionally
$\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}(h(p),c)\,\mid\,(p,c)\in
M_{0}\mathclose{\,{|}\;\\!\\!\\!{\\}}}\,\mid\,M_{0}\in\mathcal{M}_{0}\\}=\mathcal{M}_{0}^{\prime}$
holds, i.e., the initial markings in $N$ are mapped to the initial markings in
$N^{\prime}$

We define _P/T Petri nets_ as high-level Petri nets with singletons
$\mathit{Col}=\\{\bullet\\}$ and $\mathit{Var}=\\{v_{\bullet}\\}$ for colors
and variables, i.e., in a marking, every place holds a number of tokens
$\bullet$, which is the only value ever assigned to the variable $v_{\bullet}$
on every arc. The guard of every transition in a P/T Petri net is
$\mathit{true}$.

###### Example 1.1

(a) A safe high-level Petri net.

(b) The symbolic unfolding of the net in 1(a)

Figure 1: A safe high-level Petri net $N$ in 1(a), and (a prefix of) the
infinite symbolic unfolding $U(N)$ in 1(b). We have
$\mathit{Col}=\\{0,\dots,m\\}$ and $\mathit{Var}=\\{x,y,z,w\\}$.

Let $\mathit{Col}=\\{0,\dots,m\\}$ for a fixed $m$, and
$\mathit{Var}=\\{x,y,z,w\\}$ be the given sets of colors and variables. In
Figure 1(a), the running example $N$ of a high-level Petri net is depicted.
Places are drawn as circles, and transitions as squares. The flow is described
by labeled arrows, and the guards are written next to the respective
transition. $N$ has just one initial marking
$M_{0}=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(a,0),(b,0)\mathclose{\,{|}\;\\!\\!\\!{\\}}}$,
which is depicted in the net. In all our examples we view $0$ as a “special”
color, in the sense that we employ unlabeled arcs as an abbreviation for arcs
labeled with an additional variable $x_{0}$, and the guard of the respective
transition having an additional term $x_{0}=0$ in its guard. Thus, we handle
$0$ as we would the token $\bullet$ in the P/T case. From $M_{0}$ the two
transitions $\alpha$ and $\beta$ can fire, taking the color $0$ from place $a$
resp. $b$ and placing a number $k\in\\{1,\dots,m\\}$ on place $c$ resp. $d$
when firing in mode $\\{x\leftarrow k\\}$. The mode $\\{x\leftarrow 0\\}$ is
for both transitions excluded by their respective guard. When both $\alpha$
and $\beta$ fired, the net arrived at a marking
$\mathopen{{\\{}\;\\!\\!\\!{|}\,}(c,k),(d,\ell)\mathclose{\,{|}\;\\!\\!\\!{\\}}}$.
From there, $\varepsilon$ can fire arbitrarily often, always replacing the
colors $k,\ell$ currently residing on $c,d$ by any colors
$0<k^{\prime},\ell^{\prime}\leq m$ by firing in mode $\\{x\leftarrow
k,y\leftarrow\ell,z\leftarrow k^{\prime},w\leftarrow\ell^{\prime}\\}$. From
every marking
$\mathopen{{\\{}\;\\!\\!\\!{|}\,}(c,k),(d,\ell)\mathclose{\,{|}\;\\!\\!\\!{\\}}}$
satisfying $\ell=3\cdot k$, transition $t$ can fire, ending the execution of
the net.

###  1.2 Symbolic Branching Processes and Unfoldings

A high-level net structure
$\mathcal{N}=(\mathit{Col},\mathit{Var},P,T,F,\iota)$ is called _ordinary_ if
there is at most one arc connecting any two nodes in $\mathcal{N}$, i.e.,
$\forall(x,y)\in(P\times T)\cup(T\times P):\sum_{v\in\mathit{Var}}F(x,v,y)\leq
1$. For such an ordinary net structure, analogously to the well-known low-
level case, two nodes $x,y\in P\cup T$ are in _structural conflict_ , denoted
by $x\sharp y$, if $\exists p\in P\,\exists t,t^{\prime}\in T:{t\neq
t^{\prime}}\land p\rightarrow t\land p\rightarrow t^{\prime}\land t\leq x\land
t^{\prime}\leq y$.

A _high-level occurrence net_ is a high-level Petri net
$O=(\mathit{Col},\mathit{Var},B,E,H,\iota,\mathcal{K}_{0})$ with an ordinary
net structure $(\mathit{Col},\mathit{Var},B,E,H,\iota)$, where $B$ is a set of
_conditions_ (places), $E$ is a set of _events_ (transitions), $H$ is a flow
relation, and $\mathcal{K}_{0}$ is the set of initial _cuts_ (reachable
markings), such that the four properties below are satisfied.

The properties i) – iii) are exactly the same as in the low-level case and
concern solely the net structure. Property iv) generalizes the corresponding
requirement of low-level occurrence nets to the current situation, in which,
just as in the low-level case, every condition has at most one event in its
preset, and that those conditions having an empty preset constitute the
initial cut. Case iv.a) describes the conditions that initially hold a color,
at the “top” of the net. Case iv.b) on the other hand describes the conditions
“deeper” in the net, which initially do not hold a color.

The properties that a high-level occurrence net must satisfy are:

  1. i)

No event is in structural self-conflict, i.e., $\forall e\in E:\neg(e\sharp
e)$.

  2. ii)

No node is its own causal predecessor, i.e., $\forall x\in B\cup
E:{\neg(x<x)}$.

  3. iii)

The flow relation is well-founded, i.e., $\forall x\in B\cup
E:|\\{y\,\mid\,y\leq x\\}|<\infty$.

  4. iv)

For every $b\in B$, exactly one of the following holds:

    1. a)

$\forall K_{0}\in\mathcal{K}_{0}:\sum_{c\in\mathit{Col}}K_{0}(b,c)=1$ and
$\\{e\,\mid\,e\rightarrow b\\}=\emptyset$.
In this case we denote $\mathit{pre}(b)=(\bot,v^{b})$.

    2. b)

$\forall K_{0}\in\mathcal{K}_{0}:\sum_{c\in\mathit{Col}}K_{0}(b,c)=0$ and
there exists a unique pair $(e,v)$ s.t. $(e,v,b)\in H$. In this case we denote
$\mathit{pre}(b)=(e,v)$

We denote by $B_{0}=\\{b\in B\,\mid\,\exists K_{0}\in\mathcal{K}_{0}\,\exists
c\in\mathit{Col}:(b,c)\in K_{0}\\}$ the conditions from iv.a) occupied in all
initial cuts. $\bot$ can be seen as a “special event” that fires only once to
initialize the net, and produces the initial cuts $K_{0}\in\mathcal{K}_{0}$ by
assigning values to the variables $v^{b}$ on “special arcs” $(\bot,v^{b},b)$
towards the conditions $b\in B_{0}$.

In a crucial notation for this paper, we define in case iv.a)
$\mathbf{e}(b)=\bot$, and $\mathbf{v}(b)=v^{b}$, and in case iv.b) we identify
the event $e$ by $\mathbf{e}(b)$ and the variable $v$ by $\mathbf{v}(b)$. By
this notation, $\forall b\in B:\mathit{pre}(b)=(\mathbf{e}(b),\mathbf{v}(b))$.
We can say that whenever a condition $b$ holds a color $c$, then it got placed
there by firing $\mathbf{e}(b)$ in a mode that binds $\mathbf{v}(b)$ to the
color $c$.

In a high-level occurrence net, we define for every event $e$ the predicates
$\mathit{loc\text{-}pred}(e)$ and $\mathit{pred}(e)$. The predicate
$\mathit{pred}(e)$ is satisfiable iff $e$ is not dead, i.e., there are cuts
$K_{0},\dots,K_{n}$ with $K_{0}\in\mathcal{K}_{0}$ and events
$e_{1},\dots,e_{n}$, s.t. $K_{0}[e_{1}\rangle\dots[e_{n}\rangle
K_{n}[e\rangle$. This predicate is obtained by building a conjunction over all
_local predicates_ of events $e^{\prime}$ with $e^{\prime}\leq e$, and the
predicate of the special event $\bot$.

The local predicate of $e$ is, in its turn, a conjunction of two predicates
expressing that (i) the guard of the event $e$ is satisfied, and (ii) that for
any $(b,v)\in\mathit{pre}(e)$, the value of the variable $v$ coincides with
the color that the event $\mathbf{e}(b)$ placed in $b$. To realize this, the
variables $v\in\mathit{Var}(e)$ are instantiated by the index $e$, so that
$v_{e}$ describes the value assigned to $v$ by a mode of $e$. Having the
definition of $\mathbf{e}(b)$ and $\mathbf{v}(b)$ from above in mind, for a
condition $b$, we abbreviate
$\mathbf{v}_{\mathbf{e}}(b)=\mathbf{v}(b)_{\mathbf{e}(b)}$. Formally, we have

$\displaystyle\mathit{loc\text{-}pred}(e)\quad$
$\displaystyle=\quad\iota(e)[v\leftarrow
v_{e}]_{v\in\mathit{Var}(e)}\quad\land\quad\bigwedge_{(b,v)\in\mathit{pre}(e)}v_{e}=\mathbf{v}_{\mathbf{e}}(b)$
$\displaystyle\mathit{pred}(e)\quad$
$\displaystyle=\quad\mathit{pred}(\bot)\land\bigwedge_{e^{\prime}\leq
e}\mathit{loc\text{-}pred}(e^{\prime}),$

where
$\mathit{pred}(\bot)=\bigvee_{K_{0}\in\mathcal{K}_{0}}\bigwedge_{(b,c)\in
K_{0}}(v_{\bot}^{b}=c)$ symbolically represents the set of initial cuts.

A _symbolic branching process_ of a high-level Petri net $N$ is a pair
$\beta=(O,h)$ with an occurrence net
$O=(\mathit{Col},\mathit{Var},B,E,H,\iota,\mathcal{K}_{0})$ in which
$\mathit{pred}(e)$ is satisfiable for all $e\in E$, and an initial
homomorphism $h:O\to N$ that is injective on events with the same preset,
i.e., $\forall e,e^{\prime}\in
E:(\mathit{pre}(e)=\mathit{pre}(e^{\prime})\land
h(e)=h(e^{\prime}))\Rightarrow e=e^{\prime}$.

For two symbolic branching processes $\beta=(O,h)$ and
$\beta^{\prime}=(O^{\prime},h^{\prime})$ of a high-level Petri net, $\beta$ is
a _prefix_ of $\beta^{\prime}$ if there exists an injective initial
homomorphism $\phi$ from $O$ into $O^{\prime}$, such that
$h^{\prime}\circ\phi=h$. In [11] it is stated that for any given high-level
Petri net $N$ there exists a unique maximal branching process (maximal w.r.t.
the prefix relation and unique up to isomorphism). This branching process is
called the _symbolic unfolding_ , and denoted by
$\varUpsilon(N)=(U(N),\pi^{N})$. The value of $\pi^{N}(x)$ is called the
_label_ of a node $x$ in $U(N)$.

###### Example 1.2

Consider again the high-level Petri net $N$ from Figure 1(a). In Figure 1(b)
we see (a prefix of) the infinite occurrence net $U(N)$ of the symbolic
unfolding $\varUpsilon(N)$. We depict the prefix with two instances of each
$t$ and $\varepsilon$. Each node in the unfolding is named after the
represented place resp. transition (i.e., its label), equipped with a
superscript. We include the “special event” $\bot$, that can only fire once,
in the drawing. The guards of events are omitted, since they have the same
guards as their label. Instead, the local predicate of each event is written
next to it.

The local predicate of $\alpha^{\prime}$, namely $x_{\alpha^{\prime}}>0$
expresses that the assignment of colors to variables by a mode of
$\alpha^{\prime}$ must satisfy the constraint given by the guard of its label
$\alpha$. Analogously for $\beta^{\prime}$. The same is expressed in the local
predicate of $t^{\prime}$ by $y_{t^{\prime}}=3\cdot x_{t^{\prime}}$, coming
from the guard $y=3\cdot x$ of $t$. Additionally, the first part of the
conjunction formalizes that, since
$(c^{\prime},x)\in\mathit{pre}(t^{\prime})$, the value that a mode of
$t^{\prime}$ assigns to $x$ must be the same that a mode of
$\mathbf{e}(c^{\prime})=\alpha^{\prime}$ assigned to
$\mathbf{v}(c^{\prime})=x$. This is expressed as
$x_{t^{\prime}}=x_{\alpha^{\prime}}$. The second part of the conjunction
formalizes the same for $y$ and $d^{\prime}$. The whole predicate of
$t^{\prime}$ is then given by

$\mathit{pred}(t^{\prime})=x_{\alpha^{\prime}}>0\land
x_{\beta^{\prime}}>0\land x_{t^{\prime}}=x_{\alpha^{\prime}}\land
y_{t^{\prime}}=x_{\beta^{\prime}}\land y_{t^{\prime}}=3\cdot x_{t^{\prime}}.$

Since it is satisfiable for example by $\\{x_{\alpha^{\prime}}\leftarrow
1,x_{\beta^{\prime}}\leftarrow 3,x_{t^{\prime}}\leftarrow
1,y_{t^{\prime}}\leftarrow 3\\}$ (meaning that $t$ can fire in mode
$\\{x\leftarrow 1,y\leftarrow 3\\}$ after $\alpha$ fired in mode
$\\{x\leftarrow 1\\}$ and $\beta$ fired in mode $\\{x\leftarrow 3\\}$), the
node $t^{\prime}$ is an event in the unfolding.

The blue shading of event $\varepsilon^{\prime\prime}$ and $t^{\prime\prime}$
indicates that they are what we later term _cut-off events_ , which leads to
the _complete finite prefix_ being marked by the blue thick lines being
obtained by Alg. 1, as described later. The unfolding itself is infinite.

As we see in the definition of high-level occurrence nets, the notion of
causality and structural conflict are the same as in the low-level case.
However, a set of events in an occurrence net can also be in what we call
_color conflict_ , meaning that the conjunction of their predicates is not
satisfiable. In a symbolic branching process, this means that the constraints
on the values of the firing modes, coming from the guards of the transitions,
prevent joint occurrence of all events from such a set in any _one_ run of the
net:

The nodes in a set $X\subseteq E\cup B$ and are in _color conflict_ if

$\bigwedge_{e\in X\cap E}\mathit{pred}(e)\land\bigwedge_{b\in X\cap
B}\mathit{pred}(\mathbf{e}(b))$

is _not_ satisfiable. The nodes of $X$ are _concurrent_ if they are _not_ in
color conflict, and for each $x,x^{\prime}\in X^{\prime}$, neither
$x<x^{\prime}$ , nor $x^{\prime}<x$, nor $x\sharp x^{\prime}$ holds. A set of
concurrent conditions is called a _co-set_.

Note that while a set of nodes is defined to be in structural conflict if and
only if two nodes in it are in structural conflict, the same does not hold for
color conflict: it is possible to have a set $\\{x_{1},x_{2},x_{3}\\}$ of
nodes that are in color conflict, but for which every subset of cardinality 2
is _not_ in color conflict. We demonstrate this on an example.

######  Example 1.3 (Color conflict)

(a) A high-level Petri net with $\mathit{Col}=\mathbb{Z}$ and
$\mathit{Var}=\\{x\\}$.

(b) The symbolic unfolding of the net in 2(a), with the events
$\\{e_{1},e_{2},e_{3}\\}$ in color conflict.

Figure 2: Illustration and example of nodes in color conflict.

In Figure 2(a), a high-level Petri net with initial marking
$\mathopen{{\\{}\;\\!\\!\\!{|}\,}(p_{0},0)\mathclose{\,{|}\;\\!\\!\\!{\\}}}$
is depicted. The only enabled transition is $t_{0}$, placing the same color
$\sigma(x)\in\mathbb{Z}=\\{\dots,-1,0,1,2,\dots\\}$ on each of the three
places $p_{1},p_{2},p_{3}$ when fired in mode
$\sigma=\\{x\leftarrow\sigma(x)\\}$. From each of these places, the color
$\sigma(x)$ may be taken by a respective transition; The three transitions
$t_{1},t_{2},t_{3}$, however, each have a guard: $\iota(t_{1})=(x\leq 0)$,
$\iota(t_{2})=(x\neq 0)$, and $\iota(t_{3})=(x\geq 0)$. Depending on the mode
$\sigma$ in which $t_{0}$ fired, always two of the three transitions are
fireable: if $\sigma(x)=0$ then $t_{1}$ and $t_{3}$ can both fire (in mode
$\\{x\leftarrow 0\\}$), if $\sigma(x)<0$ then $t_{1}$ and $t_{2}$ can fire,
and if $\sigma(x)>0$ then $t_{2}$ and $t_{3}$ can fire.

Since the high-level Petri net in Figure 2(a) is a high-level occurrence net
and all predicates are satisfiable, it is structurally equivalent to its own
symbolic unfolding in Figure 2(b). The set $\\{b_{1},b_{2},b_{3}\\}$ is a co-
set, since the conditions are neither in conflict, nor causally related, and
$\bigwedge_{b\in\\{b_{1},b_{2},b_{3}\\}}\mathit{pred}(\mathbf{e}(b))$, which
is equivalent to $\mathit{true}$, is satisfiable, i.e., the conditions are
_not_ in color conflict. Consequently, the set $\\{e_{1},e_{2},e_{3}\\}$ is
also not in structural conflict, and the events are not causally related.
However, there now _is_ a color conflict between these three events, since
$\bigwedge_{e\in\\{e_{1},e_{2},e_{3}\\}}\mathit{pred}(e)$ implies
$x_{e_{0}}\leq 0\land x_{e_{0}}\neq 0\land x_{e_{0}}\geq 0$, which obviously
is not satisfiable. In contrast, each of the sets $\\{e_{i},e_{j}\\}$ with
$i,j\in\\{1,2,3\\}$, $i\neq j$ is _not_ in color conflict. This makes each of
the sets $\\{b_{i}^{\prime},b_{j}^{\prime}\\}$ a co-set, while
$\\{b_{1}^{\prime},b_{2}^{\prime},b_{3}^{\prime}\\}$ is not a co-set.

Having employed the notions of conflict, we come to one of the most important
definitions when dealing with unfoldings, namely _configurations_.

######  Definition 1.4 (Configuration [11])

A _(symbolic) configuration_ is a set of high-level events that is free of
structural conflict and color conflict, and causally closed. The
configurations in a symbolic branching process $\beta$ are collected in the
set $\mathcal{C}(\beta)$.

For a configuration $C$, we define by
$\operatorname{cut}(C):=(B_{0}\cup(C\rightarrow))\setminus(\rightarrow C)$ the
high-level conditions that are occupied after any concurrent execution of $C$.
Note that $\operatorname{cut}(C)$ is a co-set, and that $\emptyset$ is a
configuration with $\operatorname{cut}(\emptyset)=B_{0}$.

Let $e\in E$ be a high-level event. We define the so-called _cone
configuration_ $[e]:=\\{e^{\prime}\in E\,\mid\,e^{\prime}\leq e\\}$.
Additionally, we define the sets
$\mathit{Var}_{e}:=\\{v_{e}\,\mid\,v\in\mathit{Var}(e)\\}$ and
$\mathit{Var}_{\bot}:=\\{v_{\bot}^{b}\,\mid\,b\in B_{0}\\}$ of indexed
variables, and for a set $E^{\prime}\subseteq E\cup\\{\bot\\}$ we denote
$\mathit{Var}_{E^{\prime}}:=\bigcup_{e\in E^{\prime}}\mathit{Var}_{e}$. Note
that, for every event $e$, $\mathit{pred}(e)$ is a predicate over the
variables $\mathit{Var}_{[e]\cup\\{\bot\\}}$.

###  1.3 Properties of the Symbolic Unfolding.

Having recalled the definitions and formal language from [11], we now delve
into the novel aspects of this paper. We state three analogues of well-known
properties of the Unfolding of P/T Petri nets for the symbolic unfolding of
high-level nets. These properties are:

  1. (i)

The cuts in the unfolding represent precisely the reachable markings in the
net.

  2. (ii)

For every transition that can occur in the net, there is an event in the
unfolding with corresponding label (and vice versa).

  3. (iii)

The unfolding is complete in the sense that for any configuration, the part of
the unfolding that “lies after” that configuration is the unfolding of the
original net with the initial markings being the ones represented by the
configurations cut.

The properties are stated in Prop. 1.6, Prop. 1.8, and Prop. 1.10,
respectively.

To express these properties, we introduce the notion of _instantiations_ of
configurations $C$, choosing a mode for every event in $C$ without creating
color conflicts. This is realized by assigning to each variable
$v_{e}\in\mathit{Var}_{C\cup\\{\bot\\}}$ a value in $\mathit{Col}$, such that
the above defined predicates evaluate to $\mathit{true}$. For each $e\in C$,
the assignment of values to the indexed variables in $\mathit{Var}_{e}$
corresponds to a mode of $e$.

######  Definition 1.5 (Instantiation of Configuration)

For a given configuration $C$, an _instantiation of $C$_ is a function
$\theta:\mathit{Var}_{C\cup\\{\bot\\}}\to\mathit{Col}$, such that $\forall
e\in C\cup\\{\bot\\}:\mathit{pred}({e})[\theta]\equiv\mathit{true}$, i.e., it
satisfies all predicates in the configuration. The set of instantiations of a
given configurations $C$ is denoted by $\Theta(C)$.

Note that, by definition, every configuration $C$ has an instantiation
$\theta$. We denote by
$\operatorname{cut}(C,\theta):=\\{(b,c)\,\mid\,b\in\operatorname{cut}(C)\land\theta(\mathbf{v}_{\mathbf{e}}(b))=c\\}\subseteq
B\times\mathit{Col}$ the _cut_ of an “instantiated configuration”, and by
$\operatorname{mark}(C,\theta):=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(h(b),c)\,\mid\,(b,c)\in\operatorname{cut}(C,\theta)\mathclose{\,{|}\;\\!\\!\\!{\\}}}$
its _marking_. We collect both of these in
$\mathcal{K}(C):=\\{\operatorname{cut}(C,\theta)\,\mid\,\theta\in\Theta(C)\\}$
and
$\mathcal{M}(C):=\\{\operatorname{mark}(C,\theta)\,\mid\,\theta\in\Theta(C)\\}$.
Note that in this notation, for the empty configuration we have
$\mathcal{K}(\emptyset)=\mathcal{K}_{0}$ and
$\mathcal{M}(\emptyset)=\mathcal{M}_{0}$.

###### Proposition 1.6

Let $N$ be a high-level Petri net and $\varUpsilon$ its symbolic unfolding.
Then
$\mathcal{R}(N)=\\{\operatorname{mark}(C,\theta)\,\mid\,C\in\mathcal{C}(\varUpsilon),\theta\in\Theta(C)\\}$.

###### Proof 1.7

The proof is an easy induction over the number $n$ of transitions/events
needed to reach a respective marking/cut. The induction anchor $n=0$ is proved
by using that $\pi$ is an initial homomorphism which gives
$\mathcal{M}_{0}=\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}(\pi(b),c)\,\mid\,(b,c)\in
K_{0}\mathclose{\,{|}\;\\!\\!\\!{\\}}}\,\mid\,K_{0}\in\mathcal{K}_{0}\\}=\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}(\pi(b),c)\,\mid\,(b,c)\in
K\mathclose{\,{|}\;\\!\\!\\!{\\}}}\,\mid\,K\in\mathcal{K}(\emptyset)\\}=\\{\operatorname{mark}(\emptyset.\theta)\,\mid\,\theta\in\Theta(\emptyset)\\}$.
The induction step is realized by Prop. 1.8.

###### Proposition 1.8

The symbolic unfolding $\varUpsilon=(U,\pi)$ with events $E$ of a high-level
Petri net $N=(P,T,F,\iota,\mathcal{M}_{0})$ satisfies $\forall
C\in\mathcal{C}(\varUpsilon)\;\forall\theta\in\Theta(C)\;\forall t\in
T\;\forall\sigma\in\Sigma(t):$

$\operatorname{mark}(C,\theta)[t,\sigma\rangle\ \Leftrightarrow\ \exists e\in
E:\pi(e)=t\land\operatorname{cut}(C,\theta)[e,\sigma\rangle.$

###### Proof 1.9

Let
$U=(B,E,H,\iota,\mathcal{K}_{0}),C\in\mathcal{C}(\varUpsilon),\theta\in\Theta(C),t\in
T,{\sigma\in\Sigma(t)}$.

Let $\operatorname{mark}(C,\theta)[t,\sigma\rangle$, which means

$\mathit{pre}(t,\sigma)\leq\operatorname{mark}(C,\theta)=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(\pi(b),\theta(\mathbf{v}_{\mathbf{e}}(b)))\,\mid\,(b,\theta(\mathbf{v}_{\mathbf{e}}(b)))\in\operatorname{cut}(C,\theta)\mathclose{\,{|}\;\\!\\!\\!{\\}}},$

leading to

$\mathopen{{\\{}\;\\!\\!\\!{|}\,}(\pi(b),v)\,\mid\,(p,v)\in\mathit{pre}(t),\pi(b)=p,(b,\theta(\mathbf{v}_{\mathbf{e}}(b)))\in\operatorname{cut}(C,\theta)\mathclose{\,{|}\;\\!\\!\\!{\\}}}=\mathit{pre}(t).$

Aiming a contradiction, assume $\nexists e\in
E:\pi(e)=t\land\operatorname{cut}(C,\theta)[e,\sigma\rangle.$ We now extend
$\varUpsilon$ by such an event. We add to $E$ an event $\widetilde{e}$ with
$\pi(\widetilde{e})=t$ and $\iota(\widetilde{e})=\iota(t)$. We define
$\mathit{pre}(\widetilde{e})=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(b,v)\,\mid\,(p,v)\in\mathit{pre}(t),\pi(b)=p,(b,\theta(\mathbf{v}_{\mathbf{e}}(b)))\in\operatorname{cut}(C,\theta)\mathclose{\,{|}\;\\!\\!\\!{\\}}}$.
Then we have
$\mathit{pre}(\pi(\widetilde{e}))=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(\pi(b),v)\,\mid\,(b,v)\in\mathit{pre}(\widetilde{e})\mathclose{\,{|}\;\\!\\!\\!{\\}}}$.
For every $(p,v)\in\mathit{post}(t)$, we then add $\mathit{post}(t)(p,v)$
conditions $b$ with $\pi(b)=p$ to $B$ and add $(\widetilde{e},v,b)$ to $H$. We
thus get
$\mathit{post}(\pi(\widetilde{e}))=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(\pi(b),v)\,\mid\,(b,v)\in\mathit{post}(\widetilde{e})\mathclose{\,{|}\;\\!\\!\\!{\\}}}$.
We now created a symbolic branching process bigger than $\varUpsilon$,
contradicting that $\varUpsilon$ is the symbolic unfolding.

Assume on the other hand $\exists e\in
E:\pi(e)=t\land\operatorname{cut}(C,\theta)[e,\sigma\rangle.$ Then
$\mathit{pre}(e,\sigma)\leq\operatorname{cut}(C,\theta)$, and therefore,
$\mathit{pre}(t)=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(\pi(b),v)\,\mid\,(b,v)\in\mathit{pre}(e)\mathclose{\,{|}\;\\!\\!\\!{\\}}}\leq\mathopen{{\\{}\;\\!\\!\\!{|}\,}(\pi(b),v)\,\mid\,(b,v)\in\operatorname{cut}(C,\theta)\mathclose{\,{|}\;\\!\\!\\!{\\}}}=\operatorname{mark}(C,\theta)$,
meaning $\operatorname{mark}(C,\theta)[t,\sigma\rangle$.

Given a configuration $C$ of a symbolic branching process $\beta=(O,h)$, we
define ${\Uparrow}C$ as the pair $(O^{\prime},h^{\prime})$, where $O^{\prime}$
is the unique subnet of $O$ whose set of nodes is $\\{x\in B\cup
E\,\mid\,x\notin(C\cup\rightarrow C)\land\forall y\in C:\lnot(y\sharp
x)\land(C\cup\\{x\\}\text{ is not in color conflict})\\}$ with the set
$\mathcal{K}(C)$ of initial cuts, and $h^{\prime}$ is the restriction of $h$
to the nodes of $O^{\prime}$. The branching process ${\Uparrow}C$ is referred
to as the _future_ of $C$.

###### Proposition 1.10

If $\beta$ is a symbolic branching process of $(\mathcal{N},\mathcal{M}_{0})$
and $C$ is a configuration of $\beta$, then ${\Uparrow}C$ is a branching
process of $(\mathcal{N},\mathcal{M}(C))$. Moreover, if $\beta$ is the
unfolding of $(\mathcal{N},\mathcal{M}_{0})$, then ${\Uparrow}C$ is the
unfolding of $(\mathcal{N},\mathcal{M}(C))$.

###### Proof 1.11

Let ${\Uparrow}C=(O^{\prime},h^{\prime})$ with
$O^{\prime}=(B^{\prime},E^{\prime},F^{\prime},\iota^{\prime},\mathcal{K}(C))$.
To show that $O^{\prime}$ is an occurrence net, we have to show i – iv from
the definition on page 1.2. i – iii are purely structural properties and
follow from the fact that $O$ is an occurrence net. iv is satisfied since
$\forall b\in\operatorname{cut}(C)\;\forall
K\in\mathcal{K}(C):\sum_{c\in\mathit{Col}}K(b,c)=1$ and $\forall b\in
B^{\prime}\setminus\operatorname{cut}(C)\;\forall
K\in\mathcal{K}(C):\sum_{c\in\mathit{Col}}K(b,c)=0$. $h^{\prime}$ is a
homomorphism that is injective on events with the same preset since $h$ is,
and that $h^{\prime}$ is initial follows by Prop. 1.6 and Prop. 1.8.

When $\beta$ is the symbolic unfolding of $(\mathcal{N},\mathcal{M}_{0})$,
then the maximality of ${{\Uparrow}C}$ follows from the maximality of $\beta$,
making ${{\Uparrow}C}$ the symbolic unfolding of
$(\mathcal{N},\mathcal{M}(C))$.

##  2 Finite & Complete Prefixes of Symbolic Unfoldings

We combine ideas from [8] (computing small finite and complete prefixes of
unfoldings) with results from [11] (symbolic unfoldings of high-level Petri
nets) to define and construct complete finite prefixes of symbolic unfoldings
of high-level Petri nets. We generalize the concepts and the ERV-algorithm
from [8] for safe P/T Petri nets to a class of safe high-level Petri nets, and
compare this generalization to the original. We will see that for P/T nets
interpreted as high-level nets, all generalized concepts (i.e., complete
prefixes, adequate orders, cut-off events), and, as a consequence, the result
of the generalized ERV-algorithm, all coincide with their P/T counterparts.

We start by lifting the definition of completeness to the level of symbolic
unfoldings. Together with Prop. 1.6 and Prop. 1.8, this can be seen as a
direct translation from the low-level case described, e.g., in [8].

######  Definition 2.1 (Complete prefix)

Let $\beta=(O,h)$ be a prefix of the symbolic unfolding of a high-level Petri
net $N$, with events $E^{\prime}$. Then $\beta$ is called _complete_ if for
every reachable marking $M$ in $N$ there exists $C\in\mathcal{C}(\beta)$ and
$\theta\in\Theta(C)$ s.t.

  1. i)

$M=\operatorname{mark}(C,\theta)$, and

  2. ii)

$\forall t\in T\,\forall\sigma\in\Sigma(t):\ M[t,\sigma\rangle\ \Rightarrow\
\exists e\in E^{\prime}:h(e)=t\ \land\
\operatorname{cut}(C,\theta)[e,\sigma\rangle.$

We now define the class $\mathbf{N}_{\mathbf{F}}$ of high-level Petri nets for
which we generalize the construction of finite and complete prefixes of the
unfolding of _safe_ P/T Petri nets from [8]. We discuss the properties
defining this class, and describe how it generalizes safe P/T nets.

######  Definition 2.2 (Class $\mathbf{N}_{\mathbf{F}}$)

The class $\mathbf{N}_{\mathbf{F}}$ contains all finite high-level Petri nets
$N=(P,T,F,\iota,\mathcal{M}_{0})$ satisfying the following three properties:

  1. (1)

The net is _safe_ , i.e., in every reachable marking there lies at most $1$
color on every place (formally; $\forall M\in\mathcal{R}(N)\,\forall p\in
P:\sum_{c\in\mathit{Col}}M(p,c)\leq 1$).

  2. (2)

Guards are written in a decidable first-order theory with the set
$\mathit{Col}$ as its domain of discourse.

  3. (3)

The net has finitely many reachable markings (formally;
$|\mathcal{R}(N)|<\infty$).

We require the safety property (1) for two reasons; on the one hand, to avoid
adding to the already heavy notation. On the other hand, while we think that a
generalization to bounded high-level Petri nets is possible, it comes with all
the troubles known from going from safe to $k$-bounded in the P/T case in [8],
plus the problems arising from the expressive power of the high-level
formalism. We therefore postpone this generalization to future work. Note
that, under the safety condition, we can w.l.o.g. assume $\mathcal{N}$ to be
ordinary (i.e., $\forall x,y\in P\cup T:\sum_{v\in\mathit{Var}}F(x,v,y)\leq
1$), since transitions violating this property could never fire. The
finiteness of $\mathcal{N}$ implies that we can assume $\mathit{Var}$ to be
finite.

While property (2) seems very strong, the goal is an algorithm that generates
a complete finite prefix of the symbolic unfolding of a given high-level Petri
net. The definition of symbolic branching processes requires the predicate of
every event added to the prefix to be satisfiable, and the predicates are
build from the guards in the given net. Thus, satisfiability checks in the
generation of the prefix seem for now inevitable. An example for such a theory
is Presburger arithmetic [14], which is a first order theory of the natural
numbers with addition. The guards in the example from Figure 1(a) are
expressible in Presburger arithmetic.

We need Property (3) to ensure that the generalized version of the cut-off
criterion from [8] yields a finite prefix constructed in the generalized ERV-
Algorithm. $|\mathcal{R}(N)|<\infty$ can be ensured by having a finite set
$\mathit{Col}$ of colors. In Sec. 4, we identify a class of high-level Petri
nets with infinitely many reachable markings for which the algorithm works
with an adapted cut-off criterion.

Under these three assumptions we generalize the finite safe P/T Petri nets
considered in [8]: every such P/T net can be seen as a high-level Petri net
with $\mathit{Col}=\\{\bullet\\}$ and all guards being $\mathit{true}$, and
thus satisfying the three properties above. Replacing the safety property (1)
by a respective “$k$-bounded property” would result in a generalization of
$k$-bounded P/T nets. In Sec. 3, we compare the result of the generalized ERV-
algorithm Alg. 1 applied to a high-level net to the result of the original
ERV-algorithm from [8] applied to the nets expansion.

For the rest of the section let
$N=(P,T,F,\iota,\mathcal{M}_{0})\in\mathbf{N}_{\mathbf{F}}$ with symbolic
unfolding $\varUpsilon=(U,\pi)=(B,E,H,\iota,\mathcal{K}_{0},\pi)$.

###  2.1 Generalizing Adequate Orders and Cut-Off Events

We lift the concept of adequate orders on the configurations of an occurrence
net to the level of symbolic unfoldings. A main property of adequate orders is
the preservation by finite _extensions_ , which are defined as for P/T-nets
(cp. [8]):

Given a configuration $C$, we denote by $C{\oplus}D$ the fact that $C\cup D$
is a configuration such that $C\cap D=\emptyset$. We say that $C{\oplus}D$ is
an _extension_ of $C$, and that $D$ is a _suffix_ of $C$. Obviously, for a
configuration $C^{\prime}$, if $C\subsetneq C^{\prime}$ then there is a
nonempty suffix $D$ of $C$ such that $C{\oplus}D=C^{\prime}$. For a
configuration $C{\oplus}D$, denote by
$O(C|D)=(\operatorname{cut}(C)\cup{{\rightarrow}D}\cup{D{\rightarrow}},D,H^{\prime},\mathcal{K}(C))$
the occurrence net “around $D$” from $\operatorname{cut}(C)$, where
$H^{\prime}$ is the restriction of $H$ to the nodes of $O(C|D)$. Note that for
every finite configuration $C$ with an extension $C{\oplus}D$, we have that
$D$ is a configuration of ${\Uparrow}C$.

We abbreviate for a marking $M$ the fact
$\exists\theta\in\Theta(C{\oplus}D):\operatorname{mark}(C,\theta|_{\mathit{Var}_{C\cup\\{\bot\\}}})=M$
by $C\llbracket M\rrbracket D$ to improve readability. Thus, $C\llbracket
M\rrbracket D$ means that the transitions corresponding to the events in $D$
can fire from $M\in\mathcal{M}(C)$.

Since we consider safe high-level Petri nets, we can relate two cuts
representing the same set of places in the following way:

###### Definition 2.3

Let $C_{1},C_{2}\in\mathcal{C}(\varUpsilon)$ with
$\pi(\operatorname{cut}(C_{1}))=\pi(\operatorname{cut}(C_{2}))$. Then there is
a unique bijection
$\phi:\operatorname{cut}(C_{1})\to\operatorname{cut}(C_{2})$ preserving $\pi$.
We call this mapping $\phi_{C_{1}}^{C_{2}}$.

The now stated Prop. 2.4 is a weak version of the arguments in [8], where the
Esparza et al. follow from the low-level version of Prop. 1.10 that if the
cuts of two low-level configurations represent the same marking in the low-
level net, then their futures are isomorphic, and the respective (unique)
isomorphism maps the suffixes of one configuration to the suffixes of the
other.

###### Proposition 2.4

Let $C_{1}$ and $C_{2}$ be two finite configurations in $\varUpsilon$, and let
$D$ be a suffix of $C_{1}$. If there is a marking
$M\in\mathcal{M}(C_{1})\cap\mathcal{M}(C_{2})$ s.t. $C_{1}\llbracket
M\rrbracket D$, then there is a unique monomorphism
$\varphi_{1,D}^{2}:O(C_{1}|D)\to{\Uparrow}C_{2}$ that satisfies
$\varphi_{1,D}^{2}(\operatorname{cut}(C_{1}))=\operatorname{cut}(C_{2})$ and
preserves the labeling $\pi$.
For this monomorphism we have that $\varphi_{1,D}^{2}(D)$ is a suffix of
$C_{2}$.

Notation. For functions $f:X\to Y$ and $f^{\prime}:X^{\prime}\to Y$ with
$X\cap X^{\prime}=\emptyset$ we define $f\uplus f^{\prime}:X\cup X^{\prime}\to
Y$ by mapping $x$ to $f(x)$ if $x\in X$ and to $f^{\prime}(x)$ if $x\in
X^{\prime}$.

###### Proof 2.5

By induction over the size $k=|D|$ of the suffix $D$.

_Base case $k=0$_. This means $D=\emptyset$. Then
$O(C_{1}|D)=(\operatorname{cut}(C_{1}),\emptyset,\emptyset,\mathcal{K}(C_{1}))$.
Since $M\in\mathcal{M}(C_{1})\cap\mathcal{M}(C_{2})$, we know that
$\pi(\operatorname{cut}(C_{1}))=\pi(\operatorname{cut}(C_{2}))$. Since we only
consider safe nets, $\varphi_{1,D}^{2}$ is uniquely realized by
$\phi_{C_{1}}^{C_{2}}:\operatorname{cut}(C_{1})\to\operatorname{cut}(C_{2})$
from Def. 2.3.

_Induction step. Let $k>0$._ Let $\theta\in\Theta(C_{1}{\oplus}D)$ s.t.
$\operatorname{mark}(C_{1},\theta|_{\mathit{Var}_{C_{1}\cup\\{\bot\\}}})=M$.
Let $e\in\mathit{Min}(D)$. Then for
$\sigma=[v\leftarrow\theta(v_{e})]_{v\in\mathit{Var}(e)}$ we have
$M[\pi(e),\sigma\rangle$. Thus, by Prop. 1.8, $\exists e^{\prime}\in
E:\pi(e^{\prime})=\pi(e)\land
C_{2}{\oplus}\\{e^{\prime}\\}\in\mathcal{C}(\varUpsilon)$. This means
${\rightarrow}e^{\prime}\subseteq(B_{0}\cup(C_{2}{\rightarrow}))\setminus({\rightarrow}C_{2})$;
else, $C_{2}{\oplus}\\{e^{\prime}\\}$ would not be a configuration. Thus,
$e^{\prime}$ is an event in ${\Uparrow}C_{2}$. Since $\pi(e)=\pi(e^{\prime})$,
we get by definition of homomorphisms that
$\\{(\pi(b),v)\,\mid\,(b,v)\in\mathit{post}(e)\\}=\\{(\pi(b),v)\,\mid\,(b,v)\in\mathit{post}(e^{\prime})\\}$.
The net $N$ is safe, therefore we can define the bijection
$\phi_{1}:(e{\rightarrow})\to(e^{\prime}{\rightarrow})$ by
$\phi_{1}(b)=b^{\prime}\Leftrightarrow\pi(b)=\pi(b^{\prime})$. We now define
$\varphi_{1}:O(C_{1}|\\{e\\})\to{{\Uparrow}C_{2}}$ by
$\varphi_{1}=\phi_{C_{1}}^{C_{2}}\uplus\\{e\mapsto
e^{\prime}\\}\uplus\phi_{1}$, which is a homomorphism satisfying the claimed
conditions.

Let now $C_{1}^{\prime}=C_{1}\cup\\{e\\}$,
$C_{2}^{\prime}=C_{2}\cup\\{\varphi_{1}(e)\\}$ and
$D^{\prime}=D\setminus\\{e\\}$. We then have for $M^{\prime}$ given by
$M[\pi(e),\sigma\rangle M^{\prime}$ that $C_{1}^{\prime}\llbracket
M^{\prime}\rrbracket D^{\prime}$,
$M^{\prime}\in\mathcal{M}(C_{1}^{\prime})\cap\mathcal{M}(C_{2}^{\prime})$, and
$|D^{\prime}|<k$. Thus, by the induction hypothesis, we get that there is a
unique monomorphism
$\varphi_{2}:O(C_{1}^{\prime}|D^{\prime})\to{\Uparrow}C_{2}^{\prime}$
satisfying the conditions above. Since $\varphi_{1}$ and $\varphi_{2}$
coincide on $\operatorname{cut}(C_{1}^{\prime})$, we can now define
$\varphi_{1,D}^{2}$ by “gluing together” $\varphi_{1}$ and $\varphi_{2}$ at
$\operatorname{cut}(C_{1}^{\prime})$.

This proves the claim for finite extensions. For an infinite extension, every
node also contained in a finite extension. Due to uniqueness of the
homomorphisms, we can define the $\varphi_{1,D}^{2}$ in the case of an
infinite $D$ as the union of all homomorphisms of smaller finite extensions.

Equipped with Prop. 2.4, we can now lift the concept of adequate order to the
level of symbolic branching processes. Compared to [7, 8], the monomorphism
$\varphi_{1,D}^{2}$ defined above replaces the isomorphism $I_{1}^{2}$ between
${\Uparrow}C_{1}$ and ${\Uparrow}C_{2}$ for two low-level configurations
$C_{1},C_{2}$ representing the same marking.

######  Definition 2.6 (Adequate order)

A partial order $\prec$ on the finite configurations of the symbolic unfolding
of a high-level Petri net is an _adequate order_ if:

  1. i)

$\prec$ is well-founded,

  2. ii)

$C_{1}\subset C_{2}$ implies $C_{1}\prec C_{2}$, and

  3. iii)

$\prec$ is preserved by finite extensions in the following way: if
$C_{1},C_{2}$ are two finite configurations, and $C_{1}{\oplus}D$ is a finite
extension of $C_{1}$ such that there is a marking
$M\in\mathcal{M}(C_{1})\cap\mathcal{M}(C_{2})$ satisfying $C_{1}\llbracket
M\rrbracket D$, then the monomorphism $\varphi_{1,D}^{2}$ from above satisfies
$C_{1}\prec C_{2}\Rightarrow C_{1}{\oplus}D\prec
C_{2}{\oplus}\varphi_{1,D}^{2}(D)$.

In the case of a P/T net interpreted as a high-level net, we have
$|\mathcal{M}(C)|=1$ for every configuration $C$, and therefore, Def. 2.6
coincides with its P/T version [8]. We could alternatively generalize the P/T
case by replacing ‘$\exists M\in\mathcal{M}(C_{1})\cap\mathcal{M}(C_{2})$ s.t.
$C_{1}\llbracket M\rrbracket D$’ by ‘$\mathcal{M}(C_{1})=\mathcal{M}(C_{2})$’,
and use the isomorphism $I_{1}^{2}$ between ${\Uparrow}C_{1}$ and
${\Uparrow}C_{2}$ to define preservation by finite extension. However, in the
upcoming generalization of the ERV-algorithm from [8], the generalized cut-off
criterion exploits property iii) of adequate orders. Using
‘$\mathcal{M}(C_{1})=\mathcal{M}(C_{2})$’ would produce an exponential blowup
of the generated prefix’s size. This is circumvented by using ‘$\exists
M\in\mathcal{M}(C_{1})\cap\mathcal{M}(C_{2})$ s.t. $C_{1}\llbracket
M\rrbracket D$’, which however leads to obtaining merely a monomorphism that
depends on the considered suffix, instead of an isomorphism between the
futures. We now show that this monomorphism sufficient:

The upcoming proof that the generalized ERV-algorithm is complete is
structurally analogous to the respective proof in [8]. It uses that, under the
conditions of Def. 2.6 iii), we also have $C_{2}\prec C_{1}\Rightarrow
C_{2}{\oplus}\varphi_{1,D}^{2}(D)\prec C_{1}{\oplus}D$. This result would
directly be obtained if $\varphi_{1,D}^{2}$ was an isomorphism, as $I_{1}^{2}$
is in the low-level case. However, a monomorphism is an isomorphism when its
codomain is restricted to its range. This idea is used in the proof of the
following proposition, which states that $\varphi_{1,D}^{2}$ indeed satisfies
the above property.

###### Proposition 2.7

Let $\prec$ be an adequate order. Under the conditions of Def. 2.6 iii) the
monomorphism $\varphi_{1,D}^{2}$ also satisfies $C_{2}\prec C_{1}\Rightarrow
C_{2}{\oplus}\varphi_{1,D}^{2}(D)\prec C_{1}{\oplus}D$.

###### Proof 2.8

Let $D^{\prime}=\varphi_{1,D}^{2}(D)$. We first show that
$\varphi_{2,D^{\prime}}^{1}(D^{\prime})=D$.

Let $\varphi_{1}:O(C_{1}|D)\to\varphi_{1,D}^{2}(O(C_{1}|D))$ be the
isomorphism that acts on $O(C_{1}|D)$ as $\varphi_{1,D}^{2}$ does, and let
$\varphi_{2}:O(C_{2}|D^{\prime})\to\varphi_{2,D^{\prime}}^{1}(O(C_{2}|D^{\prime}))$
be the isomorphism that acts on $O(C_{2}|D^{\prime})$ as
$\varphi_{2,D^{\prime}}^{1}$ does. Since
$\varphi_{1}^{-1}:\varphi_{1,D}^{2}(O(C_{1}|D))\to O(C_{1}|D)$ and
$O(C_{1}|D)\subset{\Uparrow}C_{1}$, and
$\varphi_{1}^{-1}(\varphi_{1,D}^{2}(D))=D$ is a suffix of $C_{1}$, we get by
Prop. 2.4 that $\varphi_{1}^{-1}=\varphi_{2}$, which means
$\varphi_{2,D^{\prime}}^{1}(D^{\prime})=D$.

Assume now $C_{2}\prec C_{1}$. From the proof of Prop. 2.4 we see that
$C_{2}\llbracket M\rrbracket\varphi_{1,D}^{2}(D)$. Thus, we get by the
definition of adequate order and the result above that
$C_{2}{\oplus}\varphi_{1,D}^{2}(D)\prec
C_{1}{\oplus}\varphi_{2,\varphi_{1,D}^{2}(D)}^{1}(\varphi_{1,D}^{2}(D))\allowbreak=C_{1}{\oplus}D$

In [8], Esparza et al. discuss three adequate orders on the configurations of
the low-level unfolding. In particular, they present a _total_ adequate order
that uses the _Foata normal form_ of configurations. Using such a total order
in the algorithm limits the size of the resulting finite and complete prefix;
It contains at most $|\mathcal{R}(N)|$ non cut-off events. All three adequate
orders presented in [8] can be directly lifted to the configurations of the
symbolic unfolding by exchanging every low-level term by its high-level
counterpart. The lifted order using the Foata normal form is still a total
order. We include these discussions in App. A.1.

We now define cut-off events in a symbolic unfolding. In the low-level case
[8], $\mathsf{e}$ is a cut-off event if there is another event
$\mathsf{e}^{\prime}$ satisfying $[\mathsf{e}^{\prime}]\prec[\mathsf{e}]$ and
$\operatorname{mark}([\mathsf{e}])=\operatorname{mark}([\mathsf{e}^{\prime}])$,
which ensures that the future of $\mathsf{e}$ needs not be considered further.
In the high-level case, we generalize these conditions to high-level events
$e$. However, we do not require the existence of _one_ other high-level event
$e^{\prime}$ with $[e^{\prime}]\prec[e]$ and
$\mathcal{M}([e])=\mathcal{M}([e^{\prime}])$. While this would still be a
valid cut-off criterion and would lead to finite and complete prefixes, the
upper bound on the size of such a prefix would be exponential in the number of
markings in the original net. Instead, we check whether $\mathcal{M}([e])$ is
contained in the union of _all_ $\mathcal{M}([e^{\prime}])$ with
$[e^{\prime}]\prec[e]$. This criterion expresses that we have already seen
every marking in $\mathcal{M}([e])$ in the prefix $\beta$ under construction,
and therefore need not consider the future of $e$ any further. By this, we
obtain the same upper bounds as in [8], as discussed later.

######  Definition 2.9 (Cut-off event)

Let $\prec$ be an adequate order on the configurations of the symbolic
unfolding of a high-level Petri net. Let $\beta$ be a prefix of the symbolic
unfolding containing a high-level event $e$. The high-level event $e$ is a
_cut-off_ event in $\beta$ (w.r.t. $\prec$) if
$\mathcal{M}([e])\subseteq\bigcup_{[e^{\prime}]\prec[e]}\mathcal{M}([e^{\prime}]).$

When interpreting P/T nets as high-level nets, this definition corresponds to
the cut-off events defined in [8], since then $|\mathcal{M}([e])|=1$ for all
events $e$.

###  2.2 The Generalized ERV-Algorithm

We present the algorithm for constructing a finite and complete prefix of the
symbolic unfolding of a given high-level Petri net. It is a generalization of
the ERV-algorithm from [8], and is structurally equal (and therefore looks
very similar). However, the algorithm is contingent upon the previous
section’s work of generalizing adequate orders and cut-off events, which
ultimately enables us to adopt this structure.

A crucial concept of the ERV-algorithm is the notion of “possible extensions”,
i.e., the set of individual events that extend a given prefix of the
unfolding. In Def. 2.10, we lift this concept to the level of symbolic
unfoldings. We do so by isolating the procedure of adding high-level events in
the algorithm from [11] which generates the complete symbolic unfolding of a
given high-level Petri net (but does not terminate if the symbolic unfolding
is infinite).

We define the data structures similarly to [8]. There, an event is given by a
tuple $\mathsf{e}=(\mathsf{t},\mathsf{B}^{\prime})$ with
$\mathsf{h}(\mathsf{e})=\mathsf{t}\in\mathsf{T}$ and
$\mathit{pre}(\mathsf{e})=\mathsf{B}^{\prime}\subseteq\mathsf{B}$, and a
condition given by a tuple $\mathsf{b}=(\mathsf{p},\mathsf{e})$ with
$\mathsf{h}(\mathsf{b})=\mathsf{p}\in\mathsf{P}$ and
$\mathit{pre}(\mathsf{b})=\\{\mathsf{e}\\}\subseteq\mathsf{E}$. The finite and
complete prefix is a set of such events and transitions.

In the high-level case, we need more information inside the tuples. A high-
level event is given by a tuple $e=(t,X,\mathit{pred})$ described by $h(e)=t$,
$\mathit{pre}(e)=X\subseteq B\times\mathit{Var}$, and
$\mathit{pred}(e)=\mathit{pred}$. Analogously, a high-level condition is given
by a tuple $b=(p,(e,v),\mathit{pred})$, where $h(b)=p$,
$\mathit{pre}(b)=(e,v)\in(E\times\mathit{Var})\cup(\\{\bot\\}\times\\{v^{b}\,\mid\,b\in
B_{0}\\})$, and $\mathit{pred}(\mathbf{e}(b))=\mathit{pred}$.

######  Definition 2.10 (Possible extensions)

Let $\beta=(O,h)$ be a branching process of a high-level Petri net $N$. The
_possible extensions_ $\mathit{PE}(\beta)$ are the set of tuples
$e=(t,X,\mathit{pred})$ where $t$ is a transition of $N$, and $X\subseteq
B\times\mathit{Var}$ satisfying

  * •

$\\{b\,\mid\,(b,v)\in X\\}$ is a co-set, and
$\mathit{pre}(t)=\\{(h(b),v)\,\mid\,(b,v)\in X\\}$,

  * •

$\mathit{pred}=\mathit{loc\text{-}pred}\land\big{(}\bigwedge_{(b,v)\in
X}\mathit{pred}(\mathbf{e}(b))\big{)}$ is satisfiable,
where $\mathit{loc\text{-}pred}=\iota(t)[v\leftarrow
v_{e}]_{v\in\mathit{Var}(e)}\land\big{(}\bigwedge_{(b,v)\in
X}v_{e}=\mathbf{v}_{\mathbf{e}}(b)\big{)}$,

  * •

$\mathit{Fin}$ does not contain $(t,X,\mathit{pred})$.

Since the notion of co-set in high-level occurrence nets is achieved by the
direct translation from low-level occurrence nets plus the “color conflict
freedom”, possible extensions in a prefix $\beta$ can be found by searching
first for sets of conditions that are not in structural conflict as in the
low-level case, and then checking whether these sets are in color conflict.

Alg. 1 is a generalization of the ERV-Algorithm in [8] for complete finite
prefixes of the low-level unfolding. The structure is taken from there, with
the only difference being the special initial transition $\bot$. It takes as
input a high-level Petri net $N\in\mathbf{N}_{\mathbf{F}}$ and assumes a given
adequate order $\prec$.

Data: High-level Petri net
$N=(P,T,F,\iota,\mathcal{M}_{0})\in\mathbf{N}_{\mathbf{F}}$.

Result: A complete finite prefix $\mathit{Fin}$ of the symbolic unfolding of
$N$.

$\mathit{Fin}\leftarrow\\{\bot\\}$;

$\mathit{pred}(\bot)\leftarrow\bigvee_{M_{0}\in\mathcal{M}_{0}}\bigwedge_{(p,c)\in
M_{0}}v_{\bot}^{b_{p}}=c$;

foreach  _$p\in P_{0}$_ do

Create a fresh condition $b_{p}=(p,(\bot,v^{b_{p}}),\mathit{pred}(\bot))$;

$\mathit{Fin}\leftarrow\mathit{Fin}\cup\\{b\\}$;

end foreach

$\mathit{pe}\leftarrow\mathit{PE}(\mathit{Fin})$;

$\operatorname{\mathit{cut-off}}\leftarrow\emptyset$;

while  _$\mathit{pe}\neq\emptyset$_ do

Pick $e=(t,X,\mathit{pred})$ from $\mathit{pe}$ such that $[e]$ is minimal
w.r.t. $\prec$;

if  _$[e]\cap\operatorname{\mathit{cut-off}}=\emptyset$_ then

$\mathit{Fin}\leftarrow\mathit{Fin}\cup\\{e\\}$;

foreach  _$(p,v)\in\mathit{post}(t)$_ do

Create a fresh condition $b=(p,(e,v),\mathit{pred})$;

$\mathit{Fin}\leftarrow\mathit{Fin}\cup\\{b\\}$;

end foreach

$\mathit{pe}\leftarrow\mathit{PE}(\mathit{Fin})$;

if  _$e$ is a cut-off event of $\mathit{Fin}$_ then

$\operatorname{\mathit{cut-off}}\leftarrow\operatorname{\mathit{cut-
off}}\cup\\{e\\}$;

end if

else

$\mathit{pe}\leftarrow\mathit{pe}\setminus\\{e\\}$

end if

end while

Algorithm 1 Generalization of the ERV-Algorithm from [8] for complete finite
prefixes.

###### Example 2.11

Consider the running example $N$ from Figure 1(a). Alg. 1 produces the
complete finite prefix marked by the blue line in Figure 1(b). Cut-off events
are shaded blue.

Starting with the initial conditions $a^{\prime}$ abd $b^{\prime}$, the
possible extensions are $\alpha^{\prime}$ and $\beta^{\prime}$. assuming
$[\alpha^{\prime}]\prec[\beta^{\prime}]$, we first attach $\alpha^{\prime}$
and a condition $c^{\prime}$ corresponding to the output place $c$ of
$\alpha$, and then analogously $\beta^{\prime}$ and the condition
$d^{\prime}$.

For $\alpha^{\prime}$ we have
$\mathcal{M}([\alpha^{\prime}])=\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}(c,n),(b,0)\mathclose{\,{|}\;\\!\\!\\!{\\}}}\,\mid\,n\in\\{1,\dots,m\\}\\}$
and analogously, for $\beta^{\prime}$ we have
$\mathcal{M}([\beta^{\prime}])=\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}(a,0),(d,n)\mathclose{\,{|}\;\\!\\!\\!{\\}}}\,\mid\,n\in\\{1,\dots,m\\}\\}$.
Since we have not seen these markings before, neither $\alpha^{\prime}$ nor
$\beta^{\prime}$ is a cut-off event. Thus, we have the possible extensions
$t^{\prime}$ and $\varepsilon^{\prime}$. For $t^{\prime}$ we have
$\mathcal{M}([t^{\prime}])=\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}\mathclose{\,{|}\;\\!\\!\\!{\\}}}\\}$,
since no tokens are in the net after firing $t$. However, we have not seen the
empty marking
$\mathopen{{\\{}\;\\!\\!\\!{|}\,}\mathclose{\,{|}\;\\!\\!\\!{\\}}}$ before, so
formally, $t^{\prime}$ is not a cut-off event.

For $\varepsilon^{\prime}$ we have
$\mathcal{M}([\varepsilon^{\prime}])=\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}(c,n),(d,n^{\prime})\mathclose{\,{|}\;\\!\\!\\!{\\}}}\,\mid\,n,n^{\prime}\in\\{1,\dots,m\\}\\}$.
Corresponding cuts can be reached in the prefix constructed so far by
concurrently firing $\alpha^{\prime}$ and $\beta^{\prime}$. However, no
marking
$\mathopen{{\\{}\;\\!\\!\\!{|}\,}(c,n),(d,n^{\prime})\mathclose{\,{|}\;\\!\\!\\!{\\}}}$
is represented by a _cone_ configuration before $\varepsilon^{\prime}$, and
therefore $\varepsilon^{\prime}$ does _not_ satisfy
$\mathcal{M}([\varepsilon^{\prime}])\subseteq\bigcup_{[e^{\prime}]\prec[\varepsilon^{\prime}]}\mathcal{M}([e^{\prime}])$.
This means $\varepsilon^{\prime}$ is not a cut-off event and we have to
proceed with the possible extensions $t^{\prime\prime}$ and
$\varepsilon^{\prime\prime}$.

Since
$\mathcal{M}([t^{\prime\prime}])=\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}\mathclose{\,{|}\;\\!\\!\\!{\\}}}\\}=\mathcal{M}([t^{\prime}])$
with $[t^{\prime}]\prec[t^{\prime\prime}]$, have that $t^{\prime\prime}$ is a
cut-off event. This, however, has no impact on the prefix since we cannot
continue after $t^{\prime\prime}$ anyway. For $\varepsilon^{\prime\prime}$ we
have
$\mathcal{M}([\varepsilon^{\prime\prime}])=\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}(c,n),(d,n^{\prime})\mathclose{\,{|}\;\\!\\!\\!{\\}}}\,\mid\,n,n^{\prime}\in\\{1,\dots,m\\}\\}=\mathcal{M}([\varepsilon^{\prime}])$
with $[\varepsilon^{\prime}]\prec[\varepsilon^{\prime\prime}]$. This makes
$\varepsilon^{\prime\prime}$ also a cut-off event. We therefore have no more
possible extensions, and the algorithm terminates. In the figure, this is
indicated by the blue lines.

We now prove correctness of Alg. 1 analogously to [8], by stating two
propositions – one each to show that the prefix is finite and complete,
respectively. The proof structure is also as in [8], but adapted to the
setting of high-level Petri nets and symbolic unfoldings.

###### Proposition 2.12

$\mathit{Fin}$ is finite.

Given an event $e$, define the _depth_ of $e$ as the length of the longest
chain of events $e_{1}<e_{2}<\dots<e$; the depth of $e$ is denoted by
$0pt(e)$.

###### Proof 2.13

As in [8], we prove the following results (1) – (3):

  1. (1)

For every event $e$ of $\mathit{Fin}$, $0pt(e)\leq|\mathcal{R}(N)|+1$,

  2. (2)

For every event $e$ of $\mathit{Fin}$, the sets $\mathit{pre}(e)$ and
$\mathit{post}(e)$ are finite, and

  3. (3)

For every $k\geq 0$, $\mathit{Fin}$ contains only finitely many events $e$
such that $0pt(e)\leq k$.

This works exactly as in [8], with minor adaptations to the generalization of
cut-offs in the symbolic unfolding in (1):

  1. (1)

Let $n=|\mathcal{R}(N)|$. Every chain of events
$e_{1}<e_{2}<\dots<e_{n}<e_{n+1}$ in the unfolding contains an event $e_{i}$,
$i>1$, s.t.
$\mathcal{M}([e_{i}])\subseteq\bigcup_{j=1}^{i-1}\mathcal{M}([e_{j}])$, since,
if every $\mathcal{M}([e_{j}])$, $j=1,\dots,n$, contains a marking not
contained in $\bigcup_{k=1}^{j-1}\mathcal{M}([e_{k}])$, then finally
$\bigcup_{j=1}^{n}\mathcal{M}([e_{j}])$ contains all $n$ markings. This makes
$e_{n+1}$ a cut-off event.

  2. (2)

By the construction in the algorithm we see that there is a bijection between
$\mathit{post}(e)$ and $\mathit{post}(h(e))$, and similarly for
$\mathit{pre}(e)$ and $\mathit{pre}(h(e))$. The result then follows from the
finiteness of $N$.

  3. (3)

By complete induction on $k$. The base case, $k=0$, is trivial. Let $E_{k}$ be
the set of events of depth at most $k$. We prove that if $E_{k}$ is finite
then $E_{k+1}$ is finite. By (2) and the induction hypothesis,
$\mathit{post}(E_{k})$ is finite. Since $\\{b\,\mid\,\exists
v\in\mathit{Var}:(b,v)\in\mathit{pre}(E_{k+1})\\}\subseteq\\{b\,\mid\,\exists
v\in\mathit{Var}:(b,v)\in\mathit{post}(E_{k})\\}$, we get by property iv in
the definition of occurrence nets that $E_{k+1}$ is finite.

###### Proposition 2.14

$\mathit{Fin}$ is complete.

The proof of this proposition also has the same general structure as the
respective proof in [8]. However here we use the generalizations of adequate
order, possible extensions, and the cut-off criterion to symbolic branching
processes.

###### Proof 2.15

We first show that for every reachable marking in $N$ there exists a
configuration in $\varUpsilon$ satisfying a) from the definition of complete
prefixes, and then show that one of these configurations (a minimal one) also
satisfies b).

  1. (1)

Let $M$ be an arbitrary reachable marking in $N$. Then by Prop. 1.6, we have
that there is a $C_{1}\in\mathcal{C}(\varUpsilon)$ s.t.
$M\in\mathcal{M}(C_{1})$. Let $\theta_{1}\in\Theta(C_{1})$ s.t.
$M=\operatorname{mark}(C_{1}.\theta_{1})$. If $C$ is not a configuration in
$\mathit{Fin}$, then it contains a cut-off event $e_{1}$, and so
$C_{1}=[e_{1}]{\oplus}D$ for some set $D$ of events. Let
$M_{1}=\operatorname{mark}([e_{1}].\theta_{1}|_{\mathit{Var}_{[e_{1}]\cup\\{\bot\\}}})\in\mathcal{M}([e_{1}])$.
By the definition of cut-off event, there exists an event $e_{2}$ with
$[e_{2}]\prec[e_{1}]$ and $M_{1}\in\mathcal{M}([e_{2}])$. Since we have
$C_{1}\llbracket M_{1}\rrbracket D$, we get by Prop. 2.4 that the monomorphism
$\varphi_{1}:=\varphi_{[e_{1}],D}^{[e_{2}]}:O([e_{1}]|D)\to{\Uparrow}[e_{2}]$
exists and that $\varphi_{1}(D)$ is a suffix of $[e_{2}]$. By Prop. 2.7 we
know

$C_{2}:=[e_{2}]{\oplus}\varphi_{1}(D)\prec[e_{1}]{\oplus}D=C_{1}.$

Let $\theta_{2}^{\prime}\in\Theta([e_{2}])$ s.t.
$M_{1}=\operatorname{mark}([e_{2}],\theta_{2}^{\prime})$. Define now
$\theta_{2}\in\Theta(C_{2})$ by
$\theta_{2}=\theta_{2}^{\prime}\uplus\theta_{2}^{\prime\prime}$, where
$\theta_{2}^{\prime\prime}:\mathit{Var}_{\varphi_{1}(D)}\to\mathit{Col}$ is
given by $\theta_{2}^{\prime\prime}(v_{\varphi_{1}(e)})=\theta_{1}(v_{e})$. By
this construction we get
$M=\operatorname{mark}(C_{2},\theta_{2})\in\mathcal{M}(C_{2})$.

If $C_{2}$ is not a configuration of $\mathit{Fin}$, then we can iterate the
procedure and find a configuration $C_{3}$ such that $C_{3}\prec C_{2}$ and
$M\in\mathcal{M}(C_{3})$. The procedure cannot be iterated infinitely often
because $\prec$ is well-founded. Therefore, it terminates in a configuration
of $\mathit{Fin}$.

  2. (2)

Let now $C$ be a minimal configuration w.r.t. $\prec$ s.t.
$M\in\mathcal{M}(C)$, and let $t\in T$, $\sigma\in\Sigma(t)$ s.t.
$M[t,\sigma\rangle$. If $C$ contains some cut-off event, then we can apply the
arguments of a) to conclude that $\mathit{Fin}$ contains a configuration
$C^{\prime}\prec C$ such that $M\in\mathcal{M}(C^{\prime})$. This contradicts
the minimality of $C$. So $C$ contains no cut-off events. Let
$\theta\in\Theta(C)$ s.t. $M=\operatorname{mark}(C,\theta)$. Since
$\mathit{pre}(t.\sigma)\subseteq M$, we have that there is a co-set
$B_{t,\sigma}\subseteq\operatorname{cut}(C)$ s.t.
$\mathit{pre}(t,\sigma)=\\{(h(b),\theta(\mathbf{v}_{\mathbf{e}}(b)))\,\mid\,b\in
B_{t,\sigma}\\}$. Let now $X:=\\{(b,v)\,\mid\,b\in
B_{t,\sigma},(h(b),v)\in\mathit{pre}(t)\\}$. We then have $\forall(b,v)\in
X:\sigma(v)=\theta(\mathbf{v}_{\mathbf{e}}(b))$.

We now show that

$\mathit{pred}:=\iota(t)[v\leftarrow
v_{e}]_{v\in\mathit{Var}(e)}\land\Big{(}\bigwedge_{(b,v)\in
X}v_{e}=\mathbf{v}_{\mathbf{e}}(b)\Big{)}\land\bigwedge_{(b,v)\in
X}\mathit{pred}(\mathbf{e}(b))$

is satisfiable. Let $\theta^{\prime}:=\theta\uplus(\sigma\circ[v_{e}\mapsto
v]_{v\in\mathit{Var}(e)})$. Then

     * •

$\iota(t)[v\leftarrow
v_{e}]_{v\in\mathit{Var}(e)}[\theta^{\prime}]\equiv\iota(t)[\sigma]\equiv\mathit{true}$,
and

     * •

$\big{(}\bigwedge_{(b,v)\in
X}v_{e}=\mathbf{v}_{\mathbf{e}}(b)\big{)}[\theta^{\prime}]\equiv\big{(}\bigwedge_{(b,v)\in
X}\sigma(v)=\theta(\mathbf{v}_{\mathbf{e}}(b))\big{)}\equiv\mathit{true}$, and

     * •

$\bigwedge_{(b,v)\in
X}\mathit{pred}(\mathbf{e}(b))[\theta^{\prime}]\equiv\bigwedge_{(b,v)\in
X}\mathit{pred}(\mathbf{e}(b))[\theta]\equiv\mathit{true}$, since
$\theta\in\Theta(C)$.

Thus, $\mathit{pred}[\theta^{\prime}]\equiv\mathit{true}$. Therefore,
$e=(t,X,\mathit{pred})$ is a possible extension and added in the execution of
the algorithm. Then we directly have $e\notin C$, $h(e)=t$, and with the same
arguments as in a), we get $C\cup\\{e\\}\in\mathcal{C}(\mathit{Fin})$ and
$\theta\uplus(\sigma\circ[v_{e}\mapsto
v]_{v\in\mathit{Var}(e)})\in\Theta(C\cup\\{e\\})$, which means
$\operatorname{cut}(C,\theta)[e,\sigma\rangle$. Since we chose $\theta$
independently of $t$ and $\sigma$, this concludes the proof.

Notice that by this construction, as described in [8], we get that if $\prec$
is a total order, then $\mathit{Fin}$ contains at most $|\mathcal{R}(N)|$ non
cut-off events. As already discussed in Sec. 2.1, the total adequate order
defined in [8] can be lifted to the configurations in the symbolic unfolding,
where it again is total (cp. App. A.1). Thus, we generalized the possibility
to construct such a small complete finite prefix by application of Alg. 1 with
$\prec$ being a total adequate order.

##  3 High-level versus P/T Expansion

Every high-level Petri net represents a P/T Petri net with the same behavior,
in which the places can only carry a number tokens with color $\bullet$.
Markings in a P/T Petri net describe only how many tokens lie on each place.
Each transitions only has one possible firing mode that takes and/or lays a
fixed number of tokens from resp. onto each connected place.

In this section we state in Lemma 3.2 that the expansion of a finite complete
prefix of the unfolding of a high-level Petri net is a finite and complete
prefix of the unfolding of the expanded high-level Petri net. This means the
generalization of complete prefixes is “canonical”, and compatible with the
established low-level concepts. We then compare for our running example the
results of

  * •

applying the generalized ERV-algorithm Alg. 1 to obtain a complete finite
prefix of the symbolic unfolding of a given high-level Petri net, and

  * •

first expanding a given high-level Petri net and then applying the ERV-
algorithm from [8] for a complete finite prefix of the (P/T) unfolding.

The procedure of constructing the represented P/T Petri net
$\operatorname{Exp}(N)$ (called the _expansion_) of a high-level Petri net $N$
is well established (cp., e.g., Chapter 2.4 in [3]), and we describe it here
only briefly; the places of $\operatorname{Exp}(N)$ are given by
$\mathsf{P}=\\{p.c\,\mid\,p\in P,c\in\mathit{Col}\\}$, and its transitions by
$\mathsf{T}=\\{t.\sigma\,\mid\,t\in T,\sigma\in\Sigma(t)\\}$. There is an arc
from $p.c$ to $t.\sigma$ iff $(p,c)\in\mathit{pre}(t,\sigma)$, and analogously
for arcs from transitions to places. Markings in $\operatorname{Exp}(N)$ are
functions $\mathsf{M}:\mathsf{P}\to\mathbb{N}$, describing how often the only
color $\bullet$ lies on each place $p.c$. Every such marking corresponds to a
marking $M$ in the high-level net $N$, with $M(p,c)=\mathsf{M}(p.c)$, and a
transition $t$ can fire in mode $\sigma$ from $M$ iff $t.\sigma$ can fire from
$\mathsf{M}$. Thus, we say that $N$ and $\operatorname{Exp}(N)$ have the same
behavior. For a finite high-level Petri net $N$, the expansion
$\operatorname{Exp}(N)$ is finite iff $\mathit{Col}$ is finite.

The _(low-level) unfolding_ of a P/T Petri net $\mathsf{N}$ is a tuple
$\Upsilon(\mathsf{N})=(\mathsf{U}(\mathsf{N}),\textnormal{p}^{\mathsf{N}})$,
where $\mathsf{U}(\mathsf{N})$ is an _occurrence net_ , and
$\textnormal{p}^{\mathsf{N}}:\mathsf{U}(\mathsf{N})\to\mathsf{N}$ is a _Petri
net homomorphism_ such that
$(\mathsf{U}(\mathsf{N}),\textnormal{p}^{\mathsf{N}})$ is a _maximum branching
process_ of $\mathsf{N}$. Since the definition of (low-level) branching
processes and homomorphisms is firstly well established in the literature, and
secondly so similar to their corresponding high-level definitions, we omit
them here and refer the reader for example to [6, 8].

With the notation of low-level unfoldings of P/T nets we can define for a
high-level occurrence net $O$, the P/T occurrence net
$\operatorname{Exp_{O}}(O)=\mathsf{U}(\operatorname{Exp}(O))$ (i.e., the
occurrence net from the unfolding
$\Upsilon(\operatorname{Exp}(O))=(\mathsf{U}(\operatorname{Exp}(O)),\textnormal{p}^{\operatorname{Exp}(O)})$).
We abbreviate $\textnormal{p}^{\operatorname{Exp}(O)}$ by
$\textnormal{p}^{O}$. The operator $\operatorname{Exp_{O}}$ therefore maps
high-level occurrence nets to occurrence nets (cf. [4]). Let now $\beta=(O,h)$
be a symbolic branching process of $N$. Then we can define the _expanded
symbolic branching process_
$\operatorname{Exp_{O}}(\beta)=(\operatorname{Exp_{O}}(O),\mathsf{h})$ of
$\operatorname{Exp}(N)$ with the homomorphism
$\mathsf{h}:\operatorname{Exp_{O}}(O)\to\operatorname{Exp}(N)$, defined by
$\mathsf{h}(\mathsf{e})=t.\sigma\Leftrightarrow\textnormal{p}^{O}(\mathsf{e})=e.\sigma\land
h(e)=t$ and
$\mathsf{h}(\mathsf{b})=p.c\Leftrightarrow\textnormal{p}^{O}(\mathsf{b})=b.c\land
h(b)=p$ for events $\mathsf{e}$ resp. conditions $\mathsf{b}$ in
$\operatorname{Exp_{O}}(O)$. The following diagram serves as an overview:

The following result is shown in [4]. It states that, for a high-level Petri
net $N$, the unfolding of $N$’s expansion is isomorphic to the expanded
symbolic unfolding of $N$.

######  Lemma 3.1 ([4], Sec. 4.1)

$\Upsilon(\operatorname{Exp}(N))\simeq\operatorname{Exp_{O}}(\varUpsilon(N))$.

With this result, we state the following:

###### Lemma 3.2

Let $N$ be a high-level Petri net and $\beta$ be a prefix of $\varUpsilon(N)$.
Then $\beta$ is finite and complete if and only if
$\operatorname{Exp_{O}}(\beta)$ is a finite and complete prefix of
$\Upsilon(\operatorname{Exp}(N))$.

The proof uses the results from Prop. 1.6 and Prop. 1.8, since the definition
of completeness on the symbolic level is a direct translation from its P/T
analogue.

###### Proof 3.3

Let $\beta=(O,h)$ be finite and complete. From Lemma 3.1 we already know that
$\operatorname{Exp_{O}}(O)\subseteq\mathsf{U}(\operatorname{Exp}(N))$. Since
$\operatorname{Exp_{O}}(\beta)$ is a branching process of
$\operatorname{Exp}(N)$, we see that is a prefix of the unfolding of
$\operatorname{Exp}(N)$. Also, $\operatorname{Exp_{O}}(\beta)$ is obviously
finite since $O$ is a finite high-level occurrence net.

We now prove that
$\operatorname{Exp_{O}}(\beta)=(\operatorname{Exp_{O}}(O),\mathsf{h})$ is
complete. Let $\mathsf{M}$ be a reachable marking in $\operatorname{Exp}(N)$.
Then the high-level marking $M$ defined by $M(p,c)=\mathsf{M}(p.c)$ is
reachable in $N$. Thus, since $\beta$ is complete, there is a configuration
$C\in\mathcal{C}(\beta)$ and an instantiation $\theta\in\Theta(C)$ satisfying
a) and b) from Def. 2.1. This means there is a firing sequence
$K_{0}[e_{1},\sigma_{1}\rangle K_{1}\dots[e_{n},\sigma_{n}\rangle K_{n}$ with
$\\{e_{1},\dots,e_{n}\\}=C$, $\sigma_{i}=\theta\circ[v\mapsto
v_{e_{i}}]_{v\in\mathit{Var}(e_{i})}$, and
$K_{n}=\operatorname{cut}(C,\theta)$ (meaning
$M=\operatorname{mark}(C,\theta)=\mathopen{{\\{}\;\\!\\!\\!{|}\,}(h(b),c)\,\mid\,(b,c)\in
K_{n}\mathclose{\,{|}\;\\!\\!\\!{\\}}}$). Then, in $\operatorname{Exp}(O)$,
the marking $\mathopen{{\\{}\;\\!\\!\\!{|}\,}b.c\,\mid\,(b,c)\in
K_{n}\mathclose{\,{|}\;\\!\\!\\!{\\}}}$ is reachable from the initial marking
$\mathopen{{\\{}\;\\!\\!\\!{|}\,}b.c\,\mid\,(b,c)\in
K_{0}\mathclose{\,{|}\;\\!\\!\\!{\\}}}$ by the firing sequence
$(e_{1}.\sigma_{1},\dots,e_{n}.\sigma_{n})$. Thus, there is a configuration
$\mathsf{C}=\\{\mathsf{e}_{1},\dots,\mathsf{e}_{n}\\}$ in
$\mathsf{U}(\operatorname{Exp}(O))=\operatorname{Exp_{O}}(O)$ with $\forall
i:\textnormal{p}^{\mathrm{O}}(\mathsf{e}_{i})=e_{i}.\sigma_{i}$. Then, by the
definition of $\mathsf{h}$, we get
$\operatorname{mark}^{\mathsf{h}}(\mathsf{C}):=\mathopen{{\\{}\;\\!\\!\\!{|}\,}\mathsf{h}(\mathsf{b})\,\mid\,\mathsf{b}\in\operatorname{cut}(\mathsf{C})\mathclose{\,{|}\;\\!\\!\\!{\\}}}=\mathopen{{\\{}\;\\!\\!\\!{|}\,}h(b).c\,\mid\,(b,c)\in
K_{n}\mathclose{\,{|}\;\\!\\!\\!{\\}}}=\mathsf{M}$.

Let now $t.\sigma\in\mathsf{T}$ s.t. $\mathsf{M}[t.\sigma\rangle$. Then
$M[t,\sigma\rangle$. Since $C$, $\theta$ satisfy property b) from Def. 2.1, we
know that $\exists e\in E$ s.t. $e\notin C$, $h(e)=t$, and
$C,\theta[e,\sigma\rangle$. This means, in $\operatorname{Exp}(\beta)$, we
have $\mathopen{{\\{}\;\\!\\!\\!{|}\,}b.c\,\mid\,(b,c)\in
K_{n}\mathclose{\,{|}\;\\!\\!\\!{\\}}}[e.\sigma\rangle$. Thus, there exists an
$\mathsf{e}$ in $\mathsf{U}(\operatorname{Exp}(\beta))$ such that
$\mathsf{C}[\mathsf{e}\rangle$ and
$\textnormal{p}^{\mathrm{O}}(\mathsf{e})=e.\sigma$, which again means that
$\mathsf{h}(\mathsf{e})=h(e).\sigma=t.\sigma$. This proves that
$\operatorname{Exp_{O}}(\beta)$ is complete.

The other direction works analogously.

We can now compare the two complete finite prefixes resulting from the
original ERV-algorithm from [8] applied to $\operatorname{Exp}(N)$ and the
generalized ERV-algorithm Alg. 1 applied to $N\in\mathbf{N}_{\mathbf{F}}$.
From the definition of the generalized cut-off criterion we get that both
these prefixes have the same depth. However, due to the high-level
representation, the breadth of the symbolic prefix can be substantially
smaller. This is the case for our running example:

###### Example 3.4

Figure 3: The complete finite prefix of $\Upsilon(\operatorname{Exp}(N))$ of
the running example $N$ from Figure 1(a) calculated by the original ERV-
Algorithm.

Consider again $N\in\mathbf{N}_{\mathbf{F}}$ from Figure 1(a) with
$\mathit{Col}=\\{0,1,\dots,m\\}$ for a fixed $m>0$. The finite complete prefix
of $\Upsilon(\operatorname{Exp}(N))$ is depicted in Fig. 3. Instead of giving
each event/condition a distinct name, we indicated the label of each node
inside of it. For events with label $\varepsilon$ we even omitted the mode,
since it is derivable from the connected conditions. Cut-off events and their
output conditions are again shaded blue, and the blue line indicates the
complete finite prefix resulting from the original ERV-algorithm.

After firing an instance of $\alpha$ and an instance of $\beta$, we arrive at
conditions with labels $c.k$ and $d.\ell$. If these satisfy $\ell=k\cdot 3$
then we can fire an instance of $t$, which means we have
$\lfloor\frac{m}{3}\rfloor$ such events. Only the first is no cut-off event,
since their configurations all represent the same (empty) marking. This empty
marking is however also the reason why we cannot continue even after the first
instance of $t$.

For each combination of an output condition of an instance of $\alpha$ (the
$m$ instances of $c$) and an output condition of an instance of $\beta$ (the
$m$ instances of $d$), we have $m^{2}$ possibilities to fire an instance of
$\varepsilon$. The reason for this is that in the high-level net $N$, the
output variables are independent of the input variables. This leads to $m^{4}$
many $\varepsilon$-events of depth $2$.

All except the first $m^{2}$ of those are cut-off events. After the non cut-
off events, however, we have to repeat the part from above for the ERV-
algorithm to terminate. All in all the complete finite prefix contains
$6m^{4}+4m+2\lfloor\frac{m}{3}\rfloor+2$ nodes for every fixed $m$ in the
color class $\mathit{Col}=\\{0,1,\dots,m\\}$. The complete finite prefix of
the _symbolic_ unfolding $\varUpsilon(N)$ that is shown in Figure 1(b), on the
other hand has the same number of nodes for every $m$.

Generalizing this example to a family of nets gives the following proposition:

###### Proposition 3.5

For every $n\in\mathbb{N}$, there is a family $(N_{m}^{n})_{m>1}$ of high-
level nets in $\mathbf{N}_{\mathbf{F}}$ such that every $N_{m}^{n}$ has the
set of colors $\mathit{Col}=\\{0,\dots,m\\}$ and satisfies that

  * •

the complete finite prefix of $\varUpsilon(N_{m}^{n})$ obtained by Alg. 1 has
the same number of nodes for every $m$,

  * •

the number of nodes in the low-level prefix of
$\Upsilon(\operatorname{Exp}(N_{m}^{n}))$ obtained by the original ERV-
algorithm is greater than $m^{n}$.

In particular, the benchmark family Fork And Join, presented in Sec. 6.2.1
satisfies this property.

##  4 Handling Infinitely Many Reachable Markings

Unfoldings of unbounded P/T Petri nets (i.e., with infinitely many markings)
have been investigated in [15, 16], and in [17] concurrent well-structured
transition systems with infinite state space are unfolded. When applying the
generalized ERV-algorithm, Alg. 1, to high-level Petri nets with infinitely
many reachable markings (therefore violating (3) from the definition of
$\mathbf{N}_{\mathbf{F}}$), the proof for finiteness of the resulting prefix
does not hold anymore: the proof of Prop. 2.12, step (1), is a generalization
of the proof of the respective claim in [8] (which uses the pigeonhole
principle). It is argued that we cannot have $|\mathcal{R}(N)|+1$ consecutive
events s.t. their cone configurations each generate a marking in the net not
seen before, and we thus have a cut-off event. When we deal with infinitely
many markings, this argument cannot be made.

In this section, we introduce a class $\mathbf{N}_{\mathbf{SC}}$ of safe high-
level nets, called symbolically compact, that have possibly infinitely many
reachable markings (and therefore an infinite expansion), generalizing the
class $\mathbf{N}_{\mathbf{F}}$. We then proceed to make adaptions to Alg. 1
(i.e., to the used cut-off criterion), so that it generates a finite and
complete prefix of the symbolic unfolding for any
$N\in\mathbf{N}_{\mathbf{SC}}$.

The following Lemma precisely describes the finite high-level Petri nets for
which a finite and complete prefix of the symbolic unfolding exists. They are
characterized by having a bound on the number of steps needed to arrive at
every reachable marking. For the proof we argue that in the case of such a
bound, the symbolic unfolding up to depth $n+1$ is a finite and complete
prefix, and that in the absence of such a bound no depth of a prefix is enough
for it to be complete.

###### Lemma 4.1

For a finite high-level Petri net $N=(\mathcal{N},\mathcal{M}_{0})$ there
exists a finite and complete prefix of $\varUpsilon(N)$ if and only if there
exists a bound $n\in\mathbb{N}$ such that every marking in $\mathcal{R}(N)$ is
reachable from a marking in $\mathcal{M}_{0}$ by firing at most $n$
transitions.

###### Proof 4.2

From Prop. 1.6 and Prop. 1.8 we see that for a finite high-level Petri net
with such a bound $n$, the prefix of the symbolic unfolding containing exactly
the events $e$ with $0pt(e)\leq n+1$ is complete. Finiteness of this prefix
follows from the finiteness of the original net and the definition of
homomorphism.

Assume now that no such bound exists, and, for the purpose of contradiction,
assume that there is a finite and complete prefix $\beta$ of $\varUpsilon(N)$.
Denote $\widetilde{n}=\max\\{|C|\,\mid\,C\in\mathcal{C}(\beta)\\}<\infty$.
Then there exists a marking $M\in\mathcal{R}(N)$ for which we have to fire at
least $\widetilde{n}+1$ transitions to reach it. Again from Prop. 1.6 and
Prop. 1.8 it follows that a configuration $C$ with $M\in\mathcal{M}(C)$ must
contain at least $\widetilde{n}+1$ events, contradicting that $\beta$ is
complete.

###  4.1 Symbolically Compact High-level Petri Nets

We use the result of Lemma 4.1 to define the class $\mathbf{N}_{\mathbf{SC}}$
of high-level nets for which we adapt the algorithm for constructing finite
and complete prefixes of the symbolic unfolding.

######  Definition 4.3 (Class $\mathbf{N}_{\mathbf{SC}}$)

A finite high-level Petri net $N$ is called _s ymbolically compact_ if it
satisfies (1) and (2) from Def. 2.2, and

  * (3@itemi)

There is a bound $n\in\mathbb{N}$ on the number of transition firings needed
to reach all markings in $\mathcal{R}(N)$.

We denote the class containing all symbolically compact high-level Petri nets
by $\mathbf{N}_{\mathbf{SC}}$.

Note that in the case of a (finite, safe) P/T net, property (3*) is equivalent
to (3) (i.e., $|\mathcal{R}(N)|<\infty$). However, this is _not_ true for all
high-level nets $N$: while $|\mathcal{R}(N)|<\infty$ still implies (3*)
(meaning $\mathbf{N}_{\mathbf{F}}\subseteq\mathbf{N}_{\mathbf{SC}}$), the
reverse implication does not hold, as our running example from Figure 1(a)
demonstrates when we change the set of colors to $\mathit{Col}=\mathbb{N}$: it
then still satisfies (1) and (2), with
$\mathcal{R}(N)=\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}(a,0),(b,0)\mathclose{\,{|}\;\\!\\!\\!{\\}}},\mathopen{{\\{}\;\\!\\!\\!{|}\,}\mathclose{\,{|}\;\\!\\!\\!{\\}}}\\}\cup\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}(c,n),(b,0)\mathclose{\,{|}\;\\!\\!\\!{\\}}},\mathopen{{\\{}\;\\!\\!\\!{|}\,}(a,0),(d,n^{\prime})\mathclose{\,{|}\;\\!\\!\\!{\\}}},\allowbreak\mathopen{{\\{}\;\\!\\!\\!{|}\,}(c,n),(d,n^{\prime})\mathclose{\,{|}\;\\!\\!\\!{\\}}}\,\mid\,n,n^{\prime}\in\mathbb{N}\\}.$
So we have infinitely many markings that can all be reached by firing at most
two transitions, meaning the net satisfies (3*) and is therefore symbolically
compact.

Lemma 4.1 implies that the class $\mathbf{N}_{\mathbf{SC}}$ of symbolically
compact nets contains exactly all high-level Petri nets satisfying (1) and (2)
for which a finite and complete prefix of the symbolic unfolding exists
(independently of whether the number of reachable markings is finite). Since
the reachable markings of a high-level Petri net and its expansion correspond
to each other, this observation leads to an interesting subclass
$\mathbf{N}_{\mathbf{SC}}\setminus\mathbf{N}_{\mathbf{F}}$ of symbolically
compact high-level Petri nets that have infinitely many reachable markings.
For every net $N$ in this subclass

  * •

there exists a finite and complete prefix of $\varUpsilon(N)$, but

  * •

there does _not_ exist a finite and complete prefix of
$\varUpsilon(\operatorname{Exp}(N))$.

In particular, the original ERV-algorithm cannot be applied to
$\operatorname{Exp}(N)$, since the expansion is an infinite net.

An example for such a net is our running example from Figure 1(a) when we
replace the color class $\mathit{Col}=\\{0,1,\dots,m\\}$ by
$\mathit{Col}=\mathbb{N}$. Much simpler is the following net, also with
$\mathit{Col}=\mathbb{N}$:

Obviously, every reachable marking
$\mathopen{{\\{}\;\\!\\!\\!{|}\,}(p,n)\mathclose{\,{|}\;\\!\\!\\!{\\}}}$ with
$n\in\mathbb{N}$ can be reached by firing $t$ one time in mode $\\{x\leftarrow
0,y\leftarrow n\\}$, so the net is symbolically compact. The expansion of this
net however is infinite, and the original ERV-algorithm does not terminate
when applied to it.

###  4.2 Insufficiency of the Cut-off Criterion for $\mathbf{N}_{\mathbf{SC}}$

Naturally, the question arises whether the generalized ERV-Algorithm, Alg. 1,
also yields a finite and complete prefix of a symbolically compact input net.
For many examples (like the simple one above) this is the case. However, there
are symbolically compact high-level Petri nets for which Alg. 1 does _not_
terminate.

(a) A symbolically compact net with $\mathit{Col}=\mathbb{N}$.

(b) A prefix of the symbolic unfolding of the net in 4(a).

Figure 4: A symbolically compact net in 4(a) where Alg. 1, trying to build a
complete finite prefix of the symbolic unfolding shown in 4(b), does not
terminate.

The criterion such a net must satisfy is that in the unfolding, there is an
infinite sequence of cone configurations $[e_{1}],[e_{2}],\dots$ with
$[e_{1}]\prec[e_{2}]\prec\dots$ such that

  * •

$\forall i\,\exists K\in\mathcal{K}([e_{i}]):K[e_{i+1}\rangle$, i.e.,
$(e_{1},e_{2},\dots)$ is a fireable sequence in the symbolic unfolding,

  * •

$\forall
i:\mathcal{M}([e_{i}])\not\subseteq\bigcup_{[e^{\prime}]\prec[e_{i}]}\mathcal{M}([e^{\prime}])$,
i.e., no event $e_{i}$ is a cut-off event.

Note that in the second condition, there the $e^{\prime}$ in the union are are
abitrary events in the unfolding, and not restricted to the sequence
$(e_{1},e_{2},\dots)$. An example for such a net is shown in Figure 4(a):

The set of colors is given by $\mathit{Col}=\mathbb{N}$. Initially there is a
token $0$ in each of the places $a$ and $c$. The token on $a$ can cycle
between $a$ and $b$ by transitions $\alpha$ and $\beta$. Analogously, the
other token can cycle between $c$ and $d$ by $\gamma$ and $\delta$.
Additionally, in the inital marking, there is a color $1$ on place $p$. This
number can be increased by $1$ by firing $t$. Thus, every number $n$ can be
placed on $p$ by $n-1$ firings of $t$. When, however, the two cycling tokens
of color $0$ are on places $b$ and $d$, an arbitrary number $n$ can be placed
directly on $p$ by firing $\varepsilon$. The net therefore is symbolically
compact.

Examine now the unfolding in Figure 4(b). Cut-off events and their output
conditions are again shaded blue. For a cleaner presentation do not write the
local predicate next to each event. For the event $\varepsilon^{\prime}$ we
have
$\mathcal{M}([\varepsilon^{\prime}])=\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}(b,0),(d,0),(p,n)\mathclose{\,{|}\;\\!\\!\\!{\\}}}\,\mid\,n\in\mathbb{N}\\}$.
This means by firing no event, only $\beta^{\prime\prime}$, only
$\delta^{\prime\prime}$, or both $\beta^{\prime\prime}$ and
$\delta^{\prime\prime}$ from the corresponding cut, we can represent every
reachable marking in the net.

The sequence $[t^{1}],[t^{2}],\dots$ of cone configurations, with the
corresponding events shaded orange, now satisfies the criterion from above:
The first condition is obviously satisfied. The sequence of events corresponds
to firing $t$ infinitely often, always increasing the number on $p$ by $1$.
The cones $[t^{i}]$ are the only cone configurations where the cuts represent
markings with _no tokens_ on the two places $b$ and $d$. For all other cones
in the unfolding, there is a $0$ on $b$ and/or a $0$ on $d$. Thus, no event
$t^{i}$ is a cut-off event. This means if Alg. 1 is applied to the net in
Figure 4(a) it does not terminate, building a prefix containing every $t^{i}$
with $i\in\mathbb{N}^{+}$.

###  4.3 The Finite Prefix Algorithm for Symbolically Compact Nets

As previously discussed, the argument that states the existence of one event
in a chain of $|\mathcal{R}(N)|+1$ consecutive events, such that every marking
represented by its cone configuration is contained in the union of all
markings represented by previous cone configurations, cannot be applied in the
case of an infinite number of reachable markings. Consequently, Alg. 1 may not
terminate when applied to a net in
$\mathbf{N}_{\mathbf{SC}}\setminus\mathbf{N}_{\mathbf{F}}$. However, condition
(3*) guarantees that every marking reached by a cone configuration $[e]$ with
depth $>n$ can be reached by a configuration $C$ containing no more than $n$
events.

For the algorithm to terminate, we need to adjust the cut-off criterion since
we do not know whether $C$ is also a cone configuration, as demanded in Def.
2.9. Therefore, we define _cut-off* events_ , that generalize cut-off events.
They only require that every marking in $\mathcal{M}([e])$ has been observed
in a set $\mathcal{M}(C)$ for _any_ configuration $C\prec[e]$, rather than
just considering cone configurations:

######  Definition 4.4 (Cut-off* event)

Under the assumptions of Def. 2.9, the high-level event $e$ is a _cut-off*_
event (w.r.t. $\prec$) if
$\mathcal{M}([e])\subseteq\bigcup_{C\prec[e]}\mathcal{M}(C).$

We additionally assume that the used adequate order satisfies
$|C_{1}|<|C_{2}|\Rightarrow C_{1}\prec C_{2}$, so that every event with depth
$>n$ will be a cut-off event. Since all adequate orders discussed in [8]
satisfy this this property (cp. App. A.1), this is a reasonable requirement.
This adaption and assumption now lead to:

###### Theorem 4.5

Assume a given adequate order $\prec$ to satisfy
$|C_{1}|<|C_{2}|\Rightarrow{C_{1}\prec C_{2}}$. When replacing in Alg. 1 the
term “cut-off event” by “cut-off* event”, it terminates for any input net
$N\in\mathbf{N}_{\mathbf{SC}}$, and generates a complete finite prefix of
$\varUpsilon(N)$.

###### Proof 4.6

The properties of symbolic unfoldings that we stated in Sec. 1.3 are
independent on the class of high-level nets. Def. 2.3 only uses that the
considered net is safe, and so do Prop. 2.4 and Prop. 2.7. We therefore only
have to check that the correctness proof for the algorithm still holds. In the
proof of Prop. 2.12 ($\mathit{Fin}$ is finite), the steps (2) and (3) are
independent of the used cut-off criterion. In step (1), however, it is shown
that the depth of events never exceeds $|\mathcal{R}(N)|+1$. This is not
applicable when $|\mathcal{R}(N)|=\infty$, as argued above. Instead we show:

  * (1@itemi)

For every event $e$ of $\mathit{Fin}$, $0pt(e)\leq n+1$, where $n$ is the
bound on the number of transitions needed to reach all markings in
$\mathcal{R}(N)$.

In the proof of Prop. 2.14, the cut-off criterion is used to show (by an
infinite descent approach), for any marking $M\in\mathcal{R}(N)$ the existence
of a minimal configuration $C\in\mathit{Fin}$ with $M\in\mathcal{M}(C)$. Due
to the similarity of cut-off and cut-off*, this proof can easily be adapted to
work as before:

Assume that at some point during the algorithm, we reach a state
$(B^{\prime},E^{\prime},H^{\prime},\iota^{\prime},\mathcal{K}_{0}^{\prime})$
of the prefix under construction, such that there occurs a chain of events
$e_{1}<e_{2}<\dots<e_{n+1}$. We prove that $e_{n+1}$ must be a cut-off* event.
Let $M\in\mathcal{M}([e_{n+1}])$. Then, by definition of
$\mathbf{N}_{\mathbf{SC}}$, $M$ can be reached by firing at most $n$
transitions. Accordingly, from Prop. 1.8, we get that there is a configuration
$C\in\varUpsilon$ containing at most $n$ events such that
$M\in\mathcal{M}(C)$. As in the proof of Prop. 2.14, we can now follow that
there is a configuration $\widetilde{C}\in\mathcal{C}(\varUpsilon)$ such that
$M\in\mathcal{M}(\widetilde{C})$ and $\widetilde{C}\prec C$, that contains no
cut-off event and is therefore in $\mathit{Fin}$. Since $|C|\leq
n<n+1\leq|[e_{n+1}]|$, we follow $\widetilde{C}\prec[e_{n+1}]$. So we have
that $\forall M\in\mathcal{M}([e_{n+1}])\,\exists\widetilde{C}\prec[e_{n+1}]$,
which means that $e_{n+1}$ is a cut-off* event. This proves that
$\mathit{Fin}$ is finite.

The only thing remaining to show is termination. In the case of nets in
$\mathbf{N}_{\mathbf{F}}$, every object is finite, which, together with Prop.
2.12, leads to termination of the algorithm. For nets in
$\mathbf{N}_{\mathbf{SC}}\setminus\mathbf{N}_{\mathbf{F}}$, however, there is
at least one event $e$ in $\mathit{Fin}$ s.t. $|\mathcal{M}([e])|=\infty$.
Thus, we have to show that we can check the cut-off* criterion in finite time.
This follows from Cor. 5.6 in the next section, which is dedicated to
symbolically representing markings generated by configurations.

###  4.4 Feasibility of Symbolically Compact Nets and Cut-Off*

To check the cut-off* criterion of an event added to a prefix of the
unfolding, we have to compare the set of markings represented by the cut of
the event’s cone configuration to _all_ markings represented by cuts of
smaller configurations. This means that we possibly have to store the whole
state space.

This realization gives rise to two questions. Firstly, how do we manage the
storage of an infinite number of markings? This query is addressed in Sec.5,
where we demonstrate how to symbolically represent the markings represented by
a configuration’s cut and how to check the cut-off* criterion within finite
time. The prototype implementation outlined in Sec.6.1 utilizes these methods
for the $\mathbf{N}_{\mathbf{F}}$-case.

The second question that arises asks how the complete finite prefix resulting
from the generalized ERV-algorithm with the cut-off* criterion relates to a
reachability graph – both in terms of size and computation time. However, as
symbolically compact nets possibly have an infinite expansion, the
reachability graph of such a net may not exist. This implies that at present,
this method provides a more viable solution compared to having no method at
all. However, we give an outlook on how a symbolic reachability tree of a
symbolically compact net could possibly be constructed.

##### Outlook: Symbolic Reachability Trees of Symbolically Compact Nets.

The idea of a symbolic reachability tree has been realized for algebraic Petri
nets in [18] by Karsten Wolf. However, in contrast to this work, we think that
for the class of symbolically compact nets we can build a symbolic
reachability tree that is complete.

The idea is to gradually extend for every subset $P^{\prime}$ of places a
formula $\mathcal{R}_{P^{\prime}}$ that symbolically describes all reachable
markings that we have seen so far and have colors on exactly all places in
$P^{\prime}$. Initially, all formulae are $\mathit{false}$, except for
$\mathcal{R}_{P_{0}}$, where $P_{0}$ are the initially marked places.
$\mathcal{R}_{P_{0}}$ symbolically represents the set of initial markings.

The symbolic reachability tree is then constructed by starting with a root
$n_{0}$ labeled with $f_{n_{0}}=\mathcal{R}_{P_{0}}$ representing the set of
initial markings. For every transition $t$, we can determine whether $t$ can
fire in any mode from any marking represented by $f_{n_{0}}$ by a
satisfiability check. If $t$ can fire, we add a new node $n^{\prime}$, and
label it with a formula $f^{\prime}$ that symbolically represents all markings
reached from firing $t$ in any mode from any marking in $\mathcal{M}_{0}$. In
all these markings, there are colors on the same set of places $P^{\prime}$.
If $f^{\prime}\Rightarrow\mathcal{R}_{P^{\prime}}$ then we end this branch. We
then extend $\mathcal{R}_{P^{\prime}}$ to $\mathcal{R}_{P^{\prime}}\lor
f^{\prime}$.

By repeating this procedure in breadth-first order, we build a tree that
symbolically represents all reachable markings. This tree should correspond to
the complete finite prefix of the symbolic unfolding of the net to which you
added a shared resource (in form of a new place) that every transition
consumes and recreates. This makes the system sequential without changing the
sequential semantics. We give here only the idea of the tree, and not a formal
definition. In future work we want to further investigate on this idea. We can
then compare the complete finite prefix of the symbolic unfolding to the
symbolic reachability tree.

##  5 Checking Cut-offs Symbolically

We show how to check whether a high-level event $e$ is a cut-off* event
symbolically in finite time. By definition, this means checking whether
$\mathcal{M}([e])\subseteq\bigcup_{C\prec[e]}\mathcal{M}(C)$. However, since
the cut of a configuration can represent infinitely many markings, we cannot
simply store the set $\mathcal{M}(C)$ for every
$C\in\mathcal{C}(\mathit{Fin})$. Instead, we now define constraints that
symbolically describe the markings represented by a configuration’s cut.
Checking the inclusion above then reduces to checking an implication of these
constraints. Since we consider high-level Petri nets with guards written in a
decidable first order theory, such implications can be checked in finite time.

At the end we see that this method can be easily adapted to symbolically check
whether, in a prefix of the symbolic unfolding of a net
$N\in\mathbf{N}_{\mathbf{F}}$, an event $e$ is a cut-off event in the sense of
Def. 2.9. This method is also used in the implementation described in Sec.
6.1.

For the rest of this section, let
$N=(P,T,F,\iota,\mathcal{M}_{0})\in\mathbf{N}_{\mathbf{SC}}$ with symbolic
unfolding $\varUpsilon=(U,\pi)=(B,E,H,\iota,\mathcal{K}_{0},\pi)$.

We first define for every condition $b$ a new predicate
$\mathit{pred}^{\odot}(b)$ by

$\mathit{pred}^{\odot}({b}):=\mathit{pred}({\mathbf{e}(b)})\land(\pi(b)=\mathbf{v}_{\mathbf{e}}(b)).$

This predicate now has (in an abuse of notation) an extra variable, called
$\pi(b)$. The remaining variables in $\mathit{pred}({\mathbf{e}(b)})$ are
$\mathit{Var}_{[\mathbf{e}(b)]\cup\\{\bot\\}}$. As we know,
$\mathit{pred}({\mathbf{e}(b)})$ evaluates to $\mathit{true}$ under an
assignment
$\theta:\mathit{Var}_{[\mathbf{e}(b)]\cup\\{\bot\\}}\to\mathit{Col}$ if and
only if a concurrent execution of $[\mathbf{e}(b)]$ with the assigned modes is
possible (i.e., under every instantiation of $[\mathbf{e}(b)]$). In such an
execution, $\theta(\mathbf{v}_{\mathbf{e}}(b))\in\mathit{Col}$ is placed on
$b$. The predicate $\mathit{pred}^{\odot}({b})$ therefore can only be true if
$\pi(b)$ is assigned a color that can be placed on $b$.

For a co-set $B^{\prime}\subseteq B$ of high-level conditions, the constraint
on $B^{\prime}$ is an expression with free variables
$\pi(B^{\prime})=\\{\pi(b)\,\mid\,b\in B^{\prime}\\}$ describing which color
combinations can lie on the places represented by the high-level conditions.
We build the conjunction over all predicates $\mathit{pred}^{\odot}(b)$ for
$b\in B^{\prime}$ and quantify over all appearing variables $v_{e}$: the
_constraint on $B^{\prime}$_ is defined by

$\kappa(B^{\prime}):=\exists_{\bigcup_{b\in
B^{\prime}}\mathit{Var}_{[\mathbf{e}(b)]\cup\\{\bot\\}}}:\bigwedge_{b\in
B^{\prime}}\mathit{pred}^{\odot}({b}),$

We denote by $\Xi(B^{\prime})$ the set of variable assignments
$\vartheta:\pi(B^{\prime})\to\mathit{Col}$ that satisfy
$\kappa(B^{\prime})[\vartheta]\equiv\mathit{true}$.

For a configuration $C$, we have that $B^{\prime}=\operatorname{cut}(C)$ is a
co-set, $\pi(B^{\prime})=\pi(\operatorname{cut}(C))$ describes the set of
places occupied in every marking in $\mathcal{M}(C)$. Note that in this case,
we have
$\bigcup_{b\in\operatorname{cut}(C)}\mathit{Var}_{[\mathbf{e}(b)]}=\mathit{Var}_{C}$,
i.e., the bounded variables in $\kappa(\operatorname{cut}(C))$ are exactly the
variables appearing in predicates in $C$. For every instantiation $\theta$ of
$C$ we define a variable assignment
$\vartheta_{\theta}:\pi(\operatorname{cut}(C))\to\mathit{Col}$ by setting
$\forall\pi(b)\in\pi(\operatorname{cut}(C)):\vartheta_{\theta}(b)=\theta(\mathbf{v}_{\mathbf{e}}(b))$.
Instantiations of a configuration and the constraint on its cut are now
related as follows.

###### Lemma 5.1

Let $C\in\mathcal{C}(\varUpsilon)$. Then
$\Xi(\operatorname{cut}(C))=\\{\vartheta_{\theta}\,\mid\,\theta\in\Theta(C)\\}$.

###### Proof 5.2

The proof follows by construction of $\mathit{pred}^{\odot}$ and
$\vartheta_{\theta}$: Let $\vartheta\in\Xi(\operatorname{cut}(C))$. Then
$\mathit{true}\equiv\kappa(\operatorname{cut}(C))[\vartheta]$. Thus, there
exists $\theta:\mathit{Var}_{C\cup\\{\bot\\}}\to\mathit{Col}$ s.t.
$\big{(}\bigwedge_{b\in\operatorname{cut}(C)}\mathit{pred}^{\odot}({b})\big{)}[\vartheta][\theta]\equiv\mathit{true}$
and therefore

$\displaystyle\Big{(}\bigwedge_{b\in\operatorname{cut}(C)}\mathit{pred}(\mathbf{e}({b}))[\theta]\Big{)}\
\land\
\Big{(}\bigwedge_{b\in\operatorname{cut}(C)}\vartheta(\pi(b))=\theta(\mathbf{v}_{\mathbf{e}}(b))\Big{)}\quad$
$\displaystyle\equiv\quad\mathit{true}.$ (1)

From the inductive definition of $\mathit{pred}$ then follows that $\forall
e\in C\cup\\{\bot\\}:\mathit{pred}({e})[\theta]\equiv\mathit{true}$. Thus,
$\theta$ is an instantiation of $C$, and $\vartheta_{\theta}=\vartheta$, as
shown by the posterior conjunction in (1).

Let on the other hand $\theta\in\Theta(\operatorname{cut}(C))$. Then directly,
by the definition of $\mathit{pred}^{\odot}(b)$ and $\vartheta_{\theta}$, we
get
$\big{(}\bigwedge_{b\in\operatorname{cut}(C)}\mathit{pred}^{\odot}({b})\big{)}[\vartheta_{\theta}][\theta]\equiv\mathit{true}$
and by the definition of $\kappa(\operatorname{cut}(C))$ that
$\kappa(\operatorname{cut}(C))[\vartheta_{\theta}]\equiv\mathit{true}$, i.e.,
$\vartheta_{\theta}\in\Xi(\operatorname{cut}(C))$.

From the definition of $\mathcal{K}(C)$ and $\mathcal{M}(C)$ we get:

###### Corollary 5.3

Let $C\in\mathcal{C}(\varUpsilon)$. Then
$\mathcal{K}(C)=\\{\\{(b,\vartheta(\pi(b)))\,\mid\,b\in\operatorname{cut}(C)\\}\,\mid\,\vartheta\in\Xi(\operatorname{cut}(C))\\}$
and
$\mathcal{M}(C)=\\{\mathopen{{\\{}\;\\!\\!\\!{|}\,}(\pi(b),\vartheta(\pi(b)))\,\mid\,b\in\operatorname{cut}(C)\mathclose{\,{|}\;\\!\\!\\!{\\}}}\,\mid\,\vartheta\in\Xi(\operatorname{cut}(C))\\}$.

We now show how to check whether an event is a cut-off* event via the
constraints defined above. For that, we first look at general configurations
in Theorem 5.4, and then explicitly apply this result to cone configurations
$[e]$ in Cor. 5.6.

###### Theorem 5.4

Let $C,C_{1},\dots,C_{n}$ be finite configurations in the symbolic unfolding
of a safe high-level Petri net s.t. $\forall 1\leq i\leq
n:\pi(\operatorname{cut}(C))=\pi(\operatorname{cut}(C_{i}))$. Then

$\mathcal{M}(C)\subseteq\bigcup_{i=1}^{n}\mathcal{M}(C_{i})\quad\text{if and
only
if}\quad\kappa(\operatorname{cut}(C))\Rightarrow\bigvee_{i=1}^{n}\kappa(\operatorname{cut}(C_{i})).$

###### Proof 5.5

Assume $\mathcal{M}(C)\subseteq\bigcup_{i=1}^{n}\mathcal{M}(C_{i})$ and let
$\vartheta\in\Xi(\operatorname{cut}(C))$. We have that
$M_{\vartheta}:=\\{(\pi(b),\vartheta(\pi(b)))\,\mid\,b\in\operatorname{cut}(C)\\}\in\mathcal{M}(C)$
by Cor. 5.3. Thus, $\exists 1\leq i\leq n:M_{\vartheta}\in\mathcal{M}(C_{i})$.
This, again by Cor. 5.3, means
$\exists\vartheta_{i}\in\Xi(\operatorname{cut}(C_{i})):$

$M_{\vartheta}=\\{(\pi(b^{\prime}),\vartheta_{i}(\pi(b^{\prime})))\,\mid\,b^{\prime}\in\operatorname{cut}(C_{i})\\}$

This shows that $\vartheta=\vartheta_{i}$. Thus,
$\kappa(\operatorname{cut}(C_{i}))[\vartheta]\equiv\mathit{true}$, which
proves the implication.

Assume on the other hand
$\kappa(\operatorname{cut}(C))\Rightarrow\bigvee_{i=1}^{n}\kappa(\operatorname{cut}(C_{i}))$.
Let $M\in\mathcal{M}(C)$. Then
$\exists\vartheta\in\Xi(\operatorname{cut}(C)):M=\\{(\pi(b),\vartheta(\pi(b)))\,\mid\,b\in\operatorname{cut}(C)\\}$.
Thus, ${\exists 1\leq i\leq
n}:\kappa(\operatorname{cut}(C_{i}))[\vartheta]\equiv\mathit{true}$. Let
$\vartheta_{i}=\vartheta$. Then
$\vartheta_{i}\in\Xi(\operatorname{cut}(C_{i}))$, and
$M=\\{(\pi(b^{\prime}),\vartheta_{i}(\pi(b^{\prime})))\,\mid\,b^{\prime}\in\operatorname{cut}(C_{i})\\}\in\mathcal{M}(C_{i})$,
which completes the proof.

The following Corollary now gives us a characterization of cut-off* events in
a symbolic branching process. It follows from Theorem 5.4 together with the
facts that
$\mathcal{M}(C_{1})\cap\mathcal{M}(C_{2})\neq\emptyset\Rightarrow\pi(\operatorname{cut}(C_{1}))=\pi(\operatorname{cut}(C_{2}))$,
and that ${{\prec}[e]}$ is finite.

###### Corollary 5.6

Let $\beta$ be a symbolic branching process and $e$ an event in $\beta$. Then
$e$ is a cut-off* event in $\beta$ if and only if

$\kappa(\operatorname{cut}([e]))\Rightarrow\bigvee_{\begin{subarray}{c}C\prec[e]\\\
h(\operatorname{cut}(C))=h(\operatorname{cut}([e]))\end{subarray}}\kappa(\operatorname{cut}(C)).$

Thus, we showed how to decide for any event $e$ added to a prefix of the
unfolding whether it is a cut-off* event, namely, by checking the above
implication in Cor. 5.6. Note that we can also check whether $e$ is a _cut-
off_ event (w.r.t. Def. 2.9) by the implication in Cor. 5.6 when we replace
all occurrences of “$C$” by “$[e^{\prime}]$” .

##  6 Implementation and Experimental Results

In this section, we delve into the implementation details of the generalized
ERV-algorithm and discuss the results of our experiments. We give a concise
overview of the technical decisions made during implementation and provide an
evaluation of its performance across four novel benchmark families. We
identify a property called “mode determinism” that offers a heuristic for
determining whether it is faster to construct (a complete finite prefix of)
the symbolic unfolding or the low-level unfolding.

###  6.1 Implementation Specifics

Other tools designed for generating (prefixes of) P/T Petri net unfoldings
include Mole [19], Cunf [20, 21], and Punf [22]. However, as these tools are
specifically optimized for their intended purpose and do not cater to high-
level Petri nets, we opted not to integrate the new algorithms into any of
these frameworks. Furthermore, we refrain from conducting a speed comparison
between our implementation and the aforementioned tools. The objective of
Section 6 is to provide a comparison between two approaches: calculating a
respective complete finite prefix of the low-level or the symbolic unfolding.

We have devised a prototype implementation called _ColorUnfolder_ [23] written
in the Java programming language. It serves a dual purpose as an
implementation of the low-level approach as a base for comparisons on a level-
playing field and the novel symbolic approach. It can calculate a finite
complete prefix of the low-level unfolding for a given high-level Petri net,
combining the concepts from [8] (complete finite prefixes) and [9] (generating
the low-level unfolding without expansion). Additionally, it is capable of
computing a complete finite prefix of the net’s symbolic unfolding, utilizing
a modified version of Alg. 1. Since we want to compare the low-level with the
high-level case, we restricted ourselves to nets from the class
$\mathbf{N}_{\mathbf{F}}$ to guarantee that the low-level unfolding exists.

Both, the generalized (Alg. 1) and the original ([8]) ERV-algorithm create
possible extensions that are structurally dependent cut-off events, whereas in
the implementation a cut-off event never triggers the calculation of possible
extension. With the same idea, conditions in the postset of cut-off events are
never considered for finding co-sets. This leaves the finite complete prefix
unmodified, as it only eliminates unnecessary work.

More importantly, the tool operates on a modified unfolding since an
implementation using the predicates defined here turned out to be very slow.
It rewrites the predicates in the unfolding and modifies arc labels to
drastically reduce the number of variables. After a finite complete prefix of
the modified unfolding is found, the result is transformed into the expected
result with barely any overhead. The underlying idea is to reuse the same
variable in the unfolding for as long as the tokens represented by it in
firing modes have the same color. For example, in the unfolding from Figure
2(b), ColorUnfolder replaces the four variables by a single variable.

This optimization yields a significant speed up. However, when working on the
symbolic unfolding, in our experiments still more than 99 percent of the time
is spent evaluating the satisfiability of predicates to identify cut-off
events using Cor. 5.6, and to detect when to discard event candidates because
of a color conflict. For this task we chose the _cvc5_ SMT solver [24]. It
performed best in the relevant category (non-linear arithmetic with equality
and quantifiers) of the Satisfiability Modulo Theories Competition (SMT-COMP
2023)222 https://smt-comp.github.io/2023/results/equality-nonlineararith-
single-query.

###  6.2 Benchmark Families

In this section, we present four new benchmark families on which we tested the
calculation of the symbolic unfolding and compared it to the calculation of
the low-level unfolding.

####  6.2.1 Fork And Join

The most simple of our benchmark families is called _Fork And Join_. In the
initial marking, a token lies on place $p_{0}$. A transition $t$ takes this
token from $p$ and places an arbitrary color on each of its output places. A
transition $\varepsilon$ then takes these colors from all places, ending the
nets execution. We have two parameters: the first parameter, $m\in\mathbb{N}$,
determines the set of colors $\mathit{Col}=\\{0,\dots,m\\}$. The second
parameter, $n\in\mathbb{N}$, determines the number of output places of $t$.
Fig. 5 shows the independent diamonds for $n=2$ in 5(a) and for $n=4$ in 5(b).

(a) $n=2$.

(b) $n=4$.

Figure 5: Fork And Join for $n=2$ in 5(a) and $n=4$ in 5(b).

The symbolic unfolding of a Fork And Join has $n+3$ nodes as it is
structurally equal to the net itself. The low-level unfolding of the expansion
has $(n+2)(m+1)^{n}+1$ nodes (since $t$ is fireable in $(m+1)^{n}$ modes), cp.
App. A.2.

####  6.2.2 The Water Pouring Puzzle

This benchmark family generalizes a classic logic puzzle (cf., e.g., [25])
which goes as follows:

> “You have an infinite supply of water and two buckets. One holds 5 liters,
> the other holds 3 liters. Measure exactly 4 liters of water in one bucket.”

In our generalization we have two parameters. The first parameter is a finite
list $n=[n_{1},\dots,n_{k}]$ of natural numbers. Each entry $n_{i}$ represents
an available bucket holding $n_{i}$ liters. The second parameter,
$m\in\mathbb{N}$ is the amount of water that should be measured.

Figure 6: The Water Pouring Puzzle with 2 buckets, where one can hold 5 liters
and the other can hold 3 liters.

Fig. 6 shows the high-level Petri net corresponding to the parameters
$n=[3,5]$ and $m=4$, corresponding to the puzzle above. Independently of the
parameters, we have $\mathit{Col}=\mathbb{N}$. The current fill level of each
bucket $i$ is represented by a place $\mathit{bucket}$-$i$, with an initial
color $0$, and two attached transitions $\mathit{fill}$-$i$ and
$\mathit{empty}$-$i$, that, when fired, replace the color on
$\mathit{bucket}$-$i$ by $n_{i}$ or $0$, respectively. Additionally, for each
pair of buckets $i,j$, there are two transitions $i$-$\mathit{transfer}$-$j$
and $j$-$\mathit{transfer}$-$i$ that transfer as much water as possible from
one bucket to the other without overflowing it. When at least one bucket
contains $m$ liters, the goal transition can fire. We include a prefix the
symbolic unfolding of the net from Fig. 6 in App. A.2.

####  6.2.3 Hobbits And Orcs

The _Hobbits And Orcs_ problem333The problem is also known as “Missionaries
and Cannibals”, and is a variation of the “Jealous Husbands” problem. is
another logic puzzle (in particular one of many “river crossing problems”,
cf., e.g., [26, 27]) and goes as follows:

> “Three Hobbits and three Orcs must cross a river using a boat which can
> carry at most two passengers. For both river banks, if there are Hobbits
> present on the bank, they cannot be outnumbered by orcs (if they were, the
> Orcs would attack the Hobbits). The boat cannot cross the river by itself
> with no one on board.”

We generalize this problem by introducing two parameters. The first parameter,
$m\in\mathbb{N}$ is the number of both Hobbits and Orcs. We always have
equally many of the two parties. The second parameter, $n\in\mathbb{N}$ is the
number of passengers the boat can carry. We additionally assume that also on
the boat, if there are Hobbits present, they cannot be outnumbered by Orcs.

(a) An illustration of the “Hobbits And Orcs” problem.555The "Boat" icon used
in Figure 5 is by DinosoftLabs from Noun Project,
https://thenounproject.com/dinosoftlab/.

(b) The problem modeled as a high-level Petri net.

Figure 7: The Hobbits And Orcs problem with 3 Hobbits, 3 Orcs, and a boat
fitting 2 passengers.

Figure 5 shows an illustration of the original puzzle presented above, with
three of both, Hobbits and Orcs, and a boat fitting two passengers. Figure
7(b) shows the corresponding high-level Petri game. The colors are given by
$\mathit{Col}=\mathbb{N}\times\mathbb{N}$, where a tuples describes the number
of Hobbits and Orcs at a location – the left bank, the boat, or the right
bank. We start with three Hobbits and three Orcs on the left bank, indicated
by the tuple $(3,3)$ on the place $\operatorname{\mathit{bank-\ell}}$. The
four center places describe the current state of the boat, being either empty
and docked on a bank, or loaded and on the river. Initially, there is a tuple
$(0,0)$ on $\operatorname{\mathit{docked-\ell}}$, indicating an empty boat the
left bank. Via the transitions $\mathit{load}$ and $\mathit{unload}$ left and
right, the boat can be loaded or unloaded, with the guards ensuring all the
conditions from the riddle regarding the number of Hobbits and Orcs on both
banks and on the boat. When all creatures are on the right bank, the goal
transition can fire, ending the net’s execution.

####  6.2.4 Mastermind

The last benchmark family models a generalization of the classic code-breaking
game _Mastermind_ developed in the early Seventies and completely solved in
1993 [28, 29]. The game is played between two players. The _code maker_
secretly chooses an ordered, four digit color code, with six available colors.
The _code breaker_ then guesses the code. The code maker evaluates the guess
by a number of _red pins_ indicating how many colors in the guess are in the
correct position, and a number of _white pins_ indicating how many colors in
the guess appear at a different position in the code.

Figure 8: The Mastermind game with a code of length 4, 6 possible colors, and
12 attempts.

Using this knowledge, the code breaker makes the next guess, with up to twelve
attempts.

In our generalization we have three parameters. The first parameter,
$m\in\mathbb{N}$, describes the number of available colors. The second
parameter, $n\in\mathbb{N}$, describes the length of the code. The third
parameter, $k\in\mathbb{N}$, describes the number of guesses the code breaker
can make. To simplify the net, we restricted the allowed codes to not contain
any color twice.

Fig. 8 shows the high-level Petri net with $m=6$ available colors, a code of
length $n=4$, and $k=12$ possible attempts, i.e., the scenario described
above. The code maker places one color on each of the four places
$\mathit{code}$-$\mathit{i}$ by firing $\mathit{pick}$-$\mathit{code}$.
Transition $\mathit{tuple}$ puts these colors into a tuple on place
$\mathit{code}$. The purpose of this (for the model unimportant) transition is
to make the symbolic unfolding (cp. App. A.2) resemble an actual game board of
Mastermind. The code breaker, analogously to the code maker, concurrently
guesses a code via transition $\mathit{guess}$. Transition $\mathit{evaluate}$
compares this guess to the code and places the result, i.e., the corresponding
number of red and white pins, on $\mathit{result}$. From there, the code
breaker either wins if the guessed code was correct, or resets with transition
$\mathit{retry}$, provided that he has another attempt left.

###  6.3 Mode deterministic High-level Petri nets

In the experiments presented in the next section we identified an important
heuristic for whether it is faster to use the symbolic approach for a finite
complete prefix presented in this paper, or to calculate a complete finite
prefix of the low-level unfolding, combining the concepts of [8] and [9].

The identified net property is that in every reachable marking of $N$, every
transition can fire in at most one node. We call a high-level Petri net with
this property _mode deterministic_ , formally:

###### Definition 6.1

A high-level Petri net $N$ with transitions $T$ is called _mode deterministic_
iff

$\forall M\in\mathcal{R}(N)\,\forall t\in T\,\exists^{\leq
1}\sigma\in\Sigma(t):M[t,\sigma\rangle.$

In the case of a mode deterministic net $N$, the _skeleton_ of $N$’s symbolic
unfolding (essentially, the core structure of the high-level occurrence net,
devoid of arc labels and guards, and interpreted as a P/T Petri net) is
equivalent in structure to the low-level unfolding of $N$’s expansion. This
implies that the high-level abstraction does not offer any computational
advantage in the unfolding process. To the best of our knowledge, this
property has not been studied elsewhere.

An illustrative example of a family of mode deterministic nets is the
benchmark family Water Pouring Puzzle introduced in Sec. 6.2.2. Although this
property may not be immediately apparent, it does hold true that in every
state of the system, all transitions can fire in at most one mode.
Specifically, transitions $\operatorname{\mathit{fill-i}}$ and
$\operatorname{\mathit{fill-i}}$ replace the color on
$\operatorname{\mathit{bucket-i}}$ with a predetermined one. Every transition
$\operatorname{\mathit{i-transfer-j}}$ emulates the transfer of _all_ water
from bucket $i$ that can fit into bucket $j$.

A condition that guarantees $N$ to be a mode deterministic net is as follows:
“For any conceivable assignment of variables on input arcs, there exists at
most one possible mode that completes this assignment to all variables.” The
nets in the Water Pouring Puzzle family fulfill this criterion, since all
output variables ($o$) are either predetermined or derived from the input
variables ($i$).

An example for “highly non mode deterministic” nets is the benchmark family
Fork And Join from Sec. 6.2.1. There are only two transitions in the net, but
from the initial marking, $t$ can fire in _every_ of its $m^{n}$ modes. This
structural pattern of Fork And Join can also be observed in the Mastermind
benchmark family (Sec. 6.2.4), making these nets also _not_ mode
deterministic.

The Hobbits and Orcs family (Sec. 6.2.3), on the other hand, falls in between
and is notably contingent on the parameters involved. When there are only two
seats on the boat, there are merely five _potential_ modes of
$\operatorname{\mathit{load-\ell}}$ from the initial marking (reflecting the
possible ways to occupy one or both seats with two types of creatures).
However, in the scenario where there are $n$ seats on the boat, along with $m$
Hobbits and Orcs, and $m>n$, the total number of possibilities is
$\sum_{i=1}^{n}i+1=\frac{1}{2}n(n+3)$. It’s worth noting that approximately
half of these possibilities would result in more orcs than hobbits on the
boat, rendering them non-modes. Hence, given the condition $m>n$, the “degree”
of mode determinism remains unaffected by an increase in $m$, but solely
varies with the parameter $n$.

In the subsequent section, we empirically validate the hypothesis that the
level of mode determinism is inversely proportional to the benefit gained from
employing symbolic unfolding compared to low-level unfolding.

###  6.4 Experiments and Results

We now present the experimental results of applying our implementation to the
four benchmark families presented above. ColorUnfolder can check the
reachability of a (set of) marking(s) by adding a respective transition to the
net. It then stops when either an instance of this transition is added to the
finite complete prefix under construction, or Alg. 1 terminates without such
an instance.

For the nets from the Fork And Join benchmark family, the complete unfolding
(being its own smallest finite and complete prefix) is calculated. For the
benchmark families Water Pouring Puzzle and Hobbits And Orcs, the reachability
of the goal state of the riddle is checked. This is done by adding the
respective $\mathit{goal}$ transition that is depicted in each of the two
figures Fig. 6 and Fig. 7. This transition is not part of the input net.
Finally, for nets in the Mastermind benchmark family, reachability of a
marking with the result of $n-1$ red pins and $1$ white pin is checked. Such a
marking is never reachable, so always the complete (but finite) unfolding is
calculated.

The above described tasks are checked twice, once using the symbolic unfolding
and once using the low-level unfolding as described in Sec. 6.1. The
experiments are calculated with commit 124b1735 of ColorUnfolder [23] on an
otherwise idle system with an Intel i7-6700K CPU at $4.0$ GHz and $16$ GB RAM.

##### Fork & Join.

The results for Fork & Join are shown in Fig. 9.

In Fig. 9(a), the elapsed time for calculating the low-level unfolding for the
instance with $n$ places (x-axis) and $m$ colors (y-axis) is indicated by the
heatmap intensity of the respective cell. Empty cells exceeded a 5-minute
timeout. We see that the low-level approach is only viable if at least one
parameter is very small. It takes exponentially more time with a growing color
class and with growing number of places.

Since the symbolic approach outperforms the low-level approach by a wide
margin, we present it in its own figure, Fig. 9(b). For all the cases from
Fig. 9(a), the symbolic approach takes around 200 ms to complete the symbolic
unfolding. This is independent of the color class $\\{0,\dots,m\\}$. This
corresponds to the fact that the symbolic unfolding of Fork & Join is, for a
fixed number of places $n$, independent of the color class
$\mathit{Col}=\\{0,\dots,m\\}$. This even does not change for
$\mathit{Col}=\mathbb{N}$. Since cvc5 (the tool used for checking
satisfiability, cp. Sec. 6.1) can handle such infinite color domains, we fix
$\mathit{Col}=\mathbb{N}$, and Fig. 9(b) shows the elapsed time (y-axis) for
calculating the symbolic unfolding of the Fork & Join instance with $n$ places
(x-axis). This approach is very fast (but not linear in the number of places).

The symbolic approach is faster for all choices of the parameters. Only for
the smallest choices are both approaches equally fast within the margin of
error. This behavior was expected since the Petri nets are “highly non mode
deterministic”, as explained above, and the low-level unfolding is much
broader than the symbolic unfolding.

(a) Low-level, for growing number of places on x-axis, color class on y-axis
and time as heatmap intensity.

(b) Symbolic, for growing number of places on x-axis and time on y-axis.
Behavior is independent of the color class. This graph is for
$\mathit{Col}=\mathbb{N}$.

Figure 9: Time needed to calculate unfolding 9(a) and symbolic unfolding 9(b)
of Fork & Join.

##### Water Pouring Puzzle.

For the Water Pouring Puzzle we cannot get interesting results by varying one
parameter while holing the others fixed, because the complexity of the
solution is highly volatile and dependent on the combination of all
parameters. Since the nets are mode deterministic, the low-level and symbolic
unfolding, as well as their prefixes, are isomorphic.

Table 1: Results of the Water Pouring Puzzle benchmark. buckets $n$ | target $m$ | solvable | $|B|$ | $|E|$ | time low-level | time symbolic
---|---|---|---|---|---|---