Nick Würdemann

Thomas Chatain
email: thomas.chatain@inria.fr

Stefan Haar
email: stefan.haar@inria.fr

Lukas Panneke

Taking Complete Finite Prefixes To High Level, Symbolically *

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

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 socalled 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.

Introduction

Petri nets [START_REF] Reisig | Understanding Petri Nets -Modeling Techniques, Analysis Methods[END_REF], also called P/T (for Place/Transition) Petri nets or low-level Petri nets, are a wellestablished formalism for describing distributed systems. High-level Petri nets [START_REF] Jensen | Coloured Petri Nets -Basic Concepts, Analysis Methods and Practical Use -Volume 1, Second Edition[END_REF] (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 1 , 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 [START_REF] Nielsen | Petri Nets, Event Structures and Domains, Part I[END_REF]. Engelfriet generalizes this concept in [START_REF] Engelfriet | Branching Processes of Petri Nets[END_REF] by introducing the notion of branching processes, and shows that the unfolding of a net is its maximal branching process. In [START_REF] Mcmillan | A Technique of State Space Search Based on Unfolding[END_REF], McMillan gives an algorithm to compute a complete finite prefix of the unfolding of a given Petri net. In a well-known paper [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], 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 [START_REF] Khomenko | Branching Processes of High-Level Petri Nets[END_REF], 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 [START_REF] Ehrig | High-Level Net Processes[END_REF], Ehrig et al. define processes of high-level Petri nets, and in [START_REF] Chatain | Symbolic Diagnosis of Partially Observable Concurrent Systems[END_REF], Chatain and Jard define symbolic branching processes and unfoldings of highlevel Petri nets. The work on the latter is built upon in [START_REF] Chatain | Factorization Properties of Symbolic Unfoldings of Colored Petri Nets[END_REF] by Chatain and Fabre, where they consider so-called "puzzle nets". Based on the construction of a symbolic unfolding, in [START_REF] Chatain | Complete Finite Prefixes of Symbolic Unfoldings of Safe Time Petri Nets[END_REF], complete finite prefixes of safe time Petri nets are constructed, using time constraints associated with timed processes. In [START_REF] Chatain | Symbolic Unfoldings of High-Level Petri Nets and Application to Supervision of Distributed Systems[END_REF], 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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] 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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] 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

High-level Petri Nets & Symbolic Unfoldings

In [START_REF] Chatain | Symbolic Diagnosis of Partially Observable Concurrent Systems[END_REF], 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 → N a multi-set over X. We denote x ∈ A if A(x) ≥ 1. For two multi-sets A, A ′ over the same set X, we write A ≤ A ′ iff ∀x ∈ X : A(x) ≤ A ′ (x), and denote by A + A ′ and A -A ′ the multi-sets over X given by (A + A ′ )(x) = A(x) + A ′ (x) and (A-A ′ )(x) = max(A(x)-A ′ (x), 0). We use the notation {| . . . | } as introduced in [START_REF] Khomenko | Branching Processes of High-Level Petri Nets[END_REF]: elements in a multi-set can be listed explicitly as in {| x 1 , x 1 , x 2 | }, which describes the multi-set A with A(x 1 ) = 2, A(x 2 ) = 1, and A(x) = 0 for all x ∈ X \ {x 1 , x 2 }. A multi-set A is finite if there are finitely many x ∈ X such that x ∈ A. In such a case, {| f (x) | x ∈ A | }, with f (x) being an object constructed from x ∈ X, denotes the multi-set A ′ such that A ′ = x∈X A(x) • f (x), where the A(x) • y is the multi-set containing exactly A(x) copies of y.

High-level Petri Nets

A (high-level) net structure is a tuple N = (Col , Var , P, T, F, ι) with the following components: Col and 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 ×Var ×T )∪(T ×Var ×P ) → N. Let Var (t) = {v ∈ Var | ∃p ∈ P : (p, v, t) ∈ F ∨ (t, v, p) ∈ F }. The function ι maps each t ∈ T to a predicate ι(t) on Var (t), called the guard of t. By this, ι(t) can contain other (bounded) variables, but all free variables in ι(t) must appear on arcs to or from t. A marking in N is a multiset M over P × Col , describing how often each color c ∈ Col currently resides on each place p ∈ P . A high-level Petri net N = (N , M 0 ) is a net structure N together with a nonempty set M 0 of initial markings, where we assume ∀M 0 , M ′ 0 ∈ M 0 :

{| p | (p, c) ∈ M 0 | } = {| p | (p, c) ∈ M ′ 0 | }, i.e.
, in all initial markings, the same places are marked with the same number of colors. We often assume the two sets Col of colors and Var of variables to be given. In this case, we denote a high-level net structure (resp. high-level Petri net) by N = (P, T, F, ι) (resp. N = (P, T, F, ι, M 0 )).

For two nodes x, y ∈ P ∪ T , we write x → y, if there exists a variable v such that (x, v, y) ∈ F . The reflexive and irreflexive transitive closures of → are denoted respectively by ≤ and <. For a transition t ∈ T , we denote by pre (t) = {| (p, v) | (p, v, t) ∈ F | } and post (t) = {| (p, v) | (t, v, p) ∈ F | } the preset and postset of t. A firing mode of t is a mapping σ : Var (t) → Col such that ι(t) evaluates to true under the substitution given by σ, denoted by ι(t)[σ] ≡ true. We then denote pre (t, σ) = {| (p, σ(v)) | (p, v) ∈ pre (t) | } and post (t, σ) = {| (p, σ(v)) | (p, v) ∈ post (t) | }. The set of modes of t is denoted by Σ(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 σ from a marking M if M ≥ pre (t, σ), denoted by M [t, σ⟩. This firing leads to a new marking M ′ = (M -pre (t, σ))+post (t, σ), which is denoted by M [t, σ⟩M ′ . We collect in the set R(N , M) the markings reachable by firing a sequence of transitions in N from any marking in a set of markings M. We say 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 Col as its domain of discourse.

Let N = (P, T, F, ι) and N ′ = (P ′ , T ′ , F ′ , ι ′ ) be two net structures with the same sets of colors and variables. A function h : P ∪ T → P ′ ∪ T ′ is called a (high-level Petri net) homomorphism, if: i) it maps places and transitions in N into the corresponding sets in N ′ , i.e., h(P ) ⊆ P ′ and h(T ) ⊆ T ′ ;

ii) it is "compatible" with the guard, preset, and postset, of transitions, i.e., for all t ∈ T we have ι(t) = ι ′ (h(t)) and pre (h(t)) = {| (h(p), v) | (p, v) ∈ pre (t) | } and post (h(t)) = {| (h(p), v) | (p, v) ∈ post (t) | }.

For N = (N , M 0 ) and N ′ = (N ′ , M ′ 0 ), the homomorphisms between N and N ′ are the homomorphisms between N and N ′ . Such a homomorphism h is called initial if additionally {{| (h(p), c) | (p, c) ∈ M 0 | } | M 0 ∈ M 0 } = M ′ 0 holds, i.e., the initial markings in N are mapped to the initial markings in N ′

We define P/T Petri nets as high-level Petri nets with singletons Col = {•} and Var = {v • } for colors and variables, i.e., in a marking, every place holds a number of tokens •, which is the only value ever assigned to the variable v • on every arc. The guard of every transition in a P/T Petri net is true. Example 1.1. Let Col = {0, . . . , m} for a fixed m, and Var = {x, y, z, w} be the given sets of colors and variables. In Figure 1a, 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 = {| (a, 0), (b, 0) | }, 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 • in the P/T case. From M 0 the two transitions α and β can fire, taking the color 0 from place a resp.

a ′ b ′ ⊥ α ′ x α ′ > 0 β ′ x β ′ > 0 c ′ d ′ t ′ x t ′ = x α ′ ∧ y t ′ = x β ′ ∧ y t ′ = 3 • x t ′ ε ′ x ε ′ = x α ′ ∧ y ε ′ = x β ′ ∧z ε ′ , w ε ′ > 0 c ′′ d ′′ t ′′ x t ′′ = z ε ′ ∧ y t ′′ = w ε ′ ∧ y t ′′ = 3 • x t ′′ ε ′′ x ε ′′ = z ε ′ ∧ y ε ′′ = w ε ′ ∧z ε ′′ , w ε ′′ > 0 c ′′′ d ′′′ t ′′′ ε ′′′

Symbolic Branching Processes and Unfoldings

A high-level net structure N = (Col , Var , P, T, F, ι) is called ordinary if there is at most one arc connecting any two nodes in N , i.e., ∀(x, y) ∈ (P × T ) ∪ (T × P ) : v∈Var F (x, v, y) ≤ 1. For such an ordinary net structure, analogously to the well-known low-level case, two nodes x, y ∈ P ∪ T are in structural conflict, denoted by x♯y, if ∃p ∈ P ∃t, t ′ ∈ T :

t ̸ = t ′ ∧ p → t ∧ p → t ′ ∧ t ≤ x ∧ t ′ ≤ y. A high-level occurrence net is a high-level Petri net O = (Col , Var , B, E, H, ι, K 0 )
with an ordinary net structure (Col , Var , B, E, H, ι), where B is a set of conditions (places), E is a set of events (transitions), H is a flow relation, and 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:

i) No event is in structural self-conflict, i.e., ∀e ∈ E : ¬(e♯e).
ii) No node is its own causal predecessor, i.e., ∀x ∈ B ∪ E : ¬(x < x).

iii In a high-level occurrence net, we define for every event e the predicates loc-pred (e) and pred (e). The predicate pred (e) is satisfiable iff e is not dead, i.e., there are cuts K 0 , . . . , K n with K 0 ∈ K 0 and events e 1 , . . . , e n , s.t. K 0 [e 1 ⟩ . . . [e n ⟩K n [e⟩. This predicate is obtained by building a conjunction over all local predicates of events e ′ with e ′ ≤ e, and the predicate of the special event ⊥.

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) ∈ pre (e), the value of the variable v coincides with the color that the event e(b) placed in b. To realize this, the variables v ∈ Var (e) are instantiated For two symbolic branching processes β = (O, h) and

β ′ = (O ′ , h ′ ) of a high-level Petri net, β is a prefix of β ′ if there exists an injective initial homomorphism ϕ from O into O ′ , such that h ′ • ϕ = h.
In [START_REF] Chatain | Symbolic Diagnosis of Partially Observable Concurrent Systems[END_REF] 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 Υ (N ) = (U (N ), π N ). The value of π 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 1a. In Figure 1b we see (a prefix of) the infinite occurrence net U (N ) of the symbolic unfolding Υ (N ). We depict the prefix with two instances of each t and ε. 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" ⊥, 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 α ′ , namely x α ′ > 0 expresses that the assignment of colors to variables by a mode of α ′ must satisfy the constraint given by the guard of its label α. Analogously for β ′ . The same is expressed in the local predicate of t ′ by y t ′ = 3 • x t ′ , coming from the guard y = 3 • x of t. Additionally, the first part of the conjunction formalizes that, since (c ′ , x) ∈ pre (t ′ ), the value that a mode of t ′ assigns to x must be the same that a mode of e(c ′ ) = α ′ assigned to v(c ′ ) = x. This is expressed as x t ′ = x α ′ . The second part of the conjunction formalizes the same for y and d ′ . The whole predicate of t ′ is then given by

pred (t ′ ) = x α ′ > 0 ∧ x β ′ > 0 ∧ x t ′ = x α ′ ∧ y t ′ = x β ′ ∧ y t ′ = 3 • x t ′ .
Since it is satisfiable for example by {x α ′ ← 1, x β ′ ← 3, x t ′ ← 1, y t ′ ← 3} (meaning that t can fire in mode {x ← 1, y ← 3} after α fired in mode {x ← 1} and β fired in mode {x ← 3}), the node t ′ is an event in the unfolding.

The blue shading of event ε ′′ and t ′′ 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 ⊆ E ∪ B and are in color conflict if

e∈X∩E pred (e) ∧ b∈X∩B pred (e(b))
is not satisfiable. The nodes of X are concurrent if they are not in color conflict, and for each x, x ′ ∈ X ′ , neither x < x ′ , nor x ′ < x, nor x♯x ′ 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.

p 0 0 t 0 p 1 p 2 p 3 t 1 x ≤ 0 t 2 x ̸ = 0 t 3 x ≥ 0 p ′ 1 p ′ 2 p ′ 3 x x x x x x x x x (a) A high-level Petri net with Col = Z and Var = {x}. b 0 e 0 b 1 b 2 b 3 e 1 x e1 ≤ 0 ∧ x e1 = x e0 e 2 x e2 ̸ = 0 ∧ x e2 = x e0 e 3 x e3 ≥ 0 ∧ x e3 = x e0 b ′ 1 b ′ 2 b ′ 3 x x x x x x x x x ⊥ (b)
The symbolic unfolding of the net in (a), with the events {e 1 , e 2 , e 3 } in color conflict. In Figure 2a, a high-level Petri net with initial marking {| (p 0 , 0) | } is depicted. The only enabled transition is t 0 , placing the same color σ(x) ∈ Z = {. . . , -1, 0, 1, 2, . . . } on each of the three places p 1 , p 2 , p 3 when fired in mode σ = {x ← σ(x)}. From each of these places, the color σ(x) may be taken by a respective transition; The three transitions t 1 , t 2 , t 3 , however, each have a guard: ι(t 1 ) = (x ≤ 0), ι(t 2 ) = (x ̸ = 0), and ι(t 3 ) = (x ≥ 0). Depending on the mode σ in which t 0 fired, always two of the three transitions are fireable: if σ(x) = 0 then t 1 and t 3 can both fire (in mode {x ← 0}), if σ(x) < 0 then t 1 and t 2 can fire, and if σ(x) > 0 then t 2 and t 3 can fire.

Since the high-level Petri net in Figure 2a is a high-level occurrence net and all predicates are satisfiable, it is structurally equivalent to its own symbolic unfolding in Figure 2b which is equivalent to 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 e∈{e 1 ,e 2 ,e 3 } pred (e) implies x e 0 ≤ 0 ∧ x e 0 ̸ = 0 ∧ x e 0 ≥ 0, which obviously is not satisfiable. In contrast, each of the sets {e i , e j } with i, j ∈ {1, 2, 3}, i ̸ = j is not in color conflict. This makes each of the sets

{b ′ i , b ′ j } a co-set, while {b ′ 1 , b ′ 2 , b ′ 3 } 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 [START_REF] Chatain | Symbolic Diagnosis of Partially Observable Concurrent Systems[END_REF]) 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 β are collected in the set C(β).

For a configuration C, we define by cut(C) := (B 0 ∪ (C →)) \ (→ C) the high-level conditions that are occupied after any concurrent execution of C. Note that cut(C) is a co-set, and that ∅ is a configuration with cut(∅) = B 0 .

Let e ∈ E be a high-level event. We define the so-called cone configuration

Properties of the Symbolic Unfolding.

Having recalled the definitions and formal language from [START_REF] Chatain | Symbolic Diagnosis of Partially Observable Concurrent Systems[END_REF], 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:

(i) The cuts in the unfolding represent precisely the reachable markings in the net.

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

(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.7, and Prop. 1.8, 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 ∈ Var C∪{⊥} a value in Col , such that the above defined predicates evaluate to true. For each e ∈ C, the assignment of values to the indexed variables in Var e corresponds to a mode of e. Proposition 1.6. Let N be a high-level Petri net and Υ its symbolic unfolding. Then R(N

) = {mark(C, θ) | C ∈ C(Υ ), θ ∈ Θ(C)}.

Proof:

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 π is an initial homomorphism which gives Proof:

M 0 = {{| (π(b), c) | (b, c) ∈ K 0 | } | K 0 ∈ K 0 } = {{| (π(b), c) | (b, c) ∈ K | } | K ∈ K(∅)} = {mark(∅.θ) | θ ∈ Θ(∅)}.
Let U = (B, E, H, ι, K 0 ), C ∈ C(Υ ), θ ∈ Θ(C), t ∈ T, σ ∈ Σ(t). Let mark(C, θ)[t, σ⟩, which means pre (t, σ) ≤ mark(C, θ) = {| (π(b), θ(v e (b))) | (b, θ(v e (b))) ∈ cut(C, θ) | }, leading to {| (π(b), v) | (p, v) ∈ pre (t), π(b) = p, (b, θ(v e (b))) ∈ cut(C, θ) | } = pre (t).
Aiming a contradiction, assume ∄e ∈ E : π(e) = t ∧ cut(C, θ)[e, σ⟩. We now extend Υ by such an event. We add to E an event e with π( e) = t and ι( e) = ι(t). We define pre (

(t) = {| (π(b), v) | (b, v) ∈ pre (e) | } ≤ {| (π(b), v) | (b, v) ∈ cut(C, θ) | } = mark(C, θ), meaning mark(C, θ)[t, σ⟩. ⊓ ⊔
Given a configuration C of a symbolic branching process β = (O, h), we define ⇑C as the pair

(O ′ , h ′ ), where O ′ is the unique subnet of O whose set of nodes is {x ∈ B ∪ E | x / ∈ (C∪ → C) ∧ ∀y ∈ C : ¬(y♯x) ∧ (C ∪
{x} is not in color conflict)} with the set K(C) of initial cuts, and h ′ is the restriction of h to the nodes of O ′ . The branching process ⇑C is referred to as the future of C. Proposition 1.8. If β is a symbolic branching process of (N , M 0 ) and C is a configuration of β, then ⇑C is a branching process of (N , M(C)). Moreover, if β is the unfolding of (N , M 0 ), then ⇑C is the unfolding of (N , M(C)).

Proof:

Let ⇑C = (O ′ , h ′ ) with O ′ = (B ′ , E ′ , F ′ , ι ′ , K(C)).
To show that O ′ is an occurrence net, we have to show i -iv from the definition on page 6. i -iii are purely structural properties and follow from the fact that O is an occurrence net. iv is satisfied since

∀b ∈ cut(C) ∀K ∈ K(C) : c∈Col K(b, c) = 1 and ∀b ∈ B ′ \ cut(C) ∀K ∈ K(C) : c∈Col K(b, c) = 0. h ′ is
a homomorphism that is injective on events with the same preset since h is, and that h ′ is initial follows by Prop. 1.6 and Prop. 1.7.

When β is the symbolic unfolding of (N , M 0 ), then the maximality of ⇑C follows from the maximality of β, making ⇑C the symbolic unfolding of (N , M(C)). ⊓ ⊔

Finite & Complete Prefixes of Symbolic Unfoldings

We combine ideas from [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] (computing small finite and complete prefixes of unfoldings) with results from [START_REF] Chatain | Symbolic Diagnosis of Partially Observable Concurrent Systems[END_REF] (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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] 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.7, this can be seen as a direct translation from the low-level case described, e.g., in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF]. We now define the class N 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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF]. We discuss the properties defining this class, and describe how it generalizes safe P/T nets.

Definition 2.2. (Class N F )

The class N F contains all finite high-level Petri nets N = (P, T, F, ι, M 0 ) satisfying the following three properties:

(1) The net is safe, i.e., in every reachable marking there lies at most 1 color on every place (formally;

∀M ∈ R(N ) ∀p ∈ P : c∈Col M (p, c) ≤ 1).

(2) Guards are written in a decidable first-order theory with the set Col as its domain of discourse.

(3) The net has finitely many reachable markings (formally; |R(N )| < ∞).

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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], 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 N to be ordinary (i.e., ∀x, y ∈ P ∪ T : v∈Var F (x, v, y) ≤ 1), since transitions violating this property could never fire. The finiteness of N implies that we can assume 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 [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF], which is a first order theory of the natural numbers with addition. The guards in the example from Figure 1a are expressible in Presburger arithmetic.

We need Property (3) to ensure that the generalized version of the cut-off criterion from [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] yields a finite prefix constructed in the generalized ERV-Algorithm. |R(N )| < ∞ can be ensured by having a finite set 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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF]: every such P/T net can be seen as a high-level Petri net with Col = {•} and all guards being 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 ERValgorithm from [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] applied to the nets expansion.

For the rest of the section let

N = (P, T, F, ι, M 0 ) ∈ N F with symbolic unfolding Υ = (U, π) = (B, E, H, ι, K 0 , π).

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. [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF]):

Given a configuration C, we denote by C⊕D the fact that C ∪ D is a configuration such that C ∩ D = ∅. We say that C⊕D is an extension of C, and that D is a suffix of C. Obviously, for a configuration

C ′ , if C ⊊ C ′ then there is a nonempty suffix D of C such that C⊕D = C ′ . For a configuration C⊕D, denote by O(C|D) = (cut(C) ∪ →D ∪ D→, D, H ′ , K(C)) the occurrence net "around D" from cut(C)
, where H ′ is the restriction of H to the nodes of O(C|D). Note that for every finite configuration C with an extension C⊕D, we have that D is a configuration of ⇑C.

We abbreviate for a marking M the fact ∃θ ∈ Θ(C⊕D) : mark(C, θ| Var C∪{⊥} ) = M by C M D to improve readability. Thus, C M D means that the transitions corresponding to the events in D can fire from M ∈ 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 ∈ C(Υ ) with π(cut(C 1 )) = π(cut(C 2 )). Then there is a unique bijection ϕ : cut(C 1 ) → cut(C 2 ) preserving π. We call this mapping ϕ C 2 C 1 .
The now stated Prop. 2.4 is a weak version of the arguments in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], where the Esparza et al. follow from the low-level version of Prop. 1.8 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 Υ , and let D be a suffix of

C 1 . If there is a marking M ∈ M(C 1 ) ∩ M(C 2 ) s.t. C 1 M D, then there is a unique monomorphism φ 2 1,D : O(C 1 |D) → ⇑C 2 that satisfies φ 2 1,D (cut(C 1 )) = cut(C 2 )
and preserves the labeling π. For this monomorphism we have that φ 2 1,D (D) is a suffix of C 2 .

Notation. For functions f :

X → Y and f ′ : X ′ → Y with X ∩X ′ = ∅ we define f ⊎f ′ : X ∪X ′ → Y by mapping x to f (x) if x ∈ X and to f ′ (x) if x ∈ X ′ .

Proof:

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

Base case k = 0. This means

D = ∅. Then O(C 1 |D) = (cut(C 1 ), ∅, ∅, K(C 1 )). Since M ∈ M(C 1 ) ∩ M(C 2 ), we know that π(cut(C 1 )) = π(cut(C 2 )). Since we only consider safe nets, φ 2 1,D is uniquely realized by ϕ C 2 C 1 : cut(C 1 ) → cut(C 2 ) from Def. 2.3. Induction step. Let k > 0. Let θ ∈ Θ(C 1 ⊕D) s.t. mark(C 1 , θ| Var C 1 ∪{⊥} ) = M . Let e ∈ Min(D). Then for σ = [v ← θ(v e )] v∈Var (e) we have M [π(e), σ⟩. Thus, by Prop. 1.7, ∃e ′ ∈ E : π(e ′ ) = π(e) ∧ C 2 ⊕{e ′ } ∈ C(Υ ). This means →e ′ ⊆ (B 0 ∪ (C 2 →)) \ (→C 2 ); else, C 2 ⊕{e ′ } would not be a configuration. Thus, e ′ is an event in ⇑C 2 . Since π(e) = π(e ′ ), we get by definition of homomorphisms that {(π(b), v) | (b, v) ∈ post (e)} = {(π(b), v) | (b, v) ∈ post (e ′ )}. The net N is safe, therefore we can define the bijection ϕ 1 : (e→) → (e ′ →) by ϕ 1 (b) = b ′ ⇔ π(b) = π(b ′ ). We now define φ 1 : O(C 1 |{e}) → ⇑C 2 by φ 1 = ϕ C 2 C 1 ⊎ {e → e ′ } ⊎ ϕ 1 , which is a homomorphism satisfying the claimed conditions. Let now C ′ 1 = C 1 ∪ {e}, C ′ 2 = C 2 ∪ {φ 1 (e)} and D ′ = D \ {e}. We then have for M ′ given by M [π(e), σ⟩M ′ that C ′ 1 M ′ D ′ , M ′ ∈ M(C ′ 1 ) ∩ M(C ′ 2 )
, and |D ′ | < k. Thus, by the induction hypothesis, we get that there is a unique monomorphism φ 2 : O(C ′ 1 |D ′ ) → ⇑C ′ 2 satisfying the conditions above. Since φ 1 and φ 2 coincide on cut(C ′ 1 ), we can now define φ 2 1,D by "gluing together" φ 1 and φ 2 at cut(C ′ 1 ).

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 φ 2 1,D 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 [START_REF] Mcmillan | A Technique of State Space Search Based on Unfolding[END_REF][START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], the monomorphism φ 2 1,D defined above replaces the isomorphism I 2 1 between ⇑C 1 and ⇑C 2 for two low-level configurations C 1 , C 2 representing the same marking.

Definition 2.5. (Adequate order)

A partial order ≺ on the finite configurations of the symbolic unfolding of a high-level Petri net is an adequate order if:

i) ≺ is well-founded, ii) C 1 ⊂ C 2 implies C 1 ≺ C 2 , and
iii) ≺ is preserved by finite extensions in the following way: if C 1 , C 2 are two finite configurations, and

C 1 ⊕D is a finite extension of C 1 such that there is a marking M ∈ M(C 1 ) ∩ M(C 2 ) satisfying C 1 M D, then the monomorphism φ 2 1,D from above satisfies C 1 ≺ C 2 ⇒ C 1 ⊕D ≺ C 2 ⊕φ 2 1,D (D).
In the case of a P/T net interpreted as a high-level net, we have |M(C)| = 1 for every configuration C, and therefore, Def. 2.5 coincides with its P/T version [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF]. We could alternatively generalize the P/T case by replacing

'∃M ∈ M(C 1 ) ∩ M(C 2 ) s.t. C 1 M D' by 'M(C 1 ) = M(C 2 )'
, and use the isomorphism I 2 1 between ⇑C 1 and ⇑C 2 to define preservation by finite extension. However, in the upcoming generalization of the ERV-algorithm from [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], the generalized cut-off criterion exploits property iii) of adequate orders. Using 'M(C 1 ) = M(C 2 )' would produce an exponential blowup of the generated prefix's size. This is circumvented by using '∃M ∈ M(C 1 ) ∩ M(C 2 ) s.t. C 1 M 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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF]. It uses that, under the conditions of Def. 2.5 iii), we also have

C 2 ≺ C 1 ⇒ C 2 ⊕φ 2 1,D (D) ≺ C 1 ⊕D.
This result would directly be obtained if φ 2 1,D was an isomorphism, as I 2 1 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 φ 2 1,D indeed satisfies the above property.

Proposition 2.6. Let ≺ be an adequate order. Under the conditions of Def. 2.5 iii) the monomorphism φ 2 1,D also satisfies

C 2 ≺ C 1 ⇒ C 2 ⊕φ 2 1,D (D) ≺ C 1 ⊕D. Proof: Let D ′ = φ 2 1,D (D). We first show that φ 1 2,D ′ (D ′ ) = D. Let φ 1 : O(C 1 |D) → φ 2 1,D (O(C 1 |D)) be the isomorphism that acts on O(C 1 |D) as φ 2 1,D does, and let φ 2 : O(C 2 |D ′ ) → φ 1 2,D ′ (O(C 2 |D ′ )) be the isomorphism that acts on O(C 2 |D ′ ) as φ 1 2,D ′ does. Since φ -1 1 : φ 2 1,D (O(C 1 |D)) → O(C 1 |D) and O(C 1 |D) ⊂ ⇑C 1 , and φ -1 1 (φ 2 1,D (D)) = D is a suffix of C 1 , we get by Prop. 2.4 that φ -1 1 = φ 2 , which means φ 1 2,D ′ (D ′ ) = D. Assume now C 2 ≺ C 1 . From the proof of Prop. 2.4 we see that C 2 M φ 2 1,D (D)
. Thus, we get by the definition of adequate order and the result above that

C 2 ⊕φ 2 1,D (D) ≺ C 1 ⊕φ 1 2,φ 2 1,D (D) (φ 2 1,D (D)) = C 1 ⊕D ⊓ ⊔
In [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], 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 |R(N )| non cut-off events. All three adequate orders presented in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] can be directly lifted to the configurations of the symbolic unfolding by exchanging every low-level term by its highlevel 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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], e is a cut-off event if there is another event e ′ satisfying [e ′ ] ≺ [e] and mark([e]) = mark([e ′ ]), which ensures that the future of 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 ′ with [e ′ ] ≺ [e] and M([e]) = M([e ′ ]). 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 M([e]) is contained in the union of all M([e ′ ]) with [e ′ ] ≺ [e]. This criterion expresses that we have already seen every marking in M([e]) in the prefix β under construction, and therefore need not consider the future of e any further. By this, we obtain the same upper bounds as in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], as discussed later.

Definition 2.7. (Cut-off event)

Let ≺ be an adequate order on the configurations of the symbolic unfolding of a high-level Petri net. Let β be a prefix of the symbolic unfolding containing a high-level event e. The high-level event e is a cut-off event in

β (w.r.t. ≺) if M([e]) ⊆ [e ′ ]≺[e] M([e ′ ]).
When interpreting P/T nets as high-level nets, this definition corresponds to the cut-off events defined in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], since then |M([e])| = 1 for all events e.

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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], 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.8, 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 [START_REF] Chatain | Symbolic Diagnosis of Partially Observable Concurrent Systems[END_REF] 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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF]. There, an event is given by a tuple e = (t, B ′ ) with h(e) = t ∈ T and pre (e) = B ′ ⊆ B, and a condition given by a tuple b = (p, e) with h(b) = p ∈ P and pre (b) = {e} ⊆ 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, pred ) described by h(e) = t, pre (e) = X ⊆ B × Var , and pred (e) = pred . Analogously, a high-level condition is given by a tuple b = (p, (e, v), pred ), where h

(b) = p, pre (b) = (e, v) ∈ (E × Var ) ∪ ({⊥} × {v b | b ∈ B 0 }),
(t) = {(h(b), v) | (b, v) ∈ X}, • pred = loc-pred ∧ (b,v)∈X pred (e(b)) is satisfiable, where loc-pred = ι(t)[v ← v e ] v∈Var (e) ∧ (b,v)∈X v e = v e (b) , • Fin does not contain (t, X, pred ).
Since the notion of co-set in high-level occurrence nets is achieved by the direct translation from lowlevel occurrence nets plus the "color conflict freedom", possible extensions in a prefix β 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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] for complete finite prefixes of the lowlevel unfolding. The structure is taken from there, with the only difference being the special initial transition ⊥. It takes as input a high-level Petri net N ∈ N F and assumes a given adequate order ≺.

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

Starting with the initial conditions a ′ abd b ′ , the possible extensions are α ′ and β ′ . assuming

[α ′ ] ≺ [β ′ ],
we first attach α ′ and a condition c ′ corresponding to the output place c of α, and then analogously β ′ and the condition d ′ .

For

α ′ we have M([α ′ ]) = {{| (c, n), (b, 0) | } | n ∈ {1, .
. . , m}} and analogously, for

β ′ we have M([β ′ ]) = {{| (a, 0), (d, n) | } | n ∈ {1, .
. . , m}}. Since we have not seen these markings before, neither α ′ nor β ′ is a cut-off event. Thus, we have the possible extensions t ′ and ε ′ . For t ′ we have M([t ′ ]) = {{| | }}, since no tokens are in the net after firing t. However, we have not seen the empty marking {| | } before, so formally, t ′ is not a cut-off event.

For

ε ′ we have M([ε ′ ]) = {{| (c, n), (d, n ′ ) | } | n, n ′ ∈ {1, . . . , m}}.
Corresponding cuts can be reached in the prefix constructed so far by concurrently firing α ′ and β ′ . However, no marking {| (c, n), (d, n ′ ) | } is represented by a cone configuration before ε ′ , and therefore

ε ′ does not satisfy M([ε ′ ]) ⊆ [e ′ ]≺[ε ′ ] M([e ′ ]
). This means ε ′ is not a cut-off event and we have to proceed with the possible extensions t ′′ and ε ′′ .

Algorithm 1: Generalization of the ERV-Algorithm from [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] for complete finite prefixes.

Data: High-level Petri net N = (P, T, F, ι, M 0 ) ∈ N F .

Result: A complete finite prefix Fin of the symbolic unfolding of N . Fin ← {⊥};

pred (⊥) ← M 0 ∈M 0 (p,c)∈M 0 v bp ⊥ = c; foreach p ∈ P 0 do Create a fresh condition b p = (p, (⊥, v bp ), pred (⊥)); Fin ← Fin ∪ {b}; end pe ← PE (Fin); cut-off ← ∅; while pe ̸ = ∅ do Pick e = (t, X, pred ) from pe such that [e] is minimal w.r.t. ≺; if [e] ∩ cut-off = ∅ then Fin ← Fin ∪ {e}; foreach (p, v) ∈ post (t) do Create a fresh condition b = (p, (e, v), pred ); Fin ← Fin ∪ {b}; end pe ← PE (Fin); if e is a cut-off event of Fin then cut-off ← cut-off ∪{e}; end else pe ← pe \ {e} end end Since M([t ′′ ]) = {{| | }} = M([t ′ ]) with [t ′ ] ≺ [t ′′ ],
have that t ′′ is a cut-off event. This, however, has no impact on the prefix since we cannot continue after t ′′ anyway. For

ε ′′ we have M([ε ′′ ]) = {{| (c, n), (d, n ′ ) | } | n, n ′ ∈ {1, . . . , m}} = M([ε ′ ]) with [ε ′ ] ≺ [ε ′′ ].
This makes ε ′′ 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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], by stating two propositions -one each to show that the prefix is finite and complete, respectively. The proof structure is also as in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], but adapted to the setting of high-level Petri nets and symbolic unfoldings. Proposition 2.10. 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 < • • • < e; the depth of e is denoted by d(e).

Proof:

As in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], we prove the following results (1) -( 3):

(1) For every event e of Fin, d(e) ≤ |R(N )| + 1,

(2) For every event e of Fin, the sets pre (e) and post (e) are finite, and

(3) For every k ≥ 0, Fin contains only finitely many events e such that d(e) ≤ k.

This works exactly as in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], with minor adaptations to the generalization of cut-offs in the symbolic unfolding in (1):

(1) Let n = |R(N )|. Every chain of events e 1 < e 2 < • • • < e n < e n+1 in the unfolding contains an event e i , i > 1, s.t. M([e i ]) ⊆ i-1 j=1 M([e j ]), since, if every M([e j ]), j = 1, . . . , n, contains a marking not contained in j-1 k=1 M([e k ]), then finally n j=1 M([e j ]
) contains all n markings. This makes e n+1 a cut-off event.

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

(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, The proof of this proposition also has the same general structure as the respective proof in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF]. However here we use the generalizations of adequate order, possible extensions, and the cut-off criterion to symbolic branching processes.

post (E k ) is finite. Since {b | ∃v ∈ Var : (b, v) ∈ pre (E k+1 )} ⊆ {b | ∃v ∈ Var : (b, v) ∈ post (E k )},

Proof:

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

(1) Let M be an arbitrary reachable marking in N . Then by Prop. 1.6, we have that there is a

C 1 ∈ C(Υ ) s.t. M ∈ M(C 1 ). Let θ 1 ∈ Θ(C 1 ) s.t. M = mark(C 1 .θ 1 ). If C is not a configuration in
C 2 := [e 2 ]⊕φ 1 (D) ≺ [e 1 ]⊕D = C 1 . Let θ ′ 2 ∈ Θ([e 2 ]) s.t. M 1 = mark([e 2 ], θ ′ 2 ). Define now θ 2 ∈ Θ(C 2 ) by θ 2 = θ ′ 2 ⊎ θ ′′ 2 , where θ ′′ 2 : Var φ 1 (D) → Col is given by θ ′′ 2 (v φ 1 (e) ) = θ 1 (v e )
. By this construction we get

M = mark(C 2 , θ 2 ) ∈ M(C 2 ).
If C 2 is not a configuration of Fin, then we can iterate the procedure and find a configuration C 3 such that C 3 ≺ C 2 and M ∈ M(C 3 ). The procedure cannot be iterated infinitely often because ≺ is well-founded. Therefore, it terminates in a configuration of Fin.

(2) Let now C be a minimal configuration w.r.

= {(h(b), θ(v e (b))) | b ∈ B t,σ }. Let now X := {(b, v) | b ∈ B t,σ , (h(b), v) ∈ pre (t)}. We then have ∀(b, v) ∈ X : σ(v) = θ(v e (b)).
We now show that Notice that by this construction, as described in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], we get that if ≺ is a total order, then Fin contains at most |R(N )| non cut-off events. As already discussed in Sec. 2.1, the total adequate order defined in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] 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 ≺ being a total adequate order.

pred := ι(t)[v ← v e ] v∈Var (e) ∧ (b,v)∈X v e = v e (b) ∧ (b,v)∈X pred (e(b)) is satisfiable. Let θ ′ := θ ⊎ (σ • [v e → v] v∈Var (e) ). Then • ι(t)[v ← v e ] v∈Var (

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 •. 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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] for a complete finite prefix of the (P/T) unfolding.

The procedure of constructing the represented P/T Petri net Exp(N ) (called the expansion) of a high-level Petri net N is well established (cp., e.g., Chapter 2.4 in [START_REF] Jensen | Coloured Petri Nets -Basic Concepts, Analysis Methods and Practical Use -Volume 1, Second Edition[END_REF]), and we describe it here only briefly; the places of Exp(N ) are given by P = {p.c | p ∈ P, c ∈ Col }, and its transitions by

T = {t.σ | t ∈ T, σ ∈ Σ(t)}.
There is an arc from p.c to t.σ iff (p, c) ∈ pre (t, σ), and analogously for arcs from transitions to places. Markings in Exp(N ) are functions M : P → N, describing how often the only color • lies on each place p.c. Every such marking corresponds to a marking M in the high-level net N , with M (p, c) = M(p.c), and a transition t can fire in mode σ from M iff t.σ can fire from M. Thus, we say that N and Exp(N ) have the same behavior. For a finite high-level Petri net N , the expansion Exp(N ) is finite iff Col is finite.

The (low-level) unfolding of a P/T Petri net N is a tuple Υ(N) = (U(N), π N ), where U(N) is an occurrence net, and π N : U(N) → N is a Petri net homomorphism such that (U(N), π N ) is a maximum branching process of 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 [START_REF] Engelfriet | Branching Processes of Petri Nets[END_REF][START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF].

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 Exp O (O) = U(Exp(O)) (i.e., the occurrence net from the unfolding Υ(Exp(O)) = (U(Exp(O)), π Exp(O) )). We abbreviate π Exp(O) by π O . The operator Exp O therefore maps high-level occurrence nets to occurrence nets (cf. [START_REF] Chatain | Factorization Properties of Symbolic Unfoldings of Colored Petri Nets[END_REF]). Let now β = (O, h) be a symbolic branching process of N . Then we can define the expanded symbolic branching process

Exp O (β) = (Exp O (O), h) of Exp(N ) with the homomorphism h : Exp O (O) → Exp(N ), defined by h(e) = t.σ ⇔ π O (e) = e.σ ∧ h(e) = t and h(b) = p.c ⇔ π O (b) = b.c ∧ h(b) = p for events e resp. conditions b in Exp O (O).
The following diagram serves as an overview:

N O β (O, h) Exp(O) ⇝ Exp(N ) Exp O (O) U(Exp(O)) Exp O (β) (Exp O (O), h) Exp h Exp ExpO ExpO = h π O = =
The following result is shown in [START_REF] Chatain | Factorization Properties of Symbolic Unfoldings of Colored Petri Nets[END_REF]. 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 . With this result, we state the following: Lemma 3.2. Let N be a high-level Petri net and β be a prefix of Υ (N ). Then β is finite and complete if and only if Exp O (β) is a finite and complete prefix of Υ(Exp(N )).

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

Proof:

Let β = (O, h) be finite and complete. From Lemma 3.1 we already know that Exp O (O) ⊆ U(Exp(N )). Since Exp O (β) is a branching process of Exp(N ), we see that is a prefix of the unfolding of Exp(N ). Also, Exp O (β) is obviously finite since O is a finite high-level occurrence net.

We now prove that Exp O (β) = (Exp O (O), h) is complete. Let M be a reachable marking in Exp(N ). Then the high-level marking M defined by M (p, c) = M(p.c) is reachable in N . Thus, since β is complete, there is a configuration C ∈ C(β) and an instantiation θ ∈ Θ(C) satisfying a) and b) from Def. 2.1. This means there is a firing sequence The other direction works analogously.

K 0 [e 1 , σ 1 ⟩K 1 . . . [e n , σ n ⟩K n with {e 1 , . . . , e n } = C, σ i = θ • [v → v e i ] v∈Var (e i ) , and K n = cut(C, θ) (meaning M = mark(C, θ) = {| (h(b), c) | (b, c) ∈ K n | }).

⊓ ⊔

We can now compare the two complete finite prefixes resulting from the original ERV-algorithm from [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] applied to Exp(N ) and the generalized ERV-algorithm Alg. 1 applied to N ∈ N 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.3. Consider again N ∈ N F from Figure 1a with Col = {0, 1, . . . , m} for a fixed m > 0. The finite complete prefix of Υ(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 ε 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 α and an instance of β, we arrive at conditions with labels c.k and d.ℓ. If these satisfy ℓ = k • 3 then we can fire an instance of t, which means we have ⌊ m 3 ⌋ 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.

⌋, 3⌊ m 3 ⌋) ⌊ m 3 ⌋ events ⌊ m 3 ⌋ (cut-off) events t t
For each combination of an output condition of an instance of α (the m instances of c) and an output condition of an instance of β (the m instances of d), we have m 2 possibilities to fire an instance of ε. 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 ε-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⌊ m 3 ⌋ + 2 nodes for every fixed m in the color class Col = {0, 1, . . . , m}. The complete finite prefix of the symbolic unfolding Υ (N ) that is shown in Figure 1b, 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.4. For every n ∈ N, there is a family (N n m ) m>1 of high-level nets in N F such that every N n m has the set of colors Col = {0, . . . , m} and satisfies that • the complete finite prefix of Υ (N n m ) obtained by Alg. 1 has the same number of nodes for every m,

• the number of nodes in the low-level prefix of Υ(Exp(N n m )) obtained by the original ERValgorithm is greater than m n .

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

Handling Infinitely Many Reachable Markings

Unfoldings of unbounded P/T Petri nets (i.e., with infinitely many markings) have been investigated in [START_REF] Abdulla | Unfoldings of Unbounded Petri Nets[END_REF][START_REF] Desel | Finite Unfoldings of Unbounded Petri Nets[END_REF], and in [START_REF] Herbreteau | Unfolding Concurrent Well-Structured Transition Systems[END_REF] 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 N F ), the proof for finiteness of the resulting prefix does not hold anymore: the proof of Prop. 2.10, step (1), is a generalization of the proof of the respective claim in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] (which uses the pigeonhole principle). It is argued that we cannot have |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 N SC of safe high-level nets, called symbolically compact, that have possibly infinitely many reachable markings (and therefore an infinite expansion), generalizing the class N 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 prefix of the symbolic unfolding for any N ∈ N 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 = (N , M 0 ) there exists a finite and complete prefix of Υ (N ) if and only if there exists a bound n ∈ N such that every marking in R(N ) is reachable from a marking in M 0 by firing at most n transitions.

Proof: From Prop. 1.6 and Prop. 1.7 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 d(e) ≤ 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 β of Υ (N ). Denote n = max{|C| | C ∈ C(β)} < ∞. Then there exists a marking M ∈ R(N ) for which we have to fire at least n + 1 transitions to reach it. Again from Prop. 1.6 and Prop. 1.7 it follows that a configuration C with M ∈ M(C) must contain at least n + 1 events, contradicting that β is complete.

⊓ ⊔

Symbolically Compact High-level Petri Nets

We use the result of Lemma 4.1 to define the class N SC of high-level nets for which we adapt the algorithm for constructing finite and complete prefixes of the symbolic unfolding. We denote the class containing all symbolically compact high-level Petri nets by N SC .

Note that in the case of a (finite, safe) P/T net, property (3*) is equivalent to (3) (i.e., |R(N )| < ∞). However, this is not true for all high-level nets N : while |R(N )| < ∞ still implies (3*) (meaning N F ⊆ N SC ), the reverse implication does not hold, as our running example from Figure 1a demonstrates when we change the set of colors to Col = N: it then still satisfies (1) and (2), with R(N ) = {{| (a, 0), (b, 0

) | }, {| | }} ∪ {{| (c, n), (b, 0) | }, {| (a, 0), (d, n ′ ) | }, {| (c, n), (d, n ′ ) | } | n, n ′ ∈ 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 N SC of symbolically compact nets contains exactly all highlevel 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 N SC \ N 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 Υ (N ), but

• there does not exist a finite and complete prefix of Υ (Exp(N )).

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

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

p 0 t x y
Obviously, every reachable marking {| (p, n) | } with n ∈ N can be reached by firing t one time in mode {x ← 0, y ← 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.

Insufficiency of the Cut-off Criterion for N 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. Note that in the second condition, there the e ′ in the union are are abitrary events in the unfolding, and not restricted to the sequence (e 1 , e 2 , . . . ). An example for such a net is shown in Figure 4a:

a ′ c ′ p ′ . . . . . . α ′ γ ′ b ′ . . . d ′ . . . β ′ δ ′ a ′′ c
The set of colors is given by Col = 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 α and β. Analogously, the other token can cycle between c and d by γ and δ. 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 ε. The net therefore is symbolically compact.

Examine now the unfolding in Figure 4b. 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

ε ′ we have M([ε ′ ]) = {{| (b, 0), (d, 0), (p, n) | } | n ∈ N}.
This means by firing no event, only β ′′ , only δ ′′ , or both β ′′ and δ ′′ from the corresponding cut, we can represent every reachable marking in the net.

The sequence [t 1 ], 2 ], . . . 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 4a it does not terminate, building a prefix containing every t i with i ∈ N + .

The Finite Prefix Algorithm for Symbolically Compact Nets

As previously discussed, the argument that states the existence of one event in a chain of |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 N SC \N 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.7. Therefore, we define cut-off* events, that generalize cut-off events. They only require that every marking in M([e]) has been observed in a set M(C) for any configuration C ≺ [e], rather than just considering cone configurations: We additionally assume that the used adequate order satisfies

|C 1 | < |C 2 | ⇒ C 1 ≺ C 2 ,
so that every event with depth > n will be a cut-off event. Since all adequate orders discussed in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] satisfy this this property (cp. App. A.1), this is a reasonable requirement. This adaption and assumption now lead to: Theorem 4.4. Assume a given adequate order ≺ to satisfy

|C 1 | < |C 2 | ⇒ C 1 ≺ C 2 .
When replacing in Alg. 1 the term "cut-off event" by "cut-off* event", it terminates for any input net N ∈ N SC , and generates a complete finite prefix of Υ (N ).

Proof:

The properties of symbolic unfoldings that we stated in Sec. 1.3 are independent on the class of highlevel nets. Def. 2.3 only uses that the considered net is safe, and so do Prop. 2.4 and Prop. 2.6. We therefore only have to check that the correctness proof for the algorithm still holds. In the proof of Prop. 2.10 (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 |R(N )| + 1. This is not applicable when |R(N )| = ∞, as argued above. Instead we show:

(1*) For every event e of Fin, d(e) ≤ n+1, where n is the bound on the number of transitions needed to reach all markings in R(N ). In the proof of Prop. 2.11, the cut-off criterion is used to show (by an infinite descent approach), for any marking M ∈ R(N ) the existence of a minimal configuration C ∈ Fin with M ∈ 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 ′ , E ′ , H ′ , ι ′ , K ′ 0 ) of the prefix under construction, such that there occurs a chain of events e 1 < e 2 < • • • < e n+1 . We prove that e n+1 must be a cut-off* event. Let M ∈ M([e n+1 ]). Then, by definition of N SC , M can be reached by firing at most n transitions. Accordingly, from Prop. 1.7, we get that there is a configuration C ∈ Υ containing at most n events such that M ∈ M(C). As in the proof of Prop. 2.11, we can now follow that there is a configuration C ∈ C(Υ ) such that M ∈ M( C) and C ≺ C, that contains no cut-off event and is therefore in Fin.

Since |C| ≤ n < n + 1 ≤ |[e n+1 ]|, we follow C ≺ [e n+1 ]. So we have that ∀M ∈ M([e n+1 ]) ∃ C ≺ [e n+1 ],
which means that e n+1 is a cut-off* event. This proves that Fin is finite.

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

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 N 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 [START_REF] Schmidt | Parameterized Reachability Trees for Algebraic Petri Nets[END_REF] 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 ′ of places a formula R P ′ that symbolically describes all reachable markings that we have seen so far and have colors on exactly all places in P ′ . Initially, all formulae are false, except for R P 0 , where P 0 are the initially marked places. 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 = 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 ′ , and label it with a formula f ′ that symbolically represents all markings reached from firing t in any mode from any marking in M 0 . In all these markings, there are colors on the same set of places P ′ . If f ′ ⇒ R P ′ then we end this branch. We then extend R P ′ to R P ′ ∨ f ′ .

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.

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 M([e]) ⊆ C≺[e] M(C). However, since the cut of a configuration can represent infinitely many markings, we cannot simply store the set M(C) for every C ∈ C(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 ∈ N F , an event e is a cut-off event in the sense of Def. 2.7. This method is also used in the implementation described in Sec. 6.1.

For the rest of this section, let N = (P, T, F, ι, M 0 ) ∈ N SC with symbolic unfolding Υ = (U, π) = (B, E, H, ι, K 0 , π).

We first define for every condition b a new predicate pred For a co-set B ′ ⊆ B of high-level conditions, the constraint on B ′ is an expression with free variables π(B ′ ) = {π(b) | b ∈ B ′ } describing which color combinations can lie on the places represented by the high-level conditions. We build the conjunction over all predicates pred ⊙ (b) for b ∈ B ′ and quantify over all appearing variables v e : the constraint on B ′ is defined by

κ(B ′ ) := ∃ b∈B ′ Var [e(b)]∪{⊥} : b∈B ′ pred ⊙ (b),
We denote by Ξ(B ′ ) the set of variable assignments ϑ : π(B ′ ) → Col that satisfy κ(B ′ )[ϑ] ≡ true.

For a configuration C, we have that B ′ = cut(C) is a co-set, π(B ′ ) = π(cut(C)) describes the set of places occupied in every marking in M(C). Note that in this case, we have b∈cut(C) Var [e(b)] = Var C , i.e., the bounded variables in κ(cut(C)) are exactly the variables appearing in predicates in C. For every instantiation θ of C we define a variable assignment

ϑ θ : π(cut(C)) → Col by setting ∀π(b) ∈ π(cut(C)) : ϑ θ (b) = θ(v e (b)
). Instantiations of a configuration and the constraint on its cut are now related as follows.

Lemma 5.1. Let C ∈ C(Υ ). Then Ξ(cut(C)) = {ϑ θ | θ ∈ Θ(C)}.

Proof:

The proof follows by construction of pred ⊙ and ϑ

θ : Let ϑ ∈ Ξ(cut(C)). Then true ≡ κ(cut(C))[ϑ].
Thus, there exists θ :

Var C∪{⊥} → Col s.t. b∈cut(C) pred ⊙ (b) [ϑ][θ] ≡ true and therefore b∈cut(C) pred (e(b))[θ] ∧ b∈cut(C) ϑ(π(b)) = θ(v e (b)) ≡ true. (1)
From the inductive definition of pred then follows that ∀e ∈ C ∪ {⊥} : pred (e)[θ] ≡ true. Thus, θ is an instantiation of C, and ϑ θ = ϑ, as shown by the posterior conjunction in [START_REF] Würdemann | Taking Complete Finite Prefixes to High Level, Symbolically[END_REF]. Let on the other hand θ ∈ Θ(cut(C)). Then directly, by the definition of pred ⊙ (b) and ϑ θ , we get ⊓ ⊔

From the definition of K(C) and M(C) we get:

Corollary 5.2. Let C ∈ C(Υ ). Then K(C) = {{(b, ϑ(π(b))) | b ∈ cut(C)} | ϑ ∈ Ξ(cut(C))} and M(C) = {{| (π(b), ϑ(π(b))) | b ∈ cut(C) | } | ϑ ∈ Ξ(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.3, and then explicitly apply this result to cone configurations [e] in Cor. 5.4.

Theorem 5.3. Let C, C 1 , . . . , C n be finite configurations in the symbolic unfolding of a safe highlevel Petri net s.t.

∀1 ≤ i ≤ n : π(cut(C)) = π(cut(C i )). Then M(C) ⊆ n i=1 M(C i ) if and only if κ(cut(C)) ⇒ n i=1 κ(cut(C i )).
Proof:

Assume M(C) ⊆ n i=1 M(C i ) and let ϑ ∈ Ξ(cut(C)). We have that M ϑ := {(π(b), ϑ(π(b))) | b ∈ cut(C)} ∈ M(C) by Cor. 5.2. Thus, ∃1 ≤ i ≤ n : M ϑ ∈ M(C i ). This, again by Cor. 5.2, means ∃ϑ i ∈ Ξ(cut(C i )) : M ϑ = {(π(b ′ ), ϑ i (π(b ′ ))) | b ′ ∈ cut(C i )}
This shows that ϑ = ϑ i . Thus, κ(cut(C i ))[ϑ] ≡ true, which proves the implication. Assume on the other hand κ(cut(C))

⇒ n i=1 κ(cut(C i )). Let M ∈ M(C). Then ∃ϑ ∈ Ξ(cut(C)) : M = {(π(b), ϑ(π(b))) | b ∈ cut(C)}. Thus, ∃1 ≤ i ≤ n : κ(cut(C i ))[ϑ] ≡ true. Let ϑ i = ϑ. Then ϑ i ∈ Ξ(cut(C i )), and M = {(π(b ′ ), ϑ i (π(b ′ ))) | b ′ ∈ cut(C i )} ∈ 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.3 together with the facts that

M(C 1 ) ∩ M(C 2 ) ̸ = ∅ ⇒ π(cut(C 1 )) = π(cut(C 2 )
), and that ≺[e] is finite.

Corollary 5.4. Let β be a symbolic branching process and e an event in β. Then e is a cut-off* event in β if and only if

κ(cut([e])) ⇒ C≺[e] h(cut(C))=h(cut([e])) κ(cut(C)).
Thus, we showed how to decide for any event e added to a prefix of the unfolding whether it is a cutoff* event, namely, by checking the above implication in Cor. 5.4. Note that we can also check whether e is a cut-off event (w.r.t. Def. 2.7) by the implication in Cor. 5.4 when we replace all occurrences of "C" by "[e ′ ]" .

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.

Implementation Specifics

Other tools designed for generating (prefixes of) P/T Petri net unfoldings include MOLE [19], CUNF [20,[START_REF] Rodríguez | Cunf: A Tool for Unfolding and Verifying Petri Nets with Read Arcs[END_REF], and PUNF [START_REF] Khomenko | [END_REF]. 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 [START_REF] Panneke | [END_REF] 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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] (complete finite prefixes) and [START_REF] Khomenko | Branching Processes of High-Level Petri Nets[END_REF] (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 N 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 2b, 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.4, and to detect when to discard event candidates because of a color conflict. For this task we chose the CVC5 SMT solver [START_REF] Barbosa | cvc5: A Versatile and Industrial-Strength SMT Solver[END_REF]. It performed best in the relevant category (non-linear arithmetic with equality and quantifiers) of the Satisfiability Modulo Theories Competition (SMT-COMP 2023)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.

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 ε then takes these colors from all places, ending the nets execution. We have two parameters: the first parameter, m ∈ N, determines the set of colors Col = {0, . . . , m}. The second parameter, n ∈ N, determines the number of output places of t. Fig. 5 shows the independent diamonds for n = 2 in (a) and for n = 4 in (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.

The Water Pouring Puzzle

This benchmark family generalizes a classic logic puzzle (cf., e.g., [START_REF] Atwood | A process model for water jug problems[END_REF]) 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 , . . . , n k ] of natural numbers. Each entry n i represents an available bucket holding n i liters. The second parameter, m ∈ N is the amount of water that should be measured. Fig. 6 shows the high-level Petri net corresponding to the parameters n = [START_REF] Jensen | Coloured Petri Nets -Basic Concepts, Analysis Methods and Practical Use -Volume 1, Second Edition[END_REF][START_REF] Nielsen | Petri Nets, Event Structures and Domains, Part I[END_REF] and m = 4, corresponding to the puzzle above. Independently of the parameters, we have Col = N. The current fill level of each bucket i is represented by

i1 i2 0 bucket-1 0 bucket-2 1-transfer -2 (o2 ≤ 3 ∧ o1 = 0 ∧ o2 = i1 + i2) ∨(o2 = 3 ∧ o1 = i1 -(3 -i2))
2-transfer -1

(o1 ≤ 5 ∧ o2 = 0 ∧ o1 = i2 + i1) ∨(o1 = 5 ∧ o2 = i2 -(5 -i1))
fill -1 a place bucket-i, with an initial color 0, and two attached transitions fill -i and empty-i, that, when fired, replace the color on bucket-i by n i or 0, respectively. Additionally, for each pair of buckets i, j, there are two transitions i-transfer -j and j-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.

Hobbits And Orcs

The Hobbits And Orcs problem3 is another logic puzzle (in particular one of many "river crossing problems", cf., e.g., [START_REF] Jeffries | A process model for Missionaries-Cannibals and other river-crossing problems[END_REF][START_REF] Pressman | The jealous husbands and The missionaries and cannibals[END_REF]) 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 ∈ N is the number of both Hobbits and Orcs. We always have equally many of the two parties. The second parameter, n ∈ 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.

Figure 7a shows an illustration of the original puzzle presented above, with three of both, Hobbits and Orcs, and a boat fitting two passengers. Figure 7b shows the corresponding high-level Petri game.

(a) An illustration of the "Hobbits And Orcs" problem. 4(3, 3) bank -ℓ (0, 0) docked -ℓ load -ℓ

h ′ + x = h o ′ + y = o h ′ > 0 ⇒ h ′ ≥ o ′ x > 0 ⇒ x ≥ y 1 ≤ x + y ≤ 2 unload -ℓ h ′ = h + x o ′ = o + y h ′ > 0 ⇒ h ′ ≥ o ′ crossing returning (h, o) (h ′ , o ′ ) (0, 0) (x, y) (h ′ , o ′ ) (h, o) (0, 0) (x, y) docked -r load -r h ′ + x = h o ′ + y = o h ′ > 0 ⇒ h ′ ≥ o ′ x > 0 ⇒ x ≥ y 1 ≤ x + y ≤ 2 unload -r h ′ = h + x o ′ = o + y h ′ > 0 ⇒ h ′ ≥ o ′ (0, 0) bank -r (h, o) (h ′ , o ′ ) (0, 0) (x, y) (h ′ , o ′ ) (h, o) (0, 0) (x, y) Col = N × N goal (3, 3) (b)
The problem modeled as a high-level Petri net. The colors are given by Col = N × 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 bank -ℓ. 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 docked -ℓ, indicating an empty boat the left bank. Via the transitions load and 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.

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 [START_REF] Knuth | The Computer as Master Mind[END_REF][START_REF] Koyama | An optimal Mastermind Strategy[END_REF]. 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. 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 ∈ N, describes the number of available colors. The second parameter, n ∈ N, describes the length of the code. The third parameter, k ∈ 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 code-i by firing pick -code. Transition tuple puts these colors into a tuple on place 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 guess. Transition evaluate compares this guess to the code and places the result, i.e., the corresponding number of red and white pins, on result. From there, the code breaker either wins if the guessed code was correct, or resets with transition retry, provided that he has another attempt left.

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 [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] and [START_REF] Khomenko | Branching Processes of High-Level Petri Nets[END_REF].

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

∀M ∈ R(N ) ∀t ∈ T ∃ ≤1 σ ∈ Σ(t) : M [t, σ⟩.
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 fill -i and fill -i replace the color on bucket-i with a predetermined one. Every transition 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 load -ℓ 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 n i=1 i + 1 = 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.

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 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 [START_REF] Panneke | [END_REF] 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. 9a, 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. 9b. For all the cases from Fig. 9a, the symbolic approach takes around 200 ms to complete the symbolic unfolding. This is independent of the color class {0, . . . , 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 Col = {0, . . . , m}. This even does not change for Col = N. Since cvc5 (the tool used for checking satisfiability, cp. Sec. 6.1) can handle such infinite color domains, we fix Col = N, and Fig. 9b 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. 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 lowlevel and symbolic unfolding, as well as their prefixes, are isomorphic. Table 1 presents the results for this benchmark. The original puzzle with n = [START_REF] Jensen | Coloured Petri Nets -Basic Concepts, Analysis Methods and Practical Use -Volume 1, Second Edition[END_REF][START_REF] Nielsen | Petri Nets, Event Structures and Domains, Part I[END_REF] and m = 4 is included in the first line. Additionally, we randomly selected eight parameter sets such that we consider four scenarios involving 2 buckets and four scenarios involving 3 buckets.

We indicate in each scenario whether the puzzle is solvable, and in the positive case, how many steps a minimal solution has. We compare the time to check the reachability of a goal state (fireability of the goal transition, cp. above) of the low-level and symbolic approach. The faster approach is highlighted with bold font. Additionally, we notate the number of conditions (|B|) and events (|E|) of the generated prefix. Each of these two numbers coincides between the two approaches.

When we pick the parameters at random the low-level approach generally is much faster. We can, however, construct examples in which the symbolic approach outspeeds the low-level approach. In these constructed cases we have a large color domain but can reach the goal quite quickly, e.g., with two buckets of capacity 10 6 and 10 6 + 1, and a target of m = 1. We find that the low-level approach performs better when the boat capacity is smaller. For n = 2, the symbolic approach gets a timeout at m = 13 while the low-level approach can calculate the prefix up to m = 33. We expected this behavior, because a smaller the boat capacity yields a higher degree of mode determinism in the net. When the capacity increases, the net is 'less' mode deterministic. For n ≥ 6 the symbolic approach is faster for all population sizes. Independent of the boat size n, both approaches take exponentially more time with growing population size.

Mastermind. We present some results for the Mastermind benchmark in Table 2. We compare the time needed by the low-level and symbolic approach to generate the unfolding, with a timeout of two minutes. The table also shows the number of nodes (conditions |B| resp. |B|, and events |E| resp. |E|) in the unfolding. In each row the faster time is highlighted in bold font.

The first line shows the original problem with k = 12 attempts, a code length of n = 4, and m = 6 colors. We observe that in the low-level approach, time and size grow exponentially with respect to the number m of colors, whereas the high-level approach remains constant. When we increase the parameter n controlling the length of the code, both approaches grow exponentially in time. Interestingly the high-level approach only grows linear in size (number of nodes). This is due to the size of the guard of the evaluate transition increasing exponentially (n choose 2).

Overall, the symbolic approach is the clear winner of the Mastermind benchmark. The low-level approach can only barely compete for the smallest instances of the problem.

We also observe that, in comparison to other parameters, the of the high-level approach drops when n = m. We currently have no explanation for this. This could be a quirk of the SMT solvers, or alternatively, the formulas may be inherently more challenging to solve in this particular case. The low-level approach is not impacted negatively by this case, but still much slower than the symbolic approach, as seen in lines with parameters (1, 3, 3), [START_REF] Würdemann | Taking Complete Finite Prefixes to High Level, Symbolically[END_REF][START_REF] Chatain | Factorization Properties of Symbolic Unfoldings of Colored Petri Nets[END_REF][START_REF] Chatain | Factorization Properties of Symbolic Unfoldings of Colored Petri Nets[END_REF], [START_REF] Reisig | Understanding Petri Nets -Modeling Techniques, Analysis Methods[END_REF][START_REF] Jensen | Coloured Petri Nets -Basic Concepts, Analysis Methods and Practical Use -Volume 1, Second Edition[END_REF][START_REF] Jensen | Coloured Petri Nets -Basic Concepts, Analysis Methods and Practical Use -Volume 1, Second Edition[END_REF], [START_REF] Reisig | Understanding Petri Nets -Modeling Techniques, Analysis Methods[END_REF][START_REF] Chatain | Factorization Properties of Symbolic Unfoldings of Colored Petri Nets[END_REF][START_REF] Chatain | Factorization Properties of Symbolic Unfoldings of Colored Petri Nets[END_REF], and in the last four lines.

Conclusions and Outlook

We introduced the notion of complete finite prefixes of symbolic unfoldings of high-level Petri nets. We identified a class of 1-safe high-level nets generalizing 1-safe P/T nets, for which we generalized the well-known algorithm by Esparza et al. to compute such a finite and complete prefix. This constitutes a consolidation and generalization of the concepts of [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF][START_REF] Chatain | Symbolic Unfoldings of High-Level Petri Nets and Application to Supervision of Distributed Systems[END_REF][START_REF] Chatain | Factorization Properties of Symbolic Unfoldings of Colored Petri Nets[END_REF][START_REF] Chatain | Symbolic Diagnosis of Partially Observable Concurrent Systems[END_REF]. While the resulting symbolic prefix has the same depth as a finite and complete prefix of the unfolding of the represented P/T net, it can be significantly smaller due to less branching. In the case of infinitely many reachable markings (where the original algorithm is not applicable) we identified the class of so-called symbolically compact nets for which an adapted version of the generalized algorithm works. For that, we showed how to check an adapted cut-off criterion by symbolically describing sets of markings. We implemented the generalized algorithm and tested it against four novel benchmark families. This experimentation validated a heuristic indicating the circumstances where the symbolic approach outperforms the low-level approach. This heuristic relies on the concept of a net property we call "mode determinism".

Future works include the construction of a symbolic reachability graph for symbolically compact nets and a comparison with the complete finite prefix, as outlined in Sec. 4.4. Additionally, a generalization for k-bounded high-level Petri nets seems possible. Furthermore, we want to apply the results to high-level Petri games [START_REF] Gieseking | High-Level Representation of Benchmark Families for Petri Games[END_REF][START_REF] Gieseking | Solving high-level Petri games[END_REF] to find "symbolic strategies" with techniques similar to [START_REF] Finkbeiner | Bounded Synthesis for Petri Games[END_REF] or [START_REF] Chatain | Characterization of Reachable Attractors Using Petri Net Unfoldings[END_REF][START_REF] Aguirre-Samboní | Avoid One's Doom: Finding Cliff-Edge Configurations in Petri Nets[END_REF], employing a successively increasing bound on size of the considered prefix of the symbolic unfolding.

according to ≪, and contains each transition t as often as there are events in E ′ with label t. We say p(E 1 ) ≪ p(E 2 ) if p(E 1 ) is lexicographically smaller than p(E 2 ) with respect to the order ≪.

The order ≺ E is then defined as follows: let C 1 , C 2 be two configurations of the symbolic unfoldings of a high-level Petri net. . The proof that ≺ E is an adequate order works exactly as in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF]:

It is easy to show that ≺ E is a well-founded partial order implied by inclusion. We now show that ≺ E is preserved by finite extensions. As already mentioned above, |D| = |φ We prove that ≺ F is a total adequate order. In the proof, (a) -(c) are taken directly from [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], with small adaptations due to the high-level formalism. While the ideas from (d) also come directly from [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], we have work with the monomorphism φ 2 1,D instead of the isomorphism I 2 1 , and the new definition of adequate order. This is where the only deviation from [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF] happens.

Let β = (O, h) be the symbolic unfolding of N = (N , M 0 ).

(a) ≺ F is a well-founded partial order.

This follows immediately from the fact that ≺ E is a well-founded partial order as is the lexicographic order on transition sequences of some fixed length. Low-level Unfolding of Fork And Join. Since the symbolic unfolding of any Fork And Join is structurally equal to the net itself we do not display it here. Fig. 11 shows the low-level unfolding with (n + 2)(m + 1) n + 1 nodes for a Fork And Join. Symbolic Unfolding of Water Pouring Puzzle. Figure 12 shows the complete finite prefix of the symbolic unfolding of the Water Pouring Puzzle from Fig. 6 with n = [START_REF] Nielsen | Petri Nets, Event Structures and Domains, Part I[END_REF][START_REF] Jensen | Coloured Petri Nets -Basic Concepts, Analysis Methods and Practical Use -Volume 1, Second Edition[END_REF] and m = 4, calculated by our implementation COLORUNFOLDER [START_REF] Panneke | [END_REF] of the generalized ERV-algorithm, Alg. 1. The figure is automatically produced from the output of COLORUNFOLDER. Cut-off events are marked by a red border. Additionally marked by a red border are the events representing the added goal transition that checks the target states. Since the net is mode deterministic, the symbolic unfolding's skeleton coincides with the low-level unfolding. Thus, the skeleton of the complete finite prefix in Figure 12 coincides with the complete finite prefix of the low-level unfolding generated by the original ERValgorithm from [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF].

Symbolic Unfolding of Mastermind. Figure 13 shows a prefix of the symbolic unfolding of the Mastermind net from Fig. 8 with 6 available colors, a code of length 4, and 12 possible attempts. Combinatorial arguments give that the low-level unfolding has more than 10 37 nodes, so we do not present it here.

  A safe high-level Petri net.

Figure 1 :

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

  b and placing a number k ∈ {1, . . . , m} on place c resp. d when firing in mode {x ← k}. The mode {x ← 0} is for both transitions excluded by their respective guard. When both α and β fired, the net arrived at a marking {| (c, k), (d, ℓ) | }. From there, ε can fire arbitrarily often, always replacing the colors k, ℓ currently residing on c, d by any colors 0 < k ′ , ℓ ′ ≤ m by firing in mode {x ← k, y ← ℓ, z ← k ′ , w ← ℓ ′ }. From every marking {| (c, k), (d, ℓ) | } satisfying ℓ = 3 • k, transition t can fire, ending the execution of the net.

)

  The flow relation is well-founded, i.e., ∀x ∈ B ∪ E : |{y | y ≤ x}| < ∞. iv) For every b ∈ B, exactly one of the following holds: a) ∀K 0 ∈ K 0 : c∈Col K 0 (b, c) = 1 and {e | e → b} = ∅. In this case we denote pre (b) = (⊥, v b ). b) ∀K 0 ∈ K 0 : c∈Col K 0 (b, c) = 0 and there exists a unique pair (e, v) s.t. (e, v, b) ∈ H. In this case we denote pre (b) = (e, v) We denote by B 0 = {b ∈ B | ∃K 0 ∈ K 0 ∃c ∈ Col : (b, c) ∈ K 0 } the conditions from iv.a) occupied in all initial cuts. ⊥ can be seen as a "special event" that fires only once to initialize the net, and produces the initial cuts K 0 ∈ K 0 by assigning values to the variables v b on "special arcs" (⊥, v b , b) towards the conditions b ∈ B 0 . In a crucial notation for this paper, we define in case iv.a) e(b) = ⊥, and v(b) = v b , and in case iv.b) we identify the event e by e(b) and the variable v by v(b). By this notation, ∀b ∈ B : pre (b) = (e(b), v(b)). We can say that whenever a condition b holds a color c, then it got placed there by firing e(b) in a mode that binds v(b) to the color c.

  by the index e, so that v e describes the value assigned to v by a mode of e. Having the definition of e(b) and v(b) from above in mind, for a condition b, we abbreviate v e (b) = v(b) e(b) . Formally, we have loc-pred (e) = ι(e)[v ← v e ] v∈Var (e) ∧ (b,v)∈pre (e) v e = v e (b) pred (e) = pred (⊥) ∧ e ′ ≤e loc-pred (e ′ ), where pred (⊥) = K 0 ∈K 0 (b,c)∈K 0 (v b ⊥ = c) symbolically represents the set of initial cuts. A symbolic branching process of a high-level Petri net N is a pair β = (O, h) with an occurrence net O = (Col , Var , B, E, H, ι, K 0 ) in which pred (e) is satisfiable for all e ∈ E, and an initial homomorphism h : O → N that is injective on events with the same preset, i.e., ∀e, e ′ ∈ E : (pre (e) = pre (e ′ ) ∧ h(e) = h(e ′ )) ⇒ e = e ′ .

Figure 2 :

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

  . The set {b 1 , b 2 , b 3 } is a co-set, since the conditions are neither in conflict, nor causally related, and b∈{b 1 ,b 2 ,b 3 } pred (e(b)),

  [e] := {e ′ ∈ E | e ′ ≤ e}. Additionally, we define the sets Var e := {v e | v ∈ Var (e)} and Var ⊥ := {v b ⊥ | b ∈ B 0 } of indexed variables, and for a set E ′ ⊆ E ∪ {⊥} we denote Var E ′ := e∈E ′ Var e . Note that, for every event e, pred (e) is a predicate over the variables Var [e]∪{⊥} .

Definition 1 . 5 .

 15 (Instantiation of Configuration) For a given configuration C, an instantiation of C is a function θ : Var C∪{⊥} → Col , such that ∀e ∈ C ∪ {⊥} : pred (e)[θ] ≡ true, i.e., it satisfies all predicates in the configuration. The set of instantiations of a given configurations C is denoted by Θ(C). Note that, by definition, every configuration C has an instantiation θ. We denote by cut(C, θ) := {(b, c) | b ∈ cut(C) ∧ θ(v e (b)) = c} ⊆ B × Col the cut of an "instantiated configuration", and by mark(C, θ) := {| (h(b), c) | (b, c) ∈ cut(C, θ) | } its marking. We collect both of these in K(C) := {cut(C, θ) | θ ∈ Θ(C)} and M(C) := {mark(C, θ) | θ ∈ Θ(C)}. Note that in this notation, for the empty configuration we have K(∅) = K 0 and M(∅) = M 0 .

Proposition 1 . 7 .

 17 The induction step is realized by Prop. 1.7. ⊓ ⊔ The symbolic unfolding Υ = (U, π) with events E of a high-level Petri net N = (P, T, F, ι, M 0 ) satisfies ∀C ∈ C(Υ ) ∀θ ∈ Θ(C) ∀t ∈ T ∀σ ∈ Σ(t) : mark(C, θ)[t, σ⟩ ⇔ ∃e ∈ E : π(e) = t ∧ cut(C, θ)[e, σ⟩.

  e) = {| (b, v) | (p, v) ∈ pre (t), π(b) = p, (b, θ(v e (b))) ∈ cut(C, θ) | }. Then we have pre (π( e)) = {| (π(b), v) | (b, v) ∈ pre ( e) | }. For every (p, v) ∈ post (t), we then add post (t)(p, v) conditions b with π(b) = p to B and add ( e, v, b) to H. We thus get post (π( e)) = {| (π(b), v) | (b, v) ∈ post ( e) | }. We now created a symbolic branching process bigger than Υ , contradicting that Υ is the symbolic unfolding. Assume on the other hand ∃e ∈ E : π(e) = t ∧ cut(C, θ)[e, σ⟩. Then pre (e, σ) ≤ cut(C, θ), and therefore, pre

Definition 2 . 1 .

 21 (Complete prefix) Let β = (O, h) be a prefix of the symbolic unfolding of a high-level Petri net N , with events E ′ . Then β is called complete if for every reachable marking M in N there exists C ∈ C(β) and θ ∈ Θ(C) s.t. i) M = mark(C, θ), and ii) ∀t ∈ T ∀σ ∈ Σ(t) : M [t, σ⟩ ⇒ ∃e ∈ E ′ : h(e) = t ∧ cut(C, θ)[e, σ⟩.

  and pred (e(b)) = pred . Definition 2.8. (Possible extensions) Let β = (O, h) be a branching process of a high-level Petri net N . The possible extensions PE (β) are the set of tuples e = (t, X, pred ) where t is a transition of N , and X ⊆ B × Var satisfying • {b | (b, v) ∈ X} is a co-set, and pre

  Fin, then it contains a cut-off event e 1 , and so C 1 = [e 1 ]⊕D for some set D of events. LetM 1 = mark([e 1 ].θ 1 | Var [e 1 ]∪{⊥} ) ∈ M([e 1 ]).By the definition of cut-off event, there exists an event e 2 with [e 2 ] ≺ [e 1 ] and M 1 ∈ M([e 2 ]). Since we have C 1 M 1 D, we get by Prop. 2.4 that the monomorphism φ 1 := φ [e 2 ] [e 1 ],D : O([e 1 ]|D) → ⇑[e 2 ] exists and that φ 1 (D) is a suffix of [e 2 ]. By Prop. 2.6 we know

  e) [θ ′ ] ≡ ι(t)[σ] ≡ true, and • (b,v)∈X v e = v e (b) [θ ′ ] ≡ (b,v)∈X σ(v) = θ(v e (b)) ≡ true, and • (b,v)∈X pred (e(b))[θ ′ ] ≡ (b,v)∈X pred (e(b))[θ] ≡ true, since θ ∈ Θ(C). Thus, pred [θ ′ ] ≡ true. Therefore, e = (t, X, pred ) is a possible extension and added in the execution of the algorithm. Then we directly have e / ∈ C, h(e) = t, and with the same arguments as in a), we get C ∪ {e} ∈ C(Fin) and θ ⊎ (σ • [v e → v] v∈Var (e) ) ∈ Θ(C ∪ {e}), which means cut(C, θ)[e, σ⟩. Since we chose θ independently of t and σ, this concludes the proof. ⊓ ⊔

Lemma 3 .

 3 1. ([4], Sec. 4.1) Υ(Exp(N )) ≃ Exp O (Υ (N )).

  Then, in Exp(O), the marking {| b.c | (b, c) ∈ K n | } is reachable from the initial marking {| b.c | (b, c) ∈ K 0 | } by the firing sequence (e 1 .σ 1 , . . . , e n .σ n ). Thus, there is a configuration C = {e 1 , . . . , e n } in U(Exp(O)) = Exp O (O) with ∀i : π O (e i ) = e i .σ i . Then, by the definition of h, we get mark h (C) := {| h(b) | b ∈ cut(C) | } = {| h(b).c | (b, c) ∈ K n | } = M. Let now t.σ ∈ T s.t. M[t.σ⟩. Then M [t, σ⟩. Since C, θ satisfy property b) from Def. 2.1, we know that ∃e ∈ E s.t. e / ∈ C, h(e) = t, and C, θ[e, σ⟩. This means, in Exp(β), we have {| b.c | (b, c) ∈ K n | }[e.σ⟩. Thus, there exists an e in U(Exp(β)) such that C[e⟩ and π O (e) = e.σ, which again means that h(e) = h(e).σ = t.σ. This proves that Exp O (β) is complete.

Figure 3 :

 3 Figure 3: The complete finite prefix of Υ(Exp(N )) of the running example N from Figure 1a calculated by the original ERV-Algorithm.

Definition 4 . 2 .

 42 (Class N SC ) A finite high-level Petri net N is called symbolically compact if it satisfies (1) and (2) from Def. 2.2, and (3*) There is a bound n ∈ N on the number of transition firings needed to reach all markings in R(N ).

1 (

 1 a) A symbolically compact net with Col = N.

Figure 4 :

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

Definition 4 .

 4 3. (Cut-off* event) Under the assumptions of Def. 2.7, the high-level event e is a cut-off* event (w.r.t. ≺) if M([e]) ⊆ C≺[e] M(C).

  ⊙ (b) by pred ⊙ (b) := pred (e(b)) ∧ (π(b) = v e (b)). This predicate now has (in an abuse of notation) an extra variable, called π(b). The remaining variables in pred (e(b)) are Var [e(b)]∪{⊥} . As we know, pred (e(b)) evaluates to true under an assignment θ : Var [e(b)]∪{⊥} → Col if and only if a concurrent execution of [e(b)] with the assigned modes is possible (i.e., under every instantiation of [e(b)]). In such an execution, θ(v e (b)) ∈ Col is placed on b. The predicate pred ⊙ (b) therefore can only be true if π(b) is assigned a color that can be placed on b.

  b∈cut(C) pred ⊙ (b) [ϑ θ ][θ] ≡ true and by the definition of κ(cut(C)) that κ(cut(C))[ϑ θ ] ≡ true, i.e., ϑ θ ∈ Ξ(cut(C)).

  = {0, . . . , m} (b) n = 4.

Figure 5 :

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

  goal i1 = 4 ∨ i2 = 4

Figure 6 :

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

Figure 7 :

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

code-maker 0 Figure 8 :

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

  Low-level, for growing number of places on x-axis, color class on y-axis and time as heatmap intensity. Symbolic, for growing number of places on xaxis and time on y-axis. Behavior is independent of the color class. This graph is for Col = N.

Figure 9 :

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

Figure 10 :

 10 Figure 10: Results for Hobbits And Orcs problem for a fixed boat capacity n in (a), (b), (c), and population with m of each Hobbits and Orcs on the x-axis. The orange line shows the time needed by the symbolic approach and the blue line shows the low-level approach.

C 1 ≺

 1 E C 2 holds if either |C 1 | < |C 2 |, or |C 1 | = |C 2 | and p(C 1 ) ≪ p(C 2 )

2 1 ,

 1 D (D)|. Additionally, we have p(D) = p(φ2 1,D (D)), since φ 2 1,D preserves the labeling of events.Assume C 1 ≺ E C 2 . If |C 1 | < |C 2 |, then |C 1 ⊕D| < |C 2 ⊕φ 2 1,D (D)|. If |C 1 | = |C 2 | and p(C 1 ) ≪ p(C 2 ), then |C 1 ⊕D| = |C 2 ⊕φ 2 1,D(D)| and, by the properties of the lexicographic order, p(C 1 ⊕D) ≪ p(C 2 ⊕φ 2 1,D (D)). The Total Adequate Order ≺ F . The Foata normal form FC of a configuration C is obtained by starting with FC empty, and iteratively deleting the set Min(C) from C and appending it to FC , until C is empty. Given two configurations C 1 , C 2 , we can compare their Foata normal forms FC 1 = C 11 . . . C 1n 1 and FC 2 = C 21 . . . C 2n 2 with respect to the order ≪ by saying FC 1 ≪ FC 2 if there exists i≤ i ≤ n 1 such that p(C 1j ) = p(C 2j ) for every 1 ≤ j < i, and p(C 1i ) ≪ p(C 2i ).Definition A.1. (Order ≺ F ) let C 1 and C 2 be two configurations of the symbolic unfolding of a high-level Petri net. C 1 ≺ F C 2 holds if • |C 1 | < |C 2 |, or • |C 1 | = |C 2 | and p(C 1 ) ≪ p(C 2 ), or • p(C 1 ) = p(C 2 ) and FC 1 ≪ FC 2 .

(b) C 1 ⊂

 1 C 2 implies C 1 ≺ F C 2 . This is obvious, since C 1 ⊂ C 2 implies |C 1 | < |C 2 |. (c) ≺ F is total.Assume that C 1 and C 2 are two incomparable configurations under ≺ F , i.e., |C 1 | = |C 2 |, p(C 1 ) = p(C 2 ), and p(FC 1 ) = p(FC 2 ). We prove C 1 = C 2 by induction on the common size k = |C 1 | = |C 2 |.

Figure 11 :

 11 Figure 11: The symbolic unfolding of a Fork And Join, depending on the parameters m and n.

Figure 12 :( c 1 1 retry( c 1 , c 2 , c 3 , c 4 ( c 1 , c 2 , c 3 , c 4

 121112341234 Figure 12: A prefix of the symbolic unfolding of the Water Pouring Puzzle for n = [3, 5] and m = 4, produced by COLORUNFOLDER.

Figure 13 :

 13 Figure 13: A prefix of the symbolic unfolding of the Mastermind net from Fig. 8.

  t. ≺ s.t. M ∈ M(C), and let t ∈ T , σ ∈ Σ(t) s.t. M [t, σ⟩. If C contains some cut-off event, then we can apply the arguments of a) to conclude that Fin contains a configuration C ′ ≺ C such that M ∈ M(C

′

). This contradicts the minimality of C. So C contains no cut-off events. Let θ ∈ Θ(C) s.t. M = mark(C, θ). Since pre (t.σ) ⊆ M , we have that there is a co-set B t,σ ⊆ cut(C) s.t. pre (t, σ)

Table 1 :

 1 Results of the Water Pouring Puzzle benchmark. For the Hobbits And Orcs benchmark we vary the and the capacity n of the boat fixed in Figures10a, 10b, 10c, and number the of each Hobbits and Orcs, m, plotted on the x-axis. We indicate the time needed by the low-level approach in blue and by the symbolic approach in orange, with a timeout of 3 minutes.

	buckets n 3, 5	target m 4	solvable yes, 6 steps	|B| 90	|E| 75	time low-level 95 ms	time symbolic 1.2 s
	15, 17	10	yes, 18 steps	258	195	220 ms	36 s
	57, 73	51	yes, 92 steps	1294	935	1.7 s	> 1 h
	9, 12	4	no	106	74	130 ms	1.8 s
	10, 16	5	no	190	134	140 ms	11 s
	8, 14, 17	2	yes, 4 steps	411	642	300 ms	26 s
	14, 26, 27	14	yes, 15 steps	21635	15279	7.7 s	> 1 h
	12, 15, 18	10	no	2391	1442	550 ms	20 min
	12, 21, 27	8	no	4029	2444	1.0 s	88 min
	Hobbits And Orcs.

Table 2 :

 2 Results of the Mastermind benchmark.

					Low-level		Symbolic
	k 12	n 4	m 6	time > 2 min	|B| -	|E| -	time 1 min	|B| 149	|E| 36
	1	3	3	86 ms	219	48	62 ms	14	3
	1	3	5	1.8 s	18363	3720	54 ms	14	3
	1	3	6	18 s	72723	14640	61 ms	14	3
	1	3	7	> 2 min	-	-	54 ms	14	3
	1	3	1000	> 2 min	-	-	53 ms	14	3
	1	4	4	1 s	3651	624	60 ms	17	3
	1	4	5	> 2 min	-	-	67 ms	17	3
	1	5	1000	> 2 min	-	-	77 ms	20	3
	1	28	1000	> 2 min	-	-	1 s	89	3
	2	3	3	215 ms	1719	438	206 ms	24	6
	2	3	4	3.3 s	110115	27672	120 ms	24	6
	2	3	5	111 s	1726443	432060	124 ms	24	6
		3	6	> 2 min	-	-	119 ms	24	6
	2	3	1000	> 2 min	-	-	127 ms	29	6
	2	4	4	5.5 s	137235	27672	1.3 s	29	6
	2	4	5	> 2 min	-	-	116 ms	29	6
	2	4	1000	> 2 min	-	-	162 ms	29	6
	2	10	1000	> 2 min	-	-	1 s	59	6
	3	4	4	> 2 min	-	-	35 s	41	9
	4	3	3	2.6 s	46719	12138	ms	44	12
	5	3	3	39 s	234219	60888	1.3 s	54	15
	6	3	3	> 2 min	-	-	1.8 s	64	18

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[START_REF] Chatain | Factorization Properties of Symbolic Unfoldings of Colored Petri Nets[END_REF].

N. Würdemann, T. Chatain, S. Haar, L. Panneke / Taking Complete Finite Prefixes To High Level, Symbolically

N. Würdemann, T. Chatain, S. Haar, L. Panneke / Taking Complete Finite Prefixes To High Level, Symbolically

https://smt-comp.github.io/2023/results/equality-nonlineararith-single-query

The problem is also known as "Missionaries and Cannibals", and is a variation of the "Jealous Husbands" problem.

The "Boat" icon used in Figure7ais by DinosoftLabs from Noun Project, https://thenounproject.com/ dinosoftlab/.

A. Appendix

A.1. Examples of adequate orders

We show that the adequate order used in [START_REF] Mcmillan | A Technique of State Space Search Based on Unfolding[END_REF], as well as the orders ≺ E and ≺ F treated in [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF], when lifted to the symbolic unfolding, are still adequate orders. In particular we show that ≺ F is a total adequate order on the symbolic unfolding, limiting the size of the later constructed finite prefix. The definition of these orders does not change, so we take most of the following notation directly from [START_REF] Esparza | An Improvement of McMillan's Unfolding Algorithm[END_REF].

The orders ≺ M and ≺ E . The order ≺ M used in [START_REF] Mcmillan | A Technique of State Space Search Based on Unfolding[END_REF] is defined by

For a high-level Petri net N , let ≪ be an arbitrary total order on the transitions of N . Given a set E ′ of events in the unfolding of N , let p(E ′ ) be that sequence of transitions which is ordered

The base case k = 0 gives C 1 = C 2 = ∅, so assume k > 0.

We first prove Min(C 1 ) = Min(C 2 ). Aiming a contradiction, assume w.l.o.g. that e 1 ∈ Min(C 1 ) \ Min(C 2 ). Since p(Min(C 1 )) = p(Min(C 2 )), Min(C 2 ) contains an event e 2 s.t. h(e 1 ) = h(e 2 ). Since →Min(C 1 ) and →Min(C 2 ) are subsets of B 0 , and all conditions of B 0 carry different labels, we have →e 1 = →e 2 , and thus, pre (e 1 ) = pre (e 2 ). This contradicts the definition of symbolic branching processes.

First, notice that we can assume D = {e}: For e ∈ Min(D) we have from Third, we show that under these two assumptions e is a minimal event of

Let e be minimal in C ′ 1 , i.e., the transition h(e) can be fired in a mode in one initial marking. Let p ∈ →h(e); then no condition in →C ∪C→ is labeled p, since these conditions would be concurrent to the p-labeled condition in →e, contradicting that (N , M 0 ) is safe. Thus, C 1 contains no event e ′ with p ∈ →h(e ′ ), and the same holds for C 2 , since p(C 1 ) = p(C 2 ). Therefore, the conditions in cut(C 2 ) with label in →h(e) are minimal conditions of β, and φ 2 1,D (e) = e is minimal in C ′ 2 . The reverse implication holds analogously, since about C 1 and C 2 we have only used the hypothesis p(C 1 ) = p(C 2 ).

With this knowledge, we now show the implication. Assume

2 ) and so we are done. If p(Min(C 1 )) = p(Min(C 2 )) and e ∈ Min(C ′ 1 ), then

) and e / ∈ Min(C ′ 1 ), we again argue that Min(C 1 ) = Min(C 2 ) and that, hence, C \ Min(C 1 ) and C 2 \ Min(C 1 ) are configurations of the branching process ⇑Min(C 1 ) of (N , M(Min(C 1 ))). With an inductive argument we get

and are also done in this case.

A.2. More Symbolic and Low-level Unfoldings

In this appendix we present unfoldings omitted in the main body of the paper.