11institutetext: Department of Computing Science, University of Oldenburg,
Oldenburg, Germany
11email<EMAIL_ADDRESS>
# Canonical Representations for Direct Generation of Strategies in High-level
Petri Games (Full Version)333This is an extended version of [20].††thanks:
This work was supported by the German Research Foundation (DFG) through the
Research Training Group (DFG GRK 1765) SCARE and through Grant Petri Games
(No. 392735815).

Manuel Gieseking  Nick Würdemann

###### Abstract

Petri games are a multi-player game model for the synthesis problem in
distributed systems, i.e., the automatic generation of local controllers. The
model represents causal memory of the players, which are tokens on a Petri net
and divided into two teams: the controllable system and the uncontrollable
environment. For one environment player and a bounded number of system
players, the problem of solving Petri games can be reduced to that of solving
Büchi games.

High-level Petri games are a concise representation of ordinary Petri games.
Symmetries, derived from a high-level representation, can be exploited to
significantly reduce the state space in the corresponding Büchi game. We
present a new construction for solving high-level Petri games. It involves the
definition of a unique, canonical representation of the reduced Büchi game.
This allows us to translate a strategy in the Büchi game directly into a
strategy in the Petri game. An implementation applied on six structurally
different benchmark families shows in most cases a performance increase for
larger state spaces.

##  1 Introduction

Whether telecommunication networks, electronic banking, or the world wide web,
_distributed systems_ are all around us and are becoming increasingly more
widespread. Though an entire system may appear as one unit, the local
controllers in a network often act autonomously on only incomplete information
to avoid constant communication. These independent agents must behave
correctly under all possible uncontrollable behavior of the environment.
_Synthesis_ [7] avoids the error-prone task of manually implementing such
local controllers by automatically generating correct ones from a given
specification (or stating the nonexistence of such controllers). In case of a
single process in the underlying model, synthesis approaches have been
successfully applied in nontrivial applications (e.g., [3], [25]). Due to the
incomplete information in systems with multiple processes progressing on their
individual rate, modeling _asynchronous distributed systems_ is even more
cumbersome and particularly benefits from a synthesis approach.

_Petri games_ [12] (based on an underlying Petri net [31] where the tokens are
the players in the game) are a well-suited multi-player game model for the
_synthesis of asynchronous distributed systems_ because of its subclasses with
comparably low complexity results. For Petri games with a single _environment_
(_uncontrollable_) player, a bounded number of _system_ (_controllable_)
players, and a _safety objective_ , i.e., all players have to avoid designated
_bad places_ , deciding the existence of a winning strategy for the system
players is exptime-complete [13]. This problem is called the _realizability
problem_. The result is obtained via a reduction to a two-player Büchi game
with enriched markings, so called _decision sets_ , as states.

_High-level Petri nets_ [24] can concisely model large distributed systems.
Correspondingly, _high-level Petri games_ [17] are a concise high-level
representation of ordinary Petri games. For solving high-level Petri games,
the _symmetries_ [33] of the system can be exploited to build a _symbolic
Büchi game_ with a significantly smaller number of states [18]. The states are
_equivalence classes_ of decision sets and called _symbolic decision sets_.
For generating a Petri game strategy for a high-level Petri game the approach
proposed in [18] resorts to the original strategy construction in [13], i.e.,
the equivalence classes of a symbolic two-player strategy are dissolved and a
strategy for the standard two-player game is generated. Figure 1 shows the
relation of the elements just described.

High-levelPetri game $\mathit{G}$Petri
game$\mathsf{G}=\mathsf{L}(\mathit{G})$Symbolictwo-playergame
$\mathcal{G}(\mathit{G})$Two-playergame $\mathcal{G}(\mathsf{G})$Strategyin
$\mathcal{G}(\mathit{G})$Strategyin $\mathcal{G}(\mathsf{G})$Strategy
$\sigma$in
$\mathsf{G}$transform[17]reduce[13]solverepresentbisimilar[18]reduce[18]solvegenerate[18]translate[13]Symbolic
gamewith canon. rep.$\mathcal{G}(\mathit{G})^{c}$Strategyin
$\mathcal{G}(\mathit{G})^{c}$reduceSec. 3,4solvegenerateSec.
4$3$$4$$A$$\simeq$$\simeq$ Figure 1:  An overview of the scope of this paper.
The connections between the different elements describe their interplay and
where these methods are introduced. The connections labeled with “solve” mean
that a two-player (Büchi) game can be solved by standard algorithms in game
theory (e.g., [21]). The bottom level corresponds to the original reduction in
[13], the level above corresponds to the high-level counterparts described in
[17, 18], and the top level contains the elements introduced in this paper.
The new reduction is marked by thick edges.

In this paper, we propose a new construction for solving high-level Petri
games to avoid this detour while generating the strategy. In [18] the symbolic
Büchi game is generated by comparing each newly added state with all already
added ones for equivalence, i.e., the _orbit problem_ must be answered. The
new approach calculates a _canonical representation_ for each newly added
state (the _constructive orbit problem_ [8]), and only stores these
representations. This generation of a symbolic Büchi game with canonical
representations is based on the corresponding ideas for reachability graphs
from [5]. As in [18], we consider safe Petri games with a high-level
representation, and exclude Petri games where the system can proceed
infinitely without the environment. For the decidability result we consider,
as in [13], Petri games with only one environment player, i.e., in every
reachable marking there is at most one token on an environment place.

One of the main advantages of the new approach is that the canonical
representations allow to directly generate a Petri game strategy from a
symbolic Büchi game strategy without explicitly resolving all symmetries (cp.
thick edges in Fig. 1).

$\mathit{Env}$$\mathit{d}$$\mathit{I}$$\mathit{inf}$$\mathit{R}$$\mathit{h}$$\mathit{H}$$\mathit{Sys}$$\mathit{a}$$\mathit{A}$$\mathit{b}$$\mathit{B}$$C_{1}$$\bullet$$x$$x$$C_{1}$$x$$C_{1}$$y$$(y,x)$$x$$C_{1}\\!\times\\!\\{x\\}$$x$$(y,x)$$y$$C_{1}=\\{c_{1},c_{2},c_{3}\\}$$C_{2}=\\{\bullet\\}$$x,y\in
C_{1}$ ((a)) High-level Petri game $\mathit{G}$

$\mathit{Env}$$\mathit{d}_{2}$$\mathit{I}_{2}$$\mathit{inf}_{2}$$\mathit{Sys}_{2}$$\mathit{a}_{22}$$\mathit{a}_{21}$$\mathit{a}_{23}$$\mathit{A}_{22}$$\mathit{A}_{21}$$\mathit{A}_{23}$$\mathit{R}_{2}$$\mathit{h}_{2}$$\mathit{H}_{2}$$\mathit{b}_{22}$$\mathit{b}_{21}$$\mathit{b}_{23}$$\mathit{B}_{2}$$\mathit{d}_{1}$$\mathit{I}_{1}$$\mathit{inf}_{1}$$\mathit{Sys}_{1}$$\mathit{a}_{12}$$\mathit{a}_{11}$$\mathit{a}_{13}$$\mathit{A}_{12}$$\mathit{A}_{11}$$\mathit{A}_{13}$$\mathit{R}_{1}$$\mathit{h}_{1}$$\mathit{H}_{1}$$\mathit{b}_{12}$$\mathit{b}_{11}$$\mathit{b}_{13}$$\mathit{B}_{1}$$\mathit{d}_{3}$$\mathit{I}_{3}$$\mathit{inf}_{3}$$\mathit{Sys}_{3}$$\mathit{a}_{32}$$\mathit{a}_{31}$$\mathit{a}_{33}$$\mathit{A}_{32}$$\mathit{A}_{31}$$\mathit{A}_{33}$$\mathit{R}_{3}$$\mathit{h}_{3}$$\mathit{H}_{3}$$\mathit{b}_{32}$$\mathit{b}_{31}$$\mathit{b}_{33}$$\mathit{B}_{3}$
((b)) The represented P/T Petri game $\mathsf{G}=\mathsf{L}(\mathit{G})$.

Figure 2:  _Client/Server_ : The environment decides on one out of three
computers to host a server. The system players (computers) can win the game by
getting informed on the decision of the environment and connecting correctly.

Another advantage is the complexity for constructing the symbolic Büchi game.
Even though, the calculation of the canonical representation comes with a
fixed cost, less comparisons can be necessary, depending on the input system.
We implemented the new algorithm and applied our tool on the benchmark
families used in [18] and Example 1. The results show in general a performance
increase with an increasing number of states for most of the benchmark
families.

We now introduce the example on which we demonstrate the successive
development stages of the presented techniques throughout the paper.

###### Example 1

The high-level Petri game $\mathit{G}$ depicted in Fig. 2(a) models a
simplified scenario where one out of three computers must host a server for
the others to connect to. The environment nondeterministically decides which
computer must be the host. The places in the net are partitioned into _system
places_ (gray) and _environment places_ (white). An object on a place is a
player in the corresponding team. _Bad places_ are double-bordered. The
variables $x,y$ on arcs are bound only locally to the transitions, and an
assignment of objects to these variables is called a _mode_ of the transition.

The environment player $\bullet$, initially residing on place $\mathit{Env}$,
decides via transition $d$ in mode $x=\tilde{c}$ on a computer $\tilde{c}$
that should host the server. The system players (computers
$c_{1},c_{2},c_{3}\in C_{1}$), initially residing on place $\mathit{Sys}$, can
either directly, individually connect themselves to another computer via
transition $\mathit{a}$, or wait for transition $\mathit{inf}$ to be enabled.
When they choose to connect themselves directly, after firing transition
$\mathit{a}$ in different modes, the corresponding pairs of computers reside
on place $\mathit{A}$. Since the players always have to give the possibility
to proceed in the game, and transition $\mathit{h}$ cannot get enabled any
more, they must take transition $\mathit{b}$ to the bad place $\mathit{B}$. So
instead, all players should initially only allow transition $\mathit{inf}$ (in
every possible mode $x$). After the decision of the environment, transition
$\mathit{inf}$ can be fired in mode $x=\tilde{c}$, placing $\tilde{c}$ on
$\mathit{R}$. In this firing, the system players get informed on the
environment’s decision. Back on place $\mathit{Sys}$ they can, equipped with
this knowledge, each connect to the computer $\tilde{c}$ via transition
$\mathit{a}$, putting the three objects
$(c_{1},\tilde{c}),(c_{2},\tilde{c}),(c_{3},\tilde{c})$ on place $\mathit{A}$.
Thus, transition $\mathit{h}$ can be fired in mode $\tilde{c}$, and the game
terminates with $\tilde{c}$ in $\mathit{H}$. Since the system players avoided
reaching the bad place $\mathit{B}$, they win the play. This scenario is
highly symmetric, since it does not matter which computer is chosen to be the
host, as long as the others connect themselves correctly.

The remainder of this paper is structured as follows: In Sec. 2 we recall the
definitions of (high-level) Petri nets and (high-level) Petri games. In Sec. 3
we present the idea, formalization, and construction of canonical
representations. In Sec. 4 we show the application of these canonical
representations in the symbolic two-player Büchi game, and how to directly
generate a Petri game strategy. In Sec. 5, experimental results of the
presented techniques are shown. Section 6 presents the related work and Sec. 7
concludes the paper.

##  2 Petri Nets and Petri Games

This section recalls (high-level) Petri nets and -games, and the associated
concept of strategies established in [13, 17, 18]. Figure 2 serves as an
illustration.

###  2.1 P/T Petri Nets

A (marked P/T) _Petri net_ is a tuple
$\mathsf{N}=(\mathsf{P},\mathsf{T},\mathsf{F},\mathsf{M}_{\mathsf{0}})$, with
the disjoint sets of _places_ $\mathsf{P}$ and _transitions_ $\mathsf{T}$, a
_flow function_
$\mathsf{F}:(\mathsf{P}\times\mathsf{T})\cup(\mathsf{T}\times\mathsf{P})\to\mathbb{N}$,
and an _initial marking_ $\mathsf{M}_{\mathsf{0}}$, where a _marking_ is a
multi-set $\mathsf{M}:\mathsf{P}\to\mathbb{N}$ that indicates the number of
tokens on each place. $\mathsf{F}(\mathsf{x},\mathsf{y})=n>0$ means there is
an _arc_ of _weight_ $n$ from node $\mathsf{x}$ to $\mathsf{y}$ describing the
flow of tokens in the net. A transition $\mathsf{t}\in\mathsf{T}$ is _enabled_
in a marking $\mathsf{M}$ if
$\forall\mathsf{p}\in\mathsf{P}:\mathsf{F}(\mathsf{p},\mathsf{t})\leq\mathsf{M}(\mathsf{p})$.
If $\mathsf{t}$ is enabled then $\mathsf{t}$ can _fire_ in $\mathsf{M}$,
leading to a new marking $\mathsf{M}^{\prime}$ calculated by
$\forall\mathsf{p}\in\mathsf{P}:\mathsf{M}^{\prime}(\mathsf{p})=\mathsf{M}(\mathsf{p})-\mathsf{F}(\mathsf{p},\mathsf{t})+\mathsf{F}(\mathsf{t},\mathsf{p})$.
This is denoted by $\mathsf{M}[\mathsf{t}\rangle\mathsf{M}^{\prime}$.
$\mathsf{N}$ is called _safe_ if for all markings $\mathsf{M}$ that can be
reached from $\mathsf{M}_{0}$ by firing a sequence of transitions we have
$\forall\mathsf{p}\in\mathsf{P}:\mathsf{M}(\mathsf{p})\leq 1$. For each
transition $\mathsf{t}\in\mathsf{T}$ we define the _pre-_ and _postset_ of
$\mathsf{t}$ as the multi-sets
$\mathit{pre}(\mathsf{t})=\mathsf{F}(\cdot,\mathsf{t})$ and
$\mathit{post}(\mathsf{t})=\mathsf{F}(\mathsf{t},\cdot)$ over $\mathsf{P}$.

An example for a Petri net can be seen in Fig. 2(b). Ignoring the different
shades and potential double borders for now, the net’s places are depicted as
circles, transitions as squares. Dots represent the number of tokens on each
place in the initial marking of the net. The flow is depicted as weighted arcs
between places and transitions. Missing weights are interpreted as arcs of
weight $1$. In the initial marking, all transitions $\mathit{a}_{ij}$ and
$\mathit{d}_{i}$ are enabled. Firing, e.g., $\mathit{d}_{1}$ results in the
marking with one token on $\mathit{I}_{1}$, $\mathit{Sys}_{1}$,
$\mathit{Sys}_{2}$, and $\mathit{Sys}_{3}$, each.

###  2.2 P/T Petri Games

Petri games are an extension of Petri nets to incomplete information games
between two teams of players: the controllable system vs. the uncontrollable
environment. The tokens on places in a Petri net represent the individual
players. The place a player resides on determines their team membership.
Particularly, a player can switch teams. For that, the places are divided into
system places and environment places. A play of the game is a concurrent
execution of transitions in the net. During a play, the _knowledge_ of each
player is represented by their _causal history_ , i.e., all visited places and
used transitions to reach to current place. Players enrich this local
knowledge when synchronizing in a joint transition. Then the complete
knowledge of all participating players are exchanged. Based on this, players
allow or forbid transitions in their postset. A transition can only fire if
every player in its preset allows the execution. The system players in a Petri
game win a play if they satisfy a safety-condition, given by a designated set
of bad places they must not reach.

Formally, a (P/T) _Petri game_ is a tuple
$\mathsf{G}=(\mathsf{P}_{\mathsf{S}},\mathsf{P}_{\mathsf{E}},\mathsf{T},\mathsf{F},\mathsf{M}_{\mathsf{0}},\mathsf{P}_{\mathsf{B}})$,
with a set of _system places_ $\mathsf{P}_{\mathsf{S}}$, a set of _environment
places_ $\mathsf{P}_{\mathsf{E}}$, and a set of _bad places_
$\mathsf{P}_{\mathsf{B}}\subseteq\mathsf{P}_{\mathsf{S}}$. The set of all
places is denoted by
$\mathsf{P}=\mathsf{P}_{\mathsf{S}}\dot{\cup}\mathsf{P}_{\mathsf{E}}$, and
$\mathsf{T},\mathsf{F},\mathsf{M}_{0}$ are the remaining components of a Petri
net $\mathsf{N}=(\mathsf{P},\mathsf{T},\mathsf{F},\mathsf{M}_{\mathsf{0}})$,
called the _underlying net_ of $\mathsf{G}$. We consider only Petri games with
finitely many places and transitions.

In Fig. 2(b), a Petri game is depicted. We just introduced the underlying net
of the game. The system places are shaded gray, the environment places are
white. Bad places are marked by a double border. This Petri game is the
P/T-version of the high-level Petri game described in the introduction. The
three tokens/system players residing on $\mathit{Sys}_{i}$ represent the
computers. The environment player residing on $\mathit{Env}$ makes their
decision which computer should host a server by taking a transition
$\mathit{d}_{i}$. The system players can then get informed of the decision and
react accordingly as described above.

A _strategy_ for the system players in a Petri game $\mathsf{G}$ can be
formally expressed as a _sub-process_ of the _unfolding_ [10]: in the
unfolding of a Petri net, every loop is unrolled and every backward branching
place is expanded by duplicating the place, so that every transition
represents the unique occurrence of a transition during an execution of the
net. The causal dependencies in $\mathsf{G}$ (and thus, the knowledge of the
players) are naturally represented in its unfolding, which is the unfolding of
the underlying net with system-, environment-, and bad places marked
correspondingly.

A strategy is obtained from the unfolding by deleting some of the branches
that are under control of the system players. This sub-process has to meet
three conditions: (i) The strategy must be _deadlock-free_ , to avoid trivial
solutions; it must allow the possibility to continue, whenever the system can
proceed. Otherwise the system players could win with the respect to the safety
objective (bad places) if they decide to do nothing. (ii) The system players
must act in a _deterministic_ way, i.e., in no reachable marking of the
strategy two transitions involving the same system player are enabled. (iii)
_Justified refusal:_ if a transition is not in the strategy, then the reason
is that a system player in its preset forbids all occurrences of this
transition in the strategy. Thus, no pure environment decisions are
restricted, and system players can only allow or forbid a transition of the
original net, based on only their knowledge. In a _winning_ strategy, the
system players cannot reach bad places.

In Fig. 3, we see the already informally described winning strategy for the
system players in the Petri game $\mathsf{G}$. For clarity, we only show the
case in which the environment chose the first computer to be the host
completely. All computers, _after_ getting informed of the environment’s
decision, act correspondingly and connect to the first computer. The remaining
branches in the unfolding are cut off in the strategy. The other two cases
(after firing $\mathit{inf}_{2}$ or $\mathit{inf}_{3}$) are analogous. We
include the formal definitions of unfoldings and strategies in App. 0.A.

$\mathit{Env}$$\mathit{d}_{2}$$\mathit{I}_{2}$$\mathit{inf}_{2}$$\mathit{d}_{1}$$\mathit{I}_{1}$$\mathit{inf}_{1}$$\mathit{Sys}_{2}$$\mathit{a}_{22}$$\mathit{a}_{21}$$\mathit{a}_{23}$$\mathit{A}_{22}$$\mathit{A}_{21}$$\mathit{A}_{23}$$\mathit{b}_{22}$$\mathit{b}_{21}$$\mathit{b}_{23}$$\mathit{B}_{2}$$\mathit{B}_{2}$$\mathit{B}_{2}$$\mathit{Sys}_{1}$$\mathit{a}_{12}$$\mathit{a}_{11}$$\mathit{a}_{13}$$\mathit{A}_{12}$$\mathit{A}_{11}$$\mathit{A}_{13}$$\mathit{R}_{1}$$\mathit{h}_{1}$$\mathit{H}_{1}$$\mathit{b}_{12}$$\mathit{b}_{11}$$\mathit{b}_{13}$$\mathit{B}_{1}$$\mathit{B}_{1}$$\mathit{B}_{1}$$\mathit{d}_{3}$$\mathit{I}_{3}$$\mathit{inf}_{3}$$\mathit{Sys}_{3}$$\mathit{a}_{32}$$\mathit{a}_{31}$$\mathit{a}_{33}$$\mathit{A}_{32}$$\mathit{A}_{31}$$\mathit{A}_{33}$$\mathit{b}_{32}$$\mathit{b}_{31}$$\mathit{b}_{33}$$\mathit{B}_{3}$$\mathit{B}_{3}$$\mathit{B}_{3}$$\mathit{Sys}_{1}$$\mathit{a}_{12}$$\mathit{a}_{11}$$\mathit{a}_{13}$⋮⋮⋮$\mathit{Sys}_{2}$$\mathit{a}_{22}$$\mathit{a}_{21}$$\mathit{a}_{23}$⋮⋮⋮$\mathit{Sys}_{3}$$\mathit{a}_{32}$$\mathit{a}_{31}$$\mathit{a}_{33}$⋮⋮⋮⋮⋮⋮
Figure 3:  Part of a winning strategy for the system players in $\mathsf{G}$
(solid), obtained by deleting some of the branches of the unfolding (solid and
greyed out).

###  2.3 High-Level Petri Nets

While in P/T Petri nets only tokens can reside on places, in high-level Petri
nets each place is equipped with a _type_ that describes the form of data
(also called _colors_) the place can hold. Instead of weights, each arc
between a place $p$ and a transition $t$ is equipped with an _expression_ ,
indicating which of these colors are taken from or laid on $p$ when firing
$t$. Additionally, each transition $t$ is equipped with a _guard_ that
restricts when $t$ can fire.

Formally, a _high-level_ Petri net is a tuple
$\mathit{N}=(\mathit{P},\mathit{T},\mathit{F},\mathit{ty},\mathit{e},\mathit{g},\mathit{M}_{0})$,
with a set of _places_ $\mathit{P}$, a set of _transitions_ $\mathit{T}$
satisfying $\mathit{P}\cap\mathit{T}=\emptyset$, a _flow relation_
$\mathit{F}\subseteq(\mathit{P}\times\mathit{T})\cup(\mathit{T}\times\mathit{P})$,
a _type function_ $\mathit{ty}$ from $\mathit{P}$ such that for each place
$p$, $\mathit{ty}(p)$ is the set of colors that can lie on $p$, a mapping
$\mathit{e}$ that, for every transition $t$, assigns to each arc $(p,t)$ (or
$(t,p)$) in $\mathit{F}$ an expression $\mathit{e}(p,t)$ (or
$\mathit{e}(t,p)$) indicating which colors are withdrawn from $p$ (or laid on
$p$) when $t$ is fired, a _guard function_ $\mathit{g}$ that equips each
transition $t$ with a Boolean expression $\mathit{g}(t)$, an _initial marking_
$\mathit{M}_{0}$, where a _marking_ in $\mathit{N}$ is a function $\mathit{M}$
with domain $\mathit{P}$ indicating what colors reside on each place, i.e.,
$\forall p\in\mathit{P}:\mathit{M}(p)\in[\mathit{ty}(p)\to\mathbb{N}]$.

Fig. 2(a) a high-level Petri net is depicted. As in the P/T case, we ignore
the different shadings and borders of places for now. The types of the places
can be deducted from the surrounding arcs. For example, the place $\mathit{E}$
has the type $\mathit{ty}(\mathit{E})=C_{2}=\\{\bullet\\}$, and the place
$\mathit{A}$ has the type $\mathit{ty}(\mathit{A})=C_{1}\times C_{1}$. Each
arc is equipped with an expression, e.g.,
$\mathit{e}(\mathit{Sys},\mathit{a})=y$, and
$\mathit{e}(\mathit{a},\mathit{A})=(y,x)$. In the given net, all guards of
transitions are _true_ and therefore not depicted.

Typically, expressions and guards will contain variables. A _mode_ (or
valuation) $v$ of a transition $t\in\mathit{T}$ assigns to each variable $x$
occurring in $\mathit{g}(t)$, or any expression $\mathit{e}(p,t)$ or
$\mathit{e}(t,p)$, a value $v(x)$. The set $\mathit{Val}(t)$ contains all
modes of $t$. Each $v\in\mathit{Val}(t)$ assigns a Boolean value, denoted by
$v(t)$, to $g(t)$, and to each arc expression $e(p,t)$ or $e(t,p)$ a multi-set
over $\mathit{ty}(p)$, denoted by $v(p,t)$ or $v(t,p)$. A transition $t$ is
_enabled in a mode_ $v\in\mathit{Val}(t)$ in a marking $\mathit{M}$ if
$v(t)=\mathit{true}$ and for each arc $(p,t)\in\mathit{F}$ and every
$c\in\mathit{ty}(p)$ we have $v(p,t)(c)\leq\mathit{M}(p)(c)$. The marking
$\mathit{M}^{\prime}$ reached by firing $t$ in mode $v$ from $\mathit{M}$
(denoted by $\mathit{M}[t.v\rangle\mathit{M}^{\prime}$) is calculated by
$\forall p\in\mathsf{P}\ \forall
c\in\mathit{ty}(p):\mathit{M}^{\prime}(p)(c)=\mathit{M}(p)(c)-v(p,t)(c)+v(t,p)(c)$.

A high-level Petri net $\mathit{N}$ can be _transformed_ into a P/T Petri net
$\mathsf{L}(\mathit{N})$ with
$\mathsf{P}=\\{p.c\,|\,p\in\mathit{P},c\in\mathit{ty}(p)\\}$,
$\mathsf{T}=\\{t.v\,|\,t\in\mathit{T},v\in\mathit{Val}(t),v(t)=\mathit{true}\\}$,
the flow $\mathsf{F}$ defined by $\forall p.c\in\mathsf{P}\ \forall
t.v\in\mathsf{T}:\mathsf{F}(p.c,t.v)=v(p,t)(c)\land\mathsf{F}(t.v,p.c)=v(t,p)(c)$,
and initial marking $\mathsf{M}_{\mathsf{0}}$ defined by $\forall
p.c\in\mathsf{P}:\mathsf{M}_{\mathsf{0}}(p.c)=\mathit{M}_{0}(p)(c)$. The two
nets then have the same semantics: the number of tokens on a place $p.c$ in a
marking in $\mathsf{L}(\mathit{N})$ indicates the number of colors $c$ on
place $p$ in the corresponding marking in $\mathit{N}$. Firing a transition
$t.v$ in $\mathsf{L}(\mathit{N})$ corresponds to firing transition $t$ in mode
$v$ in $\mathit{N}$. We say a high-level Petri net $\mathit{N}$ _represents_
the P/T Petri net $\mathsf{L}(\mathit{N})$.

###  2.4 High-Level Petri Games

Just as P/T Petri games are structurally based on P/T Petri nets, a _high-
level Petri game_
$\mathit{G}=(\mathit{P}_{S},\mathit{P}_{E},\mathit{T},\mathit{F},\mathit{ty},\mathit{e},\mathit{g},\mathit{M}_{0},\mathit{P}_{B})$
with _underlying high-level net_
$\mathit{N}=(\mathit{P},\mathit{T},\mathit{F},\mathit{ty},\mathit{e},\mathit{g},\mathit{M}_{0})$
divides the places $\mathit{P}$ into _system places_ $\mathit{P}_{S}$ and
_environment places_ $\mathit{P}_{E}$. The set
$\mathit{P}_{B}\subseteq\mathit{P}_{S}$ indicates the bad places. High-level
Petri games represent P/T Petri games: a high-level Petri game $\mathit{G}$
(with underlying high-level net $\mathit{N}$) _represents_ a P/T Petri game
$\mathsf{L}(\mathit{G})$ with underlying P/T Petri net
$\mathsf{L}(\mathit{N})$. The classification of places $p.c$ in
$\mathsf{L}(\mathit{G})$ into system-, environment-, and bad places
corresponds to the places $p$ in the high-level game.

In Fig. 2, a high-level Petri game $\mathit{G}$ and its represented Petri game
$\mathsf{G}=\mathsf{L}(\mathit{G})$ are depicted. For the sake of clarity, we
abbreviated the nodes in $\mathsf{L}(\mathit{G})$. Thus, e.g., the transition
$\mathit{a}.[x=c_{1},y=c_{2}]$ is renamed to $\mathit{a}_{12}$. We often use
notation from the represented P/T Petri game to express situations in a high-
level game.

##  3 Canonical Representations of Symbolic Decision Sets

In this paper, we investigate for a given high-level Petri game $\mathit{G}$
with one environment player whether the system players in
$\mathsf{L}(\mathit{G})$ have a winning strategy (and possibly generate one).
This problem is solved via a reduction to a symbolic two-player Büchi game
$\mathcal{G}(\mathit{G})^{c}$. The general idea of this reduction is, as in
[13], to equip the markings of the Petri game with a set of transitions for
each system player (called _commitment sets_) which allows the players to fix
their next move. In the generated Büchi game, only a subset of all
interleavings is taken into account, in the way that the moves of the
environment player are delayed until no system player can progress without
interacting with the environment. By that, each system player gets informed
about the environment’s last position during their next move. This means that
in every state, every system player knows the current position of the
environment or learns it in the next step, before determining their next move.
Thus, the system players can be considered to be completely informed about the
game. This is only possible due to the existence of only one environment
player. For more environment players such interleavings would not ensure that
each system player is informed (or gets informed in their next move) about all
environment positions. The nodes of the game are called _decision sets_. In
[18], symmetries in the Petri net are exploited to define equivalence classes
of decision sets, called _symbolic decision sets_. These are used to create an
equivalent, but significantly smaller, Büchi game.

In this section we introduce the new canonical representations of symbolic
decision sets which serve as nodes for the new Büchi game. We transfer
relations between and properties of (symbolic) decision sets to the
established canonical representations. We start by recalling the definitions
of symmetries in Petri nets [33] and of (symbolic) decision sets [18].

From now on we consider high-level Petri games $\mathit{G}$ representing a
safe P/T Petri game $\mathsf{L}(\mathit{G})$ that has one environment player,
a bounded number of system players with a safety objective, and where the
system cannot proceed infinitely without the environment.

###  3.1 Symmetric Nets

High-level representations are often created using _symmetries_ [33] in a
Petri net. Conversely, in some high-level nets, symmetries can be read
directly from the given specification. A class of nets which allow this are
the so called _symmetric nets_ (SN) [4].111Symmetric Nets were formerly known
as Well-Formed Nets (WNs). The renaming was part of the ISO standardization
[23]. In symmetric nets, the types of places are selected from given (finite)
_basic color classes_ $C_{1},\dots,C_{n}$. For every place $p\in\mathit{P}$,
we have
$\mathit{ty}(p)=C_{1}^{p_{1}}\\!\times\\!\cdots\\!\times\\!C_{n}^{p_{n}}$ for
natural numbers $p_{1},\dots,p_{n}\in\mathbb{N}$, where $C_{i}^{p_{i}}$
denotes the $p_{i}$-fold Cartesian product of $C_{i}$.222 In the Cartesian
products $\mathit{ty}(p)$ and $\mathit{Val}(t)$, we omit all $C_{i}^{x}$ with
$x=0$ (empty sets). The possible values of variables contained in guards and
arc expressions are also basic classes. Thus, the modes of each transition
$t\in\mathit{T}$ are also given by a Cartesian product
$\mathit{Val}(t)=C_{1}^{t_{1}}\\!\times\\!\cdots\\!\times\\!C_{n}^{t_{n}}$.
Guards and arc expressions treat all elements in a color class equally.

###### Example 2

The underlying high-level net $\mathit{N}$ in Fig. 2 is a symmetric net with
basic color classes $C_{1}=\\{c_{1},c_{2},c_{3}\\}$ and $C_{2}=\\{\bullet\\}$.
We have, e.g., $\mathit{Val}(a)=C_{1}\\!\times C_{1}$ (the two coordinates
representing $y$ and $x$), and therefore, $a_{1}=2,a_{2}=0$.

###### Remark 1

In general, each basic color class $C_{i}$ is possibly partitioned into
_subclasses_ $C_{i}=\bigcup_{q=1}^{n_{i}}C_{i,q}$. In the main body of this
paper, we omit this partition. The detailed proofs in the appendix take the
general case into account.

###### Proposition 1

Any high-level Petri net can be transformed into a SN with the same basic
structure, same place types, and equivalent arc labeling (cf. [4]).

The _symmetries_ $\xi_{\mathit{N}}$ in a symmetric net $\mathit{N}$ are all
tuples $s=(s_{1},\dots,s_{n})$ such that each $s_{i}$ is a permutation on
$C_{i}$. A symmetry $s$ can be applied to a single color $c\in C_{i}$ by
$s(c)=s_{i}(c)$. The application to tuples, e.g., colors on places or
transition modes, is defined by the application in each entry. The set
$\xi_{\mathit{N}}$, together with the function composition $\circ$, forms a
group with identity $(\mathit{id}_{C_{i}})_{i=1}^{n}$. In the represented P/T
Petri net $\mathsf{L}(\mathit{N})$, symmetries can be applied to places
$\mathsf{p}=p.c\in\mathsf{P}$ and transitions $\mathsf{t}=t.v\in\mathsf{T}$ by
defining $s(p.c)=p.s(c)$ and $s(t.v)=t.s(v)$. The structure of symmetric nets
ensures $\forall s\in\xi_{\mathit{N}}\
\forall\mathsf{t}\in\mathsf{T}:\mathit{pre}(s(\mathsf{t}))=s(\mathit{pre}(\mathsf{t}))$
and $\mathit{post}(s(\mathsf{t}))=s(\mathit{post}(\mathsf{t}))$. Thus,
symmetries are compatible with the firing relation; $\forall
s\in\xi_{\mathit{N}}:\mathsf{M}[\mathsf{t}\rangle\mathsf{M}^{\prime}\Leftrightarrow
s(\mathsf{M})[s(\mathsf{t})\rangle s(\mathsf{M}^{\prime})$. In a symmetric
net, we can w.l.o.g. assume the initial marking $\mathit{M}_{0}$ to be
_symmetric_ , i.e., $\forall
s\in\xi_{\mathit{N}}:s(\mathit{M}_{0})=\mathit{M}_{0}$.

###  3.2 Symbolic Decision Sets

A _decision set_ is a set
$D\subseteq\mathsf{P}\\!\times\\!(\mathbb{P}(\mathsf{T})\cup\top)$. An element
$(\mathsf{p},\mathsf{C})\in D$ with
$\mathsf{C}\subseteq\mathit{post}(\mathsf{p})$ indicates there is a player on
place $\mathsf{p}$ who allows all transitions in $\mathsf{C}$ to fire.
$\mathsf{C}$ is then called a _commitment set_. An element
$(\mathsf{p},\top)\in D$ indicates the player on place $\mathsf{p}$ has to
choose a commitment set in the next step. The step of this decision is called
_$\top$ -resolution_.

In a $\top$-resolution, each $\top$-symbol in a decision set $D$ is replaced
with a suitable commitment set. This relation is denoted by $D[\top\rangle
D^{\prime}$. If there are no $\top$-symbols in $D$, a transition $\mathsf{t}$
is _enabled_ , if $\forall\mathsf{p}\in\mathit{pre}(\mathsf{t})\
\exists(\mathsf{p},\mathsf{C})\in D:\mathsf{t}\in\mathsf{C}$, i.e., there is a
token on every place in $\mathit{pre}(\mathsf{t})$ (as for markings) and
additionally, $\mathsf{t}$ is in every commitment set of such a token. In the
process of firing an enabled transition, the tokens are moved accordingly to
the flow $\mathsf{F}$. The moved or generated tokens on system places are then
equipped with a $\top$-symbol, while the tokens on environment places allow
_all_ transitions that they are involved in. This relation is denoted by
$D[\mathsf{t}\rangle D^{\prime}$. The _initial decision set_ is given by
$D_{0}=\\{(\mathsf{p},\\{\mathsf{t}\in\mathsf{T}\,|\,\mathsf{p}\in\mathit{pre}(\mathsf{t})\\})\,|\,\mathsf{p}\in\mathsf{P}_{\mathsf{E}}\cap\mathsf{M}_{\mathsf{0}}\\}\cup\\{(\mathsf{p},\top)\,|\,\mathsf{p}\in\mathsf{P}_{\mathsf{S}}\cap\mathsf{M}_{\mathsf{0}}\\}$,
i.e., the environment in the initial marking allows all possible transitions,
the system players still have to choose a commitment set.

###### Example 3

Assume in the Petri game in Fig. 2(a) that the computers initially allow
transition $\mathit{inf}$ in every mode. The environment player on
$\mathit{Env}$ fires transition $\mathit{d}$ in mode $c_{1}$. After that, the
system gets informed of the environment’s decision via transition
$\mathit{inf}$ in mode $c_{1}$. The system players, now back on
$\mathit{Sys}$, decide via $\top$-resolution they all want to assign
themselves to $c_{1}$. This corresponds to the following sequence of decision
sets, where we abbreviate $\mathit{Sys}$ by $\mathit{S}$.

$D_{0}$$\left(\mathit{Env}.\bullet,\\{\mathit{d}.c_{1},\mathit{d}.c_{2},\mathit{d}.c_{3}\\}\right)$$\left(\mathit{S}.c_{1},\\{\mathit{inf}\\!.c_{1},\mathit{inf}\\!.c_{2},\mathit{inf}\\!.c_{3}\\}\right)$$\left(\mathit{S}.c_{2},\\{\mathit{inf}\\!.c_{1},\mathit{inf}\\!.c_{2},\mathit{inf}\\!.c_{3}\\}\right)$$\left(\mathit{S}.c_{3},\\{\mathit{inf}\\!.c_{1},\mathit{inf}\\!.c_{2},\mathit{inf}\\!.c_{3}\\}\right)$$\left(\mathit{I}.c_{1},\\{\mathit{inf}\\!.c_{1}\\}\right)$$\left(\mathit{S}.c_{1},\\{\mathit{inf}\\!.c_{1},\mathit{inf}\\!.c_{2},\mathit{inf}\\!.c_{3}\\}\right)$$\left(\mathit{S}.c_{2},\\{\mathit{inf}\\!.c_{1},\mathit{inf}\\!.c_{2},\mathit{inf}\\!.c_{3}\\}\right)$$\left(\mathit{S}.c_{3},\\{\mathit{inf}\\!.c_{1},\mathit{inf}\\!.c_{2},\mathit{inf}\\!.c_{3}\\}\right)$$\left(\mathit{R}.c_{1},\\{g.c_{1}\\}\right)$$\left(\mathit{S}.c_{1},\top\right)$$\left(\mathit{S}.c_{2},\top\right)$$\left(\mathit{S}.c_{3},\top\right)$$\left(\mathit{R}.c_{1},\\{g.c_{1}\\}\right)$$\left(\mathit{S}.c_{1},\\{a.(c_{1},c_{1})\\}\right)$$\left(\mathit{S}.c_{2},\\{a.(c_{2},c_{1})\\}\right)$$\left(\mathit{S}.c_{3},\\{a.(c_{3},c_{1})\\}\right)$$\top$$\mathit{d}.c_{1}$$\mathit{inf}.c_{1}$$\top$

A high-level Petri game $\mathit{G}$ has the same symmetries
$\xi_{\mathit{N}}$ as its underlying symmetric net $\mathit{N}$. They can be
applied to decision sets by applying them to every occurring color $c$ or mode
$v$. For a decision set $D$, an equivalence class
$\\{s(D)\,|\,s\in\xi_{\mathit{N}}\\}$ is called the _symbolic decision set_ of
$D$, and contains symmetric situations in the Petri game. In [18], these
equivalence classes replace individual decision sets in the two-player Büchi
game to achieve a substantial state space reduction.

###### Example 4

Consider the second to last decision set in the sequence above. This situation
is symmetric to the cases where the environment chose computer $c_{2}$ or
$c_{3}$ as the host. In the example $\mathit{G}$, we have the two color
classes $C_{1}$ and $C_{2}$. Since $|C_{2}|=1$, the only permutation on
$C_{2}$ is $\mathit{id}_{C_{2}}$. Thus, the symmetries in $\mathit{G}$ are the
permutations on $C_{1}$. Symmetries transform the elements in the symbolic
decision set into each other. The corresponding symbolic decision set contains
the following three elements $D$, $D^{\prime}$, and $D^{\prime\prime}$:

$\left(\mathit{R}.c_{1},\\{g.c_{1}\\}\right)$$\left(\mathit{S}.c_{1},\top\right)$$\left(\mathit{S}.c_{2},\top\right)$$\left(\mathit{S}.c_{3},\top\right)$$\left(\mathit{R}.c_{2},\\{g.c_{2}\\}\right)$$\left(\mathit{S}.c_{1},\top\right)$$\left(\mathit{S}.c_{2},\top\right)$$\left(\mathit{S}.c_{3},\top\right)$$\left(\mathit{R}.c_{3},\\{g.c_{3}\\}\right)$$\left(\mathit{S}.c_{1},\top\right)$$\left(\mathit{S}.c_{2},\top\right)$$\left(\mathit{S}.c_{3},\top\right)$$\mathit{id}_{C_{1}}$$c_{2}\leftrightarrow
c_{3}$$c_{1}\leftrightarrow c_{2}$$c_{1}\mapsto c_{2}\mapsto c_{3}\mapsto
c_{1}$$c_{1}\leftrightarrow c_{3}$$c_{1}\mapsto c_{3}\mapsto c_{2}\mapsto
c_{1}$$D$$D^{\prime}$$D^{\prime\prime}$

Each edge between two decision sets corresponds to the application of a
symmetry. The abbreviated notation $c\mapsto c^{\prime}\mapsto
c^{\prime\prime}\mapsto c$ means that each element is mapped to the next in
line. Analogously, $c\leftrightarrow c^{\prime}$ means that $c$ and
$c^{\prime}$ are switched.

###  3.3 Canonical Representations

In order to exploit symmetries to reduce the size of the state space, one aims
to consider only one representative of each of the equivalence classes induced
by the symmetries. This can be done either by checking whether a newly
generated state is equivalent to any already generated one, or by transforming
each newly generated state into an equivalent, canonical representative. In
[18] we consider the former approach. The nodes of the symbolic Büchi game are
symbolic decision sets. In the construction, an arbitrary representative
$\overline{D}$ is chosen for each of these equivalence classes. This means,
when reaching a new node $D^{\prime}$, we must apply every symmetry $s$ to
test whether there already is a representative
$\overline{D^{\prime}}=s(D^{\prime})$, or whether $D^{\prime}$ is in a new
symbolic decision set.

In this section, we now aim at the second approach and define the new
_canonical representations_ of symbolic decision sets. For that, we first
define _dynamic representations_ , and then show how to construct a canonical
one. We use these instead of (arbitrary representatives of) symbolic decision
sets in the construction of the symbolic Büchi game in Sec. 4.

####  3.3.1 Dynamic Representations

A dynamic representation is an abstract description of a symbolic decision
set. It consists of dynamic subclasses of variables, and a dynamic decision
set where these dynamic subclasses replace explicit colors. Any (valid)
assignment of values to the variables in the dynamic subclasses results in a
decision set in the equivalence class.

Formally, a _dynamic representation_ is a tuple
$\mathscr{R}=(\mathcal{C},\mathcal{D})$, with the set of _dynamic subclasses_
$\mathcal{C}=\\{Z_{i}^{j}\,|\,1\leq i\leq n,1\leq j\leq m_{i}\\}$ for natural
numbers $m_{i}$, and a _dynamic decision set_ $\mathcal{D}$. A dynamic
subclass $Z_{i}^{j}$ contains a finite number of variables with values in
$C_{i}$. Each $Z_{i}^{j}$ has a cardinality $|Z_{i}^{j}|$ that indicates the
number of variables. In total, there are as many variables with values in
$C_{i}$ as there are colors, i.e., $\sum_{j=1}^{m_{i}}|Z_{i}^{j}|=|C_{i}|$. An
_assignment_ $\mathit{va}:\bigcup_{i=1}^{n}C_{i}\to\mathcal{C}$ is _valid_ if
it respects the cardinality of dynamic subclasses, i.e., ${|\\{c\in
C_{i}\,|\,\mathit{va}(c)=Z_{i}^{j}\\}|}=|Z_{i}^{j}|$. Every valid assignment
of colors $c\in C_{i}$ to the $Z_{i}^{j}$, $1\leq j\leq m_{i}$, gives a
partition of $C_{i}$. A dynamic decision set is the same as a decision set,
with dynamic subclasses replacing explicit colors. For every decision set $D$
in a symbolic decision set with dynamic representation
$\mathscr{R}=(\mathcal{C},\mathcal{D})$, there is a valid assignment
$\mathit{va}_{D}$ such that $D=\mathit{va}_{D}^{-1}(\mathcal{D})$. In general,
there are several dynamic representations of a symbolic decision set.

###### Example 5

Consider the symbolic decision set from the last example. We can naively build
a dynamic representation by taking one of the decision sets, and replacing
each color by a dynamic subclass of cardinality $1$. This results in as many
dynamic subclasses as there are colors, i.e.,
$\mathcal{C}=\\{Z_{1}^{1},Z_{1}^{2},Z_{1}^{3},Z_{2}^{1}\\}$ with
$|Z_{i}^{j}|=1$ for all $i,j$. Below, the resulting dynamic decision set
$\mathcal{D}$ is depicted, with valid assignments that lead to elements $D$,
$D^{\prime}$, and $D^{\prime\prime}$.

$\left(\mathit{R}.Z_{1}^{1},\\{g.Z_{1}^{1}\\}\right)$$\left(\mathit{S}.Z_{1}^{1},\top\right)$$\left(\mathit{S}.Z_{1}^{2},\top\right)$$\left(\mathit{S}.Z_{1}^{3},\top\right)$$\left(\mathit{R}.c_{1},\\{g.c_{1}\\}\right)$$\left(\mathit{S}.c_{1},\top\right)$$\left(\mathit{S}.c_{2},\top\right)$$\left(\mathit{S}.c_{3},\top\right)$$\left(\mathit{R}.c_{2},\\{g.c_{2}\\}\right)$$\left(\mathit{S}.c_{1},\top\right)$$\left(\mathit{S}.c_{2},\top\right)$$\left(\mathit{S}.c_{3},\top\right)$$\left(\mathit{R}.c_{3},\\{g.c_{3}\\}\right)$$\left(\mathit{S}.c_{1},\top\right)$$\left(\mathit{S}.c_{2},\top\right)$$\left(\mathit{S}.c_{3},\top\right)$$Z_{1}^{j}\mathrel{\reflectbox{$\mapsto$}}c_{j}$$Z_{1}^{2}\mathrel{\reflectbox{$\mapsto$}}c_{1},Z_{1}^{1}\mathrel{\reflectbox{$\mapsto$}}c_{2},$$Z_{1}^{3}\mathrel{\reflectbox{$\mapsto$}}c_{3}$$Z_{1}^{3}\mathrel{\reflectbox{$\mapsto$}}c_{1},Z_{1}^{2}\mathrel{\reflectbox{$\mapsto$}}c_{2},$$Z_{1}^{1}\mathrel{\reflectbox{$\mapsto$}}c_{3}$$\mathcal{D}$$D$$D^{\prime}$$D^{\prime\prime}$

The element $(\mathit{R}.Z_{1}^{1},\\{g.Z_{1}^{1}\\})$, e.g., represents one
arbitrary color $c$ (since $|Z_{1}^{1}|=1$) on place $\mathit{R}$ with $g.c$
in its commitment set. The same color is on place $\mathit{S}$, equipped with
a $\top$-symbol.

####  3.3.2 Minimality

We notice in the example above that $Z_{1}^{2}$ and $Z_{1}^{3}$ appear in the
same contexts in $\mathcal{D}$. The _context_ $\operatorname{con}(Z_{i}^{j})$
of a dynamic subclass $Z_{i}^{j}$ is defined as the set of tuples in
$\mathcal{D}$ where exactly one appearance of $Z_{i}^{j}$ is replaced by a
symbol $\triangledown$. So in our example
$\operatorname{con}(Z_{1}^{2})=\\{(\mathit{S}.\triangledown,\top)\\}=\operatorname{con}(Z_{1}^{3})$,
and
$\operatorname{con}(Z_{1}^{1})=\\{(\mathit{S}.\triangledown,\top),(\mathit{R}.\triangledown,\mathit{g}.c_{1}),(\mathit{R}.c_{1},\mathit{g}.\triangledown)\\}$.
This means $Z_{1}^{2}$ and $Z_{1}^{3}$ can be _merged_ into a new dynamic
subclass of cardinality $2$. The resulting new dynamic representation is given
by $\mathcal{C}_{\mathit{min}}=\\{Z_{1}^{1},Z_{1}^{2},Z_{2}^{1}\\}$ with
$|Z_{1}^{1}|=|Z_{2}^{1}|=1$ and $|Z_{1}^{2}|=2$, and
$\mathcal{D}_{\mathit{min}}=\left\\{(\mathit{R}.Z_{1}^{1},\\{g.Z_{1}^{1}\\}),(\mathit{S}.Z_{1}^{1},\top),(\mathit{S}.Z_{1}^{2},\top)\right\\}$.

$\left(\mathit{R}.Z_{1}^{1},\\{g.Z_{1}^{1}\\}\right)$$\left(\mathit{S}.Z_{1}^{1},\top\right)$$\left(\mathit{S}.Z_{1}^{2},\top\right)$$\left(\mathit{R}.c_{1},\\{g.c_{1}\\}\right)$$\left(\mathit{S}.c_{1},\top\right)$$\left(\mathit{S}.c_{2},\top\right)$$\left(\mathit{S}.c_{3},\top\right)$$\left(\mathit{R}.c_{2},\\{g.c_{2}\\}\right)$$\left(\mathit{S}.c_{1},\top\right)$$\left(\mathit{S}.c_{2},\top\right)$$\left(\mathit{S}.c_{3},\top\right)$$\left(\mathit{R}.c_{3},\\{g.c_{3}\\}\right)$$\left(\mathit{S}.c_{1},\top\right)$$\left(\mathit{S}.c_{2},\top\right)$$\left(\mathit{S}.c_{3},\top\right)$$Z_{1}^{j}\mathrel{\reflectbox{$\mapsto$}}c_{1}$$Z_{1}^{2}\mathrel{\reflectbox{$\mapsto$}}c_{2},c_{3}$$Z_{1}^{1}\mathrel{\reflectbox{$\mapsto$}}c_{2}$$Z_{1}^{2}\mathrel{\reflectbox{$\mapsto$}}c_{1},c_{3},$$Z_{1}^{1}\mathrel{\reflectbox{$\mapsto$}}c_{3}$$Z_{1}^{2}\mathrel{\reflectbox{$\mapsto$}}c_{1},c_{2},$$\mathcal{D}_{\mathit{min}}$$D$$D^{\prime}$$D^{\prime\prime}$

_Minimal representations_ do not contain any two dynamic subclasses
$Z_{i}^{j},Z_{i}^{k}$ with the same context. Given a dynamic representation,
it is algorithmically simple to construct a minimal representation of the same
symbolic decision set by merging all dynamic subclasses with the respectively
same context. The dynamic representation above that resulted from merging the
subclasses is therefore minimal. Still, minimality is not enough to obtain a
unique canonical representation, since we can permute the indices $j$ of the
dynamic subclasses $Z_{i}^{j}$.

###### Lemma 1

The minimal representations of a symbolic decision set are unique up to a
permutation of the dynamic subclasses.

This lemma can be proved using the observation that every minimal
representation can be reached from a dynamic representation that contains only
dynamic subclasses of cardinality $1$ (as the one in Example 5) by merging.

####  3.3.3 Ordering

We can choose one of the minimal representations by _ordering_ the dynamic
subclasses. In the following, we give a possible way to do that. We display
the dynamic decision set $\mathcal{D}$ as a matrix, with rows and columns
indicating (tuples of) dynamic subclasses $Z$. An element of the matrix at
entry $(Z,Z^{\prime})$ returns all tuples $(p,t)$ satisfying
$(p.Z,\mathsf{C})\in\mathcal{D}$ and $t.Z^{\prime}\in\mathsf{C}$ for a
commitment set $\mathsf{C}$. Also, all tuples $(p,\top)$ satisfying
${(p.Z,\top)\in\mathcal{D}}$ and all tuples $(p,\emptyset)$ satisfying
$(p.Z,\emptyset)\in\mathcal{D}$ are returned (in these cases, $Z^{\prime}$ is
neglected).

The elements of the matrix are in
$\mathbb{P}(\mathsf{P}\\!\times\\!(\mathsf{T}\cup\\{\top,\emptyset\\}))$.
Since this set is finite, we can give an arbitrary, but fixed, total order on
it. This order can be extended to the matrices over the set (the lexicographic
order by row-wise traversion through a matrix). Then we can determine a
permutation such that, when applied to the dynamic subclasses, the matrix is
_minimal with respect to the lexicographic order_. The corresponding dynamic
representation is called _ordered_.

###### Example 6

On the left we see the matrix of the dynamic decision set $\mathcal{D}$ in the
minimal representation given above. The first entry, at
$(Z_{1}^{1},Z_{1}^{1})$, e.g., is
$\\{(\mathit{S},\top),(\mathit{R},\mathit{g})\\}$ since
$(\mathit{S}.Z_{1}^{1},\top)$ and
$(\mathit{R}.Z_{1}^{1},\mathit{g}.Z_{1}^{1})$ are in $\mathcal{D}$. Assume
$\\{(\mathit{S},\top)\\}<\\{(S,\top),(\mathit{R},g)\\}$. When the permutation
switching $Z_{1}^{1}$ and $Z_{1}^{2}$ is applied, we get the right matrix,
which is lexicographically smaller (the first entry is smaller).

| $Z_{1}^{1}$ | $Z_{1}^{2}$
---|---|---
$Z_{1}^{1}$ | $\\{(\mathit{S},\top),(\mathit{R},\mathit{g})\\}$ | $\\{(\mathit{S},\top)\\}$
$Z_{1}^{2}$ | $\\{(\mathit{S},\top)\\}$ | $\\{(\mathit{S},\top)\\}$

$\overset{Z_{1}^{1}\leftrightarrow
Z_{1}^{2}}{\qquad\longleftarrow\\!\longrightarrow\qquad}$ $Z_{1}^{1}$
$Z_{1}^{2}$ $Z_{1}^{1}$ $\\{(\mathit{S},\top)\\}$ $\\{(\mathit{S},\top)\\}$
$Z_{1}^{2}$ $\\{(\mathit{S},\top)\\}$
$\\{(\mathit{S},\top),(\mathit{R},\mathit{g})\\}$

Thus, the minimal representation from above is transformed into a _minimal and
ordered_ representation
$(\mathcal{C}_{\mathit{ord}},\mathcal{D}_{\mathit{ord}})$ by the permutation
$Z_{1}^{1}\leftrightarrow Z_{1}^{2}$.

###### Theorem 3.1

For every symbolic decision set there is exactly one minimal and ordered
dynamic representation. We call this the _canonical_ (dynamic) representation.

The proof follows from Lemma 1 and the observation that if two ordered dynamic
representations can be transformed into each other by applying a permutation
of the dynamic subclasses, they must have the same dynamic decision set.

We can algorithmically order a minimal representation by calculating all
symmetric representations and finding the one with the lexicographically
smallest matrix. These are maximally $|\xi_{\mathit{N}}|$ comparisons of
dynamic representations. So by first making a dynamic representation minimal,
and then ordering it, we get the respective canonical representation.

###### Corollary 1

We can construct the canonical representation of a given symbolic decision set
in $O(|\xi_{\mathit{N}}|)$.

###  3.4 Relations between Canonical Representations

Between decision sets, we have the two relations $D[\top\rangle D^{\prime}$
and $D[t.v\rangle D^{\prime}$ with
$v\in\mathit{Val}(t)=C_{1}^{t_{1}}\\!\times\\!\cdots\\!\times\\!C_{n}^{t_{n}}$.
In canonical representations, we abstract from specific colors $c\in C_{i}$
and replace them by dynamic subclasses $Z_{i}^{j}$ of variables. However, in
the process of $\top$-resolution or transition firing, two objects represented
by the same dynamic subclass can act differently. This means we _instantiate_
special objects in the classes that are relevant in the $\top$-resolution or
transition firing.

For this, each dynamic subclass $Z_{i}^{j}$ in a canonical representation
$\mathscr{R}$ is _split_ into finitely many $Z_{i}^{j,k}$ of cardinality
$|Z_{i}^{j,k}|=1$ with $k>0$, and a subclass $Z_{i}^{j,0}$, containing the
possibly remaining, non-instantiated, variables. Then, a $\top$ is resolved,
or a transition is fired, with the dynamic subclasses $Z_{i}^{j,k}$ replacing
explicit data entries $c\in C_{i}$. Finally, the canonical representation
$\mathscr{R}^{\prime}$ of the reached dynamic representation is found. These
relations are denoted by $\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$ and
$\mathscr{R}[t.Z\rangle\mathscr{R}^{\prime}$, where $Z$ is a tuple of
instantiated $Z_{i}^{j,k}$.

Below we see an example that corresponds to the last two steps in Example 3.
We calculated the second canonical representation in the last section. It is
reached from the first canonical representation by firing
$\mathit{inf}\\!.Z_{1}^{2,1}$. In this process one (the only) element in
$Z_{1}^{2}$ is instantiated by a dynamic subclass $Z_{1}^{2,1}$ of cardinality
$1$. After the actual firing, the reached representation is made canonical.
Then, a $\top$ is resolved. Here, $Z_{1}^{1}$ is split into $Z_{1}^{1,1}$ and
$Z_{1}^{1,2}$ with $|Z_{1}^{1,1}|=|Z_{1}^{1,2}|=1$. In the reached dynamic
representation, no two subclasses have the same context, so it is already
minimal. After ordering we get the canonical representation.

$\left(\mathit{I}.Z_{1}^{2},\\{\mathit{inf}\\!.Z_{1}^{2}\\}\right)$$\left(\mathit{S}.Z_{1}^{1},\\{\mathit{inf}\\!.Z_{1}^{1},\mathit{inf}\\!.Z_{1}^{2}\\}\right)$$\left(\mathit{S}.Z_{1}^{2},\\{\mathit{inf}\\!.Z_{1}^{1},\mathit{inf}\\!.Z_{1}^{2}\\}\right)$$|Z_{1}^{1}|=2$$|Z_{1}^{2}|=1$$\left(\mathit{R}.Z_{1}^{1},\\{g.Z_{1}^{2}\\}\right)$$\left(\mathit{S}.Z_{1}^{1},\top\right)$$\left(\mathit{S}.Z_{1}^{2},\top\right)$$|Z_{1}^{1}|=2$$|Z_{1}^{2}|=1$$\left(\mathit{R}.Z_{1}^{3},\\{g.Z_{1}^{3}\\}\right)$$\left(\mathit{S}.Z_{1}^{1},\\{a.(Z_{1}^{1},Z_{1}^{3})\\}\right)$$\left(\mathit{S}.Z_{1}^{2},\\{a.(Z_{1}^{2},Z_{1}^{3})\\}\right)$$\left(\mathit{S}.Z_{1}^{3},\\{a.(Z_{1}^{3},Z_{1}^{3})\\}\right)$$\forall
j\in\\{1,2,3\\}:$$|Z_{1}^{j}|=2$$\mathit{inf}.(Z_{1}^{2,1})$$\top$

###### Theorem 3.2

Every relation $D[t.v\rangle D^{\prime}$ or $D[\top\rangle D^{\prime}$ between
two decision sets $D$ and $D^{\prime}$ is represented by exactly one symbolic
relation $\mathscr{R}[t.Z\rangle\mathscr{R}^{\prime}$ or
$\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$ between the respective canonical
representations $\mathscr{R}$ and $\mathscr{R}^{\prime}$.

The proof for the case $D[t.v\rangle D^{\prime}$ follows by applying a valid
assignment $\mathit{va}_{D}$ to $v$ and splitting $\mathscr{R}$
correspondingly. The case $D[\top\rangle D^{\prime}$ works analogously.

###  3.5 Properties of Canonical Representations

The goal is to use canonical representations instead of individual decision
sets or (arbitrary representatives of) symbolic decision sets as nodes in a
two player game. The edges $(\mathscr{R},\mathscr{R}^{\prime})$ in this game
are built from relations $\mathscr{R}[t.Z\rangle\mathscr{R}^{\prime}$ and
$\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$, depending on the properties of
$\mathscr{R}$. For example, if $\mathscr{R}$ describes nondeterministic
situations in the Petri game, then the edges from $\mathscr{R}$ are built in
such a way that player 0 (representing the system) cannot win the game from
there. In this section, we define the relevant properties of canonical
representations.

In [13], the following properties of a decision set $D$ are defined. Let
$\mathsf{M}(D)=\\{\mathsf{p}\in\mathsf{P}\,|\,(\mathsf{p},\top)\in
D\lor\exists\mathsf{C}\subseteq\mathsf{T}:(\mathsf{p},\mathsf{C})\in D\\}$ be
the _underlying marking_ of $D$. $D$ is _environment-dependent_ iff $\neg
D[\top\rangle$, i.e., there is no $\top$ symbol in any tuple in $D$, and
$\forall\mathsf{t}\in\mathsf{T}:D[\mathsf{t}\rangle\Rightarrow\mathit{pre}(\mathsf{t})\cap\mathsf{P}_{\mathsf{E}}\neq\emptyset$,
i.e., all enabled transitions have an environment place in their preset. $D$
_contains a bad place_ iff
$\mathsf{P}_{\mathsf{B}}\cap\mathsf{M}(D)\neq\emptyset$. $D$ is a _deadlock_
iff $\neg D[\top\rangle$, and
$\exists\mathsf{t}^{\prime}\in\mathsf{T}:\mathsf{M}(D)[\mathsf{t}^{\prime}\rangle\land\forall\mathsf{t}\in\mathsf{T}:\neg
D[\mathsf{t}\rangle$, i.e., there is a transition that is enabled in the
underlying marking, but the system forbids all enabled transitions. $D$ is
_terminating_ iff
$\forall\mathsf{t}\in\mathsf{T}:\neg\mathsf{M}(D)[\mathsf{t}\rangle$. $D$ is
_nondeterministic_ iff
$\exists\mathsf{t}_{1},\mathsf{t}_{2}:\mathsf{t}_{1}\neq\mathsf{t}_{2}\land\mathsf{P}_{\mathsf{S}}\cap\mathit{pre}(\mathsf{t}_{1})\cap\mathit{pre}(\mathsf{t}_{2})\neq\emptyset\land
D[\mathsf{t}_{1}\rangle\land D[\mathsf{t}_{2}\rangle$, i.e., two separate
transitions sharing a system place in their presets both are enabled.

In [18], we showed that all decision sets in one equivalence class share the
same of the properties defined above. Thus, we say a symbolic decision set has
one of the above properties iff its individual members have the respective
property.

We now define these properties for canonical representations. Since we do not
want to consider individual decision sets, we do that on the level of dynamic
representations. Let $\mathscr{R}=(\mathcal{C},\mathcal{D})$ be a canonical
representation. $\mathscr{R}$ is _environment-dependent_ iff
$\neg\mathscr{R}[\top\rangle$, i.e., there is no $\top$ symbol in any tuple in
$\mathcal{D}$, and $\forall t.Z:\mathscr{R}[t.Z\rangle\Rightarrow\exists
p\in\mathit{P}_{E}:(p,t)\in\mathit{F}$, and $\mathscr{R}$ _contains a bad
place_ iff $\exists p\in\mathit{P}_{B}\,\exists
X:(p.X,\top)\in\mathscr{R}\lor\exists\mathsf{C}:(p.X,\mathsf{C})\in\mathcal{D}$.
Both these properties are rather analogous to the respective property of
decision sets. For termination and deadlocks, we introduce for the given
$\mathscr{R}$ the representation $\mathscr{R}_{\mathit{all}}$ with the same
dynamic subclasses, and the dynamic decision set where every player has all
possible transitions $t.Z$ in their commitment set. Since then all transitions
that could fire in the underlying marking are enabled, this substitutes for
$\mathsf{M}(D)$. We say $\mathscr{R}$ is a _deadlock_ iff
$\neg\mathscr{R}[\top\rangle$, and $\exists
t^{\prime}.Z^{\prime}:\mathscr{R}_{\mathit{all}}[t^{\prime}.Z^{\prime}\rangle\land\forall
t.Z:\mathscr{R}[t.Z\rangle$. Analogously, $\mathscr{R}$ is _terminating_ iff
$\forall t.Z:\neg\mathscr{R}_{\mathit{all}}[t.Z\rangle$. For nondeterminism we
have to consider two cases. The first one is analogous to the property for
individual decision sets. $\mathit{ndet}_{1}(\mathscr{R})=\exists
t.Z,t^{\prime}.Z^{\prime}:t.Z\neq t^{\prime}.Z^{\prime}\land\exists
p\in\mathit{P}_{S}\,\exists X,\mathsf{C}:(p.X,\mathsf{C})\in\mathcal{D}\land
t.Z,t^{\prime}.Z^{\prime}\in\mathsf{C}\land\mathscr{R}[t,Z\rangle\land\mathscr{R}[t^{\prime}.Z^{\prime}\rangle$.
The second case considers the situation that _two instances_ of one $t.Z$ can
both fire with a shared system place in their preset.
$\mathit{ndet}_{2}(\mathscr{R})=\exists t.Z\,\exists
p\in\mathit{P}_{S}\,\exists X,\mathsf{C}:(p.X,\mathsf{C})\in\mathcal{D}\land
t.Z\in\mathsf{C}\land\exists Z_{i}^{j,k}\in
Z:|Z_{i}^{j}|>1\land\mathscr{R}[t,Z\rangle$. Finally, $\mathscr{R}$ is
_nondeterministic_ iff
$\mathit{ndet}_{1}(\mathscr{R})\lor\mathit{ndet}_{2}(\mathscr{R})$.

###### Corollary 2

The properties of a symbolic decision set and its canonical representation
coincide.

For the proof, Theorem 3.2 is applied to the properties of individual decision
sets.

##  4 Applying Canonical Representations

In this section, we define for a high-level Petri game $\mathit{G}$ the two-
player Büchi game $\mathcal{G}(\mathit{G})^{c}$ with canonical representations
$\mathscr{R}$ of symbolic decision sets, rather than arbitrary representative
$\overline{D}$ as in [18]. The edges between nodes are directly implied by the
relations $\mathscr{R}[t.Z\rangle\mathscr{R}^{\prime}$ and
$\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$ between canonical
representations. This allows to _directly_ generate a winning strategy for the
system players in $\mathsf{G}$ from a winning strategy for player 0 in
$\mathcal{G}(\mathit{G})^{c}$ (cf. Fig. 1).

###  4.1 The Symbolic Two-Player Game

We reduce a Petri game $\mathsf{G}$ with high-level representation
$\mathit{G}$ to a two-player Büchi game $\mathcal{G}(\mathit{G})^{c}$. The
goal is to directly create a strategy $\sigma$ for the system players in
$\mathsf{G}$ from a strategy $f$ for player 0 in
$\mathcal{G}(\mathit{G})^{c}$. Recall that a Petri game strategy must be
deadlock-free, deterministic, and satisfy the justified refusal condition.
Additionally, to be winning, it must not contain bad places.

The nodes in $\mathcal{G}(\mathit{G})^{c}$ are canonical representations of
symbolic decision sets, equivalence classes of situations in the Petri game.
The properties of canonical representations defined in Sec. 3.5 characterize
these situations. These properties are used in the construction of the game.
As in [13, 18], the environment in the game $\mathcal{G}(\mathit{G})^{c}$ only
moves when the system players cannot continue alone. Thus, they get informed
of the environment’s decisions in their next steps and the system can
therefore be considered as completely informed. Bad situations
(nondeterminism, deadlocks, tokens on bad places) result in player 0 not
winning. If player 0 can avoid these situations and always win the game, this
strategy can be translated into a winning strategy for the system players in
the Petri game.

The _symbolic two-player Büchi game with canonical representations_
$\mathcal{G}(\mathit{G})^{c}=(\mathit{V}_{0},\mathit{V}_{1},\mathit{E},\mathit{V}_{\mathit{F}},\mathscr{R}_{0})$
for a high-level Petri game $\mathit{G}$ has the following components. The
_nodes_ $\mathit{V}=\mathit{V}_{0}\dot{\cup}\mathit{V}_{1}$ are all possible
canonical representations $\mathscr{R}$ of symbolic decision sets in
$\mathit{G}$. The partition into _player $0$’s nodes_ $\mathit{V}_{0}$ and
_player $1$’s nodes_ $\mathit{V}_{1}$ is given by
$\mathit{V}_{1}=\\{\mathscr{R}\,|\,\mathscr{R}$ is environment dependent$\\}$
and $\mathit{V}_{0}=\mathit{V}\setminus\mathit{V}_{1}$. The _edges_
$\mathit{E}$ are constructed as follows. If $\mathscr{R}\in\mathit{V}$
contains a bad place, is a deadlock, is terminating, or is nondeterministic,
there is only a self-loop originating from $\mathscr{R}$. If
$\mathscr{R}\in\mathit{V}_{0}$ then
$(\mathscr{R},\mathscr{R}^{\prime})\in\mathit{E}$ if either
$\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$, or, if no $\top$ can be
resolved, $\mathscr{R}[t.Z\rangle\mathscr{R}^{\prime}$ with only system
players participating in $t.Z$. If $\mathscr{R}\in\mathit{V}_{1}$, then
$(\mathscr{R},\mathscr{R}^{\prime})\in\mathit{E}$ for every
$\mathscr{R}^{\prime}$ such that $\mathscr{R}[t.Z\rangle\mathscr{R}^{\prime}$,
i.e., transitions involving environment players can only fire if nothing else
is possible. The set $\mathit{V}_{\mathit{F}}$ of _accepting nodes_ contains
all representations $\mathscr{R}$ that are terminating or environment-
dependent, but are not a deadlock, nondeterministic, or contain a bad place.
The _initial state_ $\mathscr{R}_{0}$ is the canonical representation of the
symbolic decision set containing $D_{0}$.

A function $f:{\mathit{V}}^{*}\mathit{V}_{0}\to\mathit{V}$ s.t.
$\forall\mathscr{R}_{0}^{\prime}\cdots\mathscr{R}_{k}^{\prime}\in{\mathit{V}}^{*}\mathit{V}_{0}:(\mathscr{R}_{k}^{\prime},f(\mathscr{R}_{0}^{\prime}\cdots\mathscr{R}_{k}^{\prime}))\in\mathit{E}$
is called a _strategy_ for player 0. A strategy $f$ is called _winning_ iff
every _run_ $\rho=\mathscr{R}_{0}\mathscr{R}_{1}\mathscr{R}_{2}\cdots$ from
$\mathscr{R}_{0}$ in $\mathcal{G}(\mathit{G})^{c}$ (i.e., $\forall
k:(\mathscr{R}_{k},\mathscr{R}_{k+1})\in\mathit{E}$) that is _consistent with_
$f$ (i.e.,
$\mathscr{R}_{k}\in\mathit{V}_{0}\Rightarrow\mathscr{R}_{k+1}=f(\mathscr{R}_{0}\cdots\mathscr{R}_{k})$)
_satisfies the Büchi condition w.r.t. $\mathit{V}_{\mathit{F}}$_ (i.e.,
$\forall k\ \exists k^{\prime}\geq
k:\mathscr{R}_{k^{\prime}}\in\mathit{V}_{\mathit{F}}$).

In the game $\mathcal{G}(\mathit{G})$ in [18], player 0 has a winning strategy
if and only if the system players in $\mathsf{L}(\mathit{G})$ have a winning
strategy. As described above, it is built from the relations
$\overline{D}[t.c\rangle D^{\prime}$ and $\overline{D}[\top\rangle D^{\prime}$
from representatives $\overline{D}$ of symbolic decision sets. The introduced
game $\mathcal{G}(\mathit{G})^{c}$ is built analogously, with the difference
that the nodes are now canonical representations instead of arbitrary
representatives of symbolic decision sets, and the edges are built from the
relations $\mathscr{R}[t.Z\rangle\mathscr{R}^{\prime}$ and
$\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$ (cf. Theorem 3.2 and Cor. 2).
The two games are isomorphic, as depicted in Fig. 1. Thus, we get the
following result.

###### Theorem 4.1

Given a Petri game $\mathsf{G}$ with one environment player, a bounded number
of system players with a safety objective, and a high-level representation
$\mathit{G}$, there is a winning strategy for the system players in
$\mathsf{G}$ if and only if there is a winning strategy for player $0$ in
$\mathcal{G}(\mathit{G})^{c}$.

The size of $\mathcal{G}(\mathit{G})^{c}$ is the same as of
$\mathcal{G}(\mathit{G})$ (exponential in the size of $\mathsf{G}$). This
means, using $\mathcal{G}(\mathit{G})^{c}$, the question whether a winning
strategy in $\mathsf{G}$ exists can still be answered in single exponential
time [13]. In $\mathcal{G}(\mathit{G})$ we must, for a newly reached node
$D^{\prime}$, test if it is equivalent to another, already existing,
representative. This means we check for all symmetries $s\in\xi$ if
$s(D^{\prime})$ is already a node in the game. In the best case, if we
directly find the node, this is $1$ comparison. In the worst case, at step $i$
with currently $|\mathit{V}^{i}|$ nodes, we must make
$|\xi_{\mathit{N}}||\mathit{V}^{i}|$ comparisons (no symmetric node is in the
game so far). To get the canonical representation of a reached node in
$\mathcal{G}(\mathit{G})^{c}$, we must make less than ${|\xi_{\mathit{N}}|}$
comparisons to order the dynamic representation (cf. Cor. 1), and then compare
it to all existing nodes. Thus, $|\xi_{\mathit{N}}|+1$ comparisons in the best
case vs. $|\xi_{\mathit{N}}|+|\mathit{V}^{i}|$ in the $i$-th step in the worst
case. We further investigate experimentally on this in Sec. 5.

###  4.2 Direct Strategy Generation

The solving algorithm in [18] builds a strategy in the Petri game
$\mathsf{G}=\mathsf{L}(\mathit{G})$ from a strategy in
$\mathcal{G}(\mathit{G})$ by first generating a strategy in the low-level
equivalent $\mathcal{G}(\mathsf{G})$. Constituting the canonical
representations as nodes allows us to directly generate a winning strategy
$\sigma$ for the system players in $\mathsf{G}$ from a winning strategy $f$
for player $0$ in $\mathcal{G}(\mathit{G})^{c}$ (cf. Fig. 1).

The key idea is the same as in [13]. The strategy $f$ is interpreted as a tree
$T_{f}$ with labels in $\mathit{V}$, and root $r_{0}$ labeled with
$\mathscr{R}_{0}$. The tree is traversed in breadth-first order, while the
strategy $\sigma$ is extended with every reached node. To show that this
procedure is correct, we must show that the generated strategy $\sigma$ is
satisfying the conditions justified refusal, determinism, and deadlock
freedom. Justified refusal is satisfied because of the delay of environment
transitions. Assuming nondeterminism or deadlocks in the generated strategy
$\sigma$ leads to the contradiction that there are respective decision sets in
$T_{f}$. Finally, $\sigma$ is _winning_ , since $f$ also does not reach
representations that contain a bad place. For the detailed proof, cf. App.
0.A.

Initially, the strategy $\sigma$ contains places corresponding to the initial
marking $\mathsf{M}_{0}$ in the Petri game, i.e., places labeled with $p.c$
for every $p.c\in\mathsf{M}_{0}$, each with a token on them. They constitute
the initial marking $\mathsf{M}_{0}^{\sigma}$ of $\sigma$. Every node $r$ in
$T_{f}$, labeled with $\mathscr{R}$, is now associated with a set
$\mathit{K}_{r}$ of _cuts_ – reachable markings in the strategy/unfolding. The
set $\mathit{K}_{r_{0}}$, associated to the root $r_{0}$, contains only the
cut $\kappa_{0}=\mathsf{M}_{0}^{\sigma}$, the initial marking described above.

$\mathit{Env}$$\mathit{d}_{2}$$\mathit{I}_{2}$$\mathit{Sys}_{2}$$\mathit{inf}_{2}$$\mathit{Sys}_{1}$$\mathit{Sys}_{2}$$\mathit{Sys}_{3}$$\mathit{a}_{22}$$\mathit{a}_{12}$$\mathit{a}_{32}$$\mathit{A}_{22}$$\mathit{A}_{12}$$\mathit{A}_{32}$$\mathit{R}_{2}$$\mathit{h}_{2}$$\mathit{H}_{2}$$\mathit{d}_{1}$$\mathit{I}_{1}$$\mathit{Sys}_{1}$$\mathit{inf}_{1}$$\mathit{Sys}_{1}$$\mathit{Sys}_{2}$$\mathit{Sys}_{3}$$\mathit{a}_{21}$$\mathit{a}_{11}$$\mathit{a}_{31}$$\mathit{A}_{21}$$\mathit{A}_{11}$$\mathit{A}_{31}$$\mathit{R}_{1}$$\mathit{h}_{1}$$\mathit{H}_{1}$$\mathit{d}_{3}$$\mathit{I}_{3}$$\mathit{Sys}_{3}$$\mathit{inf}_{3}$$\mathit{Sys}_{1}$$\mathit{Sys}_{2}$$\mathit{Sys}_{3}$$\mathit{a}_{23}$$\mathit{a}_{13}$$\mathit{a}_{33}$$\mathit{A}_{23}$$\mathit{A}_{13}$$\mathit{A}_{33}$$\mathit{R}_{3}$$\mathit{h}_{3}$$\mathit{H}_{3}$$\sigma$$\mathscr{R}_{0}$$\big{(}\mathit{Env}.Z_{2}^{1},\\{\mathit{d}.Z_{1}^{1}\\}\big{)}$$\big{(}\mathit{S}.Z_{1}^{1},\\{\mathit{inf}\\!.Z_{1}^{1}\\}\big{)}$$\big{(}\mathit{I}.Z_{1}^{2},\\{\mathit{inf}\\!.Z_{1}^{2}\\}\big{)}$$\big{(}\mathit{S}.Z_{1}^{1},\\{\mathit{inf}\\!.Z_{1}^{1},\mathit{inf}\\!.Z_{1}^{2}\\}\big{)}$$\big{(}\mathit{S}.Z_{1}^{2},\\{\mathit{inf}\\!.Z_{1}^{1},\mathit{inf}\\!.Z_{1}^{2}\\}\big{)}$$\vdots$
$\big{(}\mathit{H}.Z_{1}^{2},\top\big{)}$$\big{(}\mathit{H}.Z_{1}^{2},\\{\\}\big{)}$$\top$$\mathit{d}.Z_{1}^{1,1}$$\mathit{inf}.Z_{1}^{2,1}$$\mathit{h}.Z_{1}^{2,1}$$\top$$|Z_{1}^{1}|=3$$|Z_{2}^{1}|=1$$|Z_{1}^{1}|=2$$|Z_{1}^{2}|=1$$|Z_{2}^{1}|=1$$|Z_{1}^{1}|=2$$|Z_{1}^{2}|=1$$|Z_{2}^{1}|=1$$T_{f}$$\kappa_{0}=\mathsf{M}_{0}^{\sigma}$$\kappa_{1}$$\kappa_{2}$$\kappa_{3}$
Figure 4:  Parts of a winning strategy for player $0$ in
$\mathcal{G}(\mathit{G})^{c}$ (a tree with gray nodes for player $0$), and the
generated strategy for the system players in $\mathsf{L}(\mathit{G})$.

Every edge $(r,r^{\prime})$ in $T_{f}$ corresponds to either a relation
$\mathscr{R}[t.Z\rangle\mathscr{R}^{\prime}$ or
$\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$. Suppose now in the breadth-
first traversal of $T_{f}$ we reach a node $r$ with label $\mathscr{R}$ and
associated cuts $\mathit{K}_{r}$. Further suppose there is an edge in $T_{f}$
from $r$ to a node $r^{\prime}$ labeled with $\mathscr{R}^{\prime}$. If the
edge $(r,r^{\prime})$ in $T_{f}$ corresponds to a relation
$\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$ in $\mathit{G}$, then the node
$r^{\prime}$ is associated to the same set of cuts
$\mathit{K}_{r^{\prime}}=\mathit{K}_{r}$ and nothing is added to the strategy.
If the edge $(r,r^{\prime})$ in $T_{f}$ corresponds to a relation
$\mathscr{R}[t.Z\rangle\mathscr{R}^{\prime}$ in $\mathit{G}$ and
$\mathscr{R}\in\mathit{V}_{0}$, then there is, for every cut
$\kappa\in\mathit{K}_{r}$, a transition $t.v$ corresponding to $t.Z$ that can
be fired from $\kappa$ (cf. Theorem 3.2). We add a transition labeled with
$t.v$ to the strategy, with its preset in $\kappa$. Furthermore, we add places
corresponding to its postset to the strategy. The cut $\kappa^{\prime}$ that
results from firing the new transition from $\kappa$ is added to
$\mathit{K}_{r^{\prime}}$. If the edge $(r,r^{\prime})$ in $T_{f}$ corresponds
to a relation $\mathscr{R}[t.Z\rangle\mathscr{R}^{\prime}$ in $\mathit{G}$ and
$\mathscr{R}\in\mathit{V}_{1}$, then we proceed exactly as in the last case,
but with the crucial difference that instead of _one_ transition $t.v$
fireable from a cut $\kappa\in\mathit{K}_{r}$, we consider _all_ such
transition instances and add them to the strategy. In this step, the number of
associated cuts can increase.

In Fig. 4, the strategy tree $T_{f}$ (consisting of only one branch) in
$\mathcal{G}(\mathit{G})^{c}$ and the generated strategy $\sigma$ in (the
unfolding of) $\mathsf{L}(\mathit{G})$ for the running example $\mathit{G}$
are depicted. The strategy $\sigma$ was already informally described in Sec. 1
and partly shown in Fig. 3. The initial canonical representation
$\mathscr{R}_{0}$ is associated to the cut representing the initial marking in
the Petri game. The $\top$-resolution does not change the associated cuts.
Firing $\mathit{d}.Z_{1}^{2,1}$ corresponds to the three firings of
$\mathit{d}_{1}$, $\mathit{d}_{2}$, and $\mathit{d}_{3}$ in the strategy.
Thus, the third canonical representation is associated to the three cuts
$\\{\mathit{Sys}_{1},\mathit{Sys}_{2},\mathit{Sys}_{3},\mathit{I}_{j}\\}$,
$j=1,2,3$. The strategy $T_{f}$ terminates in the canonical representation at
the bottom, which corresponds to the three situations where all computers
connected to the correct host.

##  5 Experimental Results

In this section we investigate the impact of using _canonical representations_
for solving the realizability problem of distributed systems modeled with
high-level Petri games with one environment player, an arbitrary number of
system players, a safety objective, and an underlying symmetric net.

A prototype [18] for generating the reduced state space of
$\mathcal{G}(\mathit{G})$ for such a high-level Petri game $\mathit{G}$ shows
a state space reduction by up to three orders of magnitude compared to
$\mathcal{G}(\mathsf{L}(\mathit{G}))$ (cf. Fig. 1) for the considered
benchmark families [18]. For this paper we extended this prototype and
implemented algorithms to obtain the same state space reduction by using
canonical representations in /$\mathcal{G}(\mathit{G})^{c}$. Furthermore, we
implemented a solving algorithm to exploit the reduced state space for the
realizability problem of high-level Petri games. As a reference, we
implemented an explicit approach which does not exploit any symmetries of the
system. We applied our algorithms on the benchmark families presented in [18]
and added a benchmark family for the running example introduced in this paper.
An extract of the results for three of these benchmark families are given in
Table 1. The complete results are in App. 0.B.

Table 1:  Comparison of the run times of the _canonical (Canon.)_ and
_membership (Memb.)_ approach solving the realizability problem (✓/✗) for the
3 benchmark families _CS_ , _DW_ , _CM_ with the number of states $|V|$ and
number of symmetries $|\xi|$. A gray number of states $|\mathsf{V}|$ for the
_explicit reference approach_ indicates a timeout. Results are obtained on an
AMD Ryzen™ 7 3700X CPU, 4.4 GHz, 64 GB RAM and a timeout (TO) of 30 minutes.
The run times are in seconds.

CS | $|\mathsf{V}|$ | $\models$ | $|V|$ | $|\xi|$ | Memb. | Canon.
---|---|---|---|---|---|---
1 | 21 | ✓ | 21 | 1 | .38 | .36
2 | 639 | ✓ | 326 | 2 | .63 | .64
3 | 45042 | ✓ | 7738 | 6 | 5.20 | 6.05
4 | _7.225e6_ | ✓ | 3.100e5 | 24 | 151.62 | 148.08
5 | _3.154e9_ | - | - | 120 | TO | TO
DW | $|\mathsf{V}|$ | $\models$ | $|V|$ | $|\xi|$ | Memb. | Canon.
1 | 57 | ✓ | 57 | 1 | .40 | .39
2 | 457 | ✓ | 241 | 2 | .67 | .62
| $\cdots$ | $\cdots$ | $\cdots$ | $\cdots$
7 | _4.055e6_ | ✓ | 5.793e5 | 7 | 100.67 | 75.24
8 | _2.097e7_ | ✓ | 2.621e6 | 8 | 986.77 | 671.04
9 | _1.053e8_ | - | - | 9 | TO | TO

CM | $|\mathsf{V}|$ | $\models$ | $|V|$ | $|\xi|$ | Memb. | Canon.
---|---|---|---|---|---|---
2/1 | 155 | ✓ | 79 | 2 | .49 | .52
2/2 | 2883 | ✗ | 760 | 4 | 1.07 | 1.08
2/3 | 58501 | ✗ | 5548 | 12 | 4.38 | 5.94
2/4 | _1.437e6_ | ✗ | 33250 | 48 | 15.12 | 14.40
2/5 | _3.419e7_ | ✗ | 1.701e5 | 240 | 296.05 | 185.81
2/6 | _8.376e8_ | - | - | 1440 | TO | TO
2-7 3/1 | 702 | ✓ | 147 | 6 | .71 | .58
3/2 | 45071 | ✓ | 4048 | 12 | 4.46 | 4.99
3/3 | _3.431e6_ | ✗ | 91817 | 36 | 89.35 | 49.90
3/4 | _2.622e8_ | - | - | 144 | TO | TO
2-7 4/1 | 2917 | ✓ | 239 | 24 | 1.24 | 1.42
4/2 | _6.587e5_ | ✓ | 16012 | 48 | 25.42 | 14.09
4/3 | _1.546e8_ | - | - | 144 | TO | TO

The benchmark family Client/Server (CS) corresponds to the running example of
the paper. With Document Workflow (DW) a cyclic document workflow between
clerks is modeled. In this benchmark family the symmetries of the systems are
only one rotation per clerk. In Concurrent Machines (CM) a hostile environment
can destroy one of the machines processing the orders. Since each machine can
only process one order, a positive realizability result is only obtained when
the number of orders is smaller than the number of machines. In Table 1 we can
see that for those benchmark families the extra effort of computing the
canonical representations (Canon.) is worthwhile for most instances compared
to the cost of checking the membership of a decision set in an equivalence
class (Memb.). This is not the case for all benchmark families.

Figure 5: Comparing the percentage performance gain of the canonical and the
membership approach with respect to the number of states and symmetries of the
input problem for the benchmark families _Package Delivery (PD)_ , _Alarm
System (AS)_ , _CM_ , _DW_ , _DWs_ , _CS_. Labels are the parameters of the
benchmark. A blue (unhatched) marker indicates a performance increase when
using canonical representations.

In Fig. 5 we have plotted the instances of all benchmark families according to
their number of symmetries and states. The color of the marker shows the
percentaged in- or decrease in performance when using canonical
representations while solving high-level Petri games. Blue (unhatched)
indicates a performance gain when using the canonical approach. This shows
that the benchmarks in general benefit from the canonical approach for an
increasing number of states (the right blue (unhatched) area). However, the
_DWs_ benchmark (a simplified version of _DW_) exhibits the opposite behavior.
This is most likely explained by the very simple structure, which favors a
quick member check.

The algorithms are integrated in
AdamSYNT333https://github.com/adamtool/adamsynt [11], open source, and
available online444https://github.com/adamtool/highlevel. Additionally, we
created an artifact with the current version running in a virtual machine for
reproducing and checking all experimental data with provided
scripts555https://doi.org/10.6084/m9.figshare.13697845.

##  6 Related Work

For the synthesis of distributed systems other approaches are most prominently
the Pnueli/Rosner model [30] and Zielonka’s asynchronous automata [34]. The
synchronous setting of Pnueli/Rosner is in general undecidable [30], but some
interesting architectures exist that have a decision procedure with
nonelementary complexity [32, 26, 15]. For asynchronous automata, the
decidability of the control problem is open in general, but again there are
several interesting cases which have a decision procedure with nonelementary
complexity [16, 29, 28].

Petri games based on P/T Petri nets are introduced in [12, 13]. Solving
unbounded Petri games is in general undecidable. However, for Petri games with
one environment player, a bounded number of system players, and a safety
objective the problem is exptime-complete. The same complexity result holds
for interchanged players [14]. High-level Petri games have been introduced in
[17]. In [18], such Petri games are solved while exploiting symmetries.

The symbolic Büchi game is inspired by the symbolic reachability graph for
high-level nets from [5], and the calculation of canonical representatives [4]
from [6]. There are several works on how to obtain symmetries of different
subclasses of high-level Petri nets efficiently [9, 4, 6, 27] and for
efficiency improvements for systems with different degrees of symmetrical
behavior [22, 1, 2].

##  7 Conclusions and Outlook

We presented a new construction for the synthesis of distributed systems
modeled by high-level Petri games with one environment player, an arbitrary
number of system players, and a safety objective. The main idea is the
reduction to a symbolic two-player Büchi game, in which the nodes are
equivalence classes of symmetric situations in the Petri game. This leads to a
significant reduction of the state space. The novelty of this construction is
to obtain the reduction by introducing canonical representations. To this end,
a theoretically cheaper construction of the Büchi game can be obtained
depending on the input system. Additionally, the representations now allow to
skip the inflated generation of an explicit Büchi game strategy and to
directly generate a Petri game strategy from the symbolic Büchi game strategy.
Our implementation, applied on six structurally different benchmark families,
shows in general a performance gain in favor of the canonical representatives
for larger state spaces.

In future work, we plan to integrate the algorithms in AdamWEB [19], a web
interface666http://adam.informatik.uni-oldenburg.de/ for the synthesis of
distributed systems, to allow for an easy insight in the symbolic games and
strategies. Furthermore, we want to continue our investigation on the benefits
of canonical representations, e.g., to directly generate high-level
representations of Petri game strategies that match the given high-level Petri
game.

## References

  * [1] Baarir, S., Haddad, S., Ilié, J.: Exploiting partial symmetries in well-formed nets for the reachability and the linear time model checking problems. In: Proc. WODES 2004. pp. 219–224 (2004), https://doi.org/10.1016/S1474-6670(17)30749-8
  * [2] Bellettini, C., Capra, L.: A quotient graph for asymmetric distributed systems. In: Proc. MASCOTS 2004. pp. 560–568 (2004), https://doi.org/10.1109/MASCOT.2004.1348313
  * [3] Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Interactive presentation: Automatic hardware synthesis from specifications: a case study. In: Proc. DATE 2007. pp. 1188–1193 (2007), https://dl.acm.org/citation.cfm?id=1266622
  * [4] Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: On well-formed coloured nets and their symbolic reachability graph. In: Jensen, K., Rozenberg, G. (eds.) High-level Petri Nets: Theory and Application, pp. 373–396. Springer (1991), https://doi.org/10.1007/978-3-642-84524-6_13
  * [5] Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: A symbolic reachability graph for coloured Petri nets. Theor. Comput. Sci. 176(1-2), 39–65 (1997), https://doi.org/10.1016/S0304-3975(96)00010-2
  * [6] Chiola, G., Dutheillet, C., Franceschinis, G., Haddad, S.: Stochastic well-formed colored nets and symmetric modeling applications. IEEE Trans. Computers 42(11), 1343–1360 (1993), https://doi.org/10.1109/12.247838
  * [7] Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic. vol. 1, pp. 3–50. Cornell Univ., Ithaca, NY (1957)
  * [8] Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Proc. CAV 1998. pp. 147–158. LNCS1427 (1998), https://doi.org/10.1007/BFb0028741
  * [9] Dutheillet, C., Haddad, S.: Regular stochastic Petri nets. In: Proc. Petri Nets (ICATPN) 1990. pp. 186–209 (1989), https://doi.org/10.1007/3-540-53863-1_26
  * [10] Esparza, J., Heljanko, K.: Unfoldings - A Partial-Order Approach to Model Checking. EATCS Monographs in Theoretical Computer Science, Springer (2008). https://doi.org/10.1007/978-3-540-77426-6
  * [11] Finkbeiner, B., Gieseking, M., Olderog, E.: Adam: Causality-based synthesis of distributed systems. In: Proc. CAV 2015, Part I. pp. 433–439. LNCS9206 (2015), https://doi.org/10.1007/978-3-319-21690-4_25
  * [12] Finkbeiner, B., Olderog, E.: Petri games: Synthesis of distributed systems with causal memory. In: Proc. GandALF 2014. pp. 217–230. EPTCS161 (2014), https://doi.org/10.4204/EPTCS.161.19
  * [13] Finkbeiner, B., Olderog, E.: Petri games: Synthesis of distributed systems with causal memory. Inf. Comput. 253, 181–203 (2017), https://doi.org/10.1016/j.ic.2016.07.006
  * [14] Finkbeiner, B., Gölz, P.: Synthesis in distributed environments. In: Proc. FSTTCS 2017. pp. 28:1–28:14 (2017), https://doi.org/10.4230/LIPIcs.FSTTCS.2017.28
  * [15] Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Proc. LICS 2005\. pp. 321–330 (2005), https://doi.org/10.1109/LICS.2005.53
  * [16] Genest, B., Gimbert, H., Muscholl, A., Walukiewicz, I.: Asynchronous games over tree architectures. In: Proc. ICALP 2013, Part II. pp. 275–286. LNCS7966 (2013), https://doi.org/10.1007/978-3-642-39212-2_26
  * [17] Gieseking, M., Olderog, E.: High-level representation of benchmark families for Petri games. CoRR abs/1904.05621 (2019), http://arxiv.org/abs/1904.05621
  * [18] Gieseking, M., Olderog, E., Würdemann, N.: Solving high-level Petri games. Acta Inf. 57(3-5), 591–626 (2020), https://doi.org/10.1007/s00236-020-00368-5
  * [19] Gieseking, M., Hecking-Harbusch, J., Yanich, A.: A web interface for Petri nets with transits and Petri games. In: Proc. TACAS 2021 (2021), https://uol.de/f/2/dept/informatik/ag/csd/pub/GHY21.pdf, to appear
  * [20] Gieseking, M., Würdemann, N.: Canonical representations for direct generation of strategies in high-level petri games. In: Proc. Petri Nets (ICATPN) 2021 (2021), to appear
  * [21] Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS2500, Springer (2002), https://doi.org/10.1007/3-540-36387-4
  * [22] Haddad, S., Ilié, J., Taghelit, M., Zouari, B.: Symbolic reachability graph and partial symmetries. In: Proc. Petri Nets (ICATPN) 1995. pp. 238–257 (1995), https://doi.org/10.1007/3-540-60029-9_43
  * [23] Hillah, L., Kordon, F., Petrucci-Dauchy, L., Trèves, N.: PN standardisation: A survey. In: Proc. FORTE 2006,. pp. 307–322. LNCS4229 (2006), https://doi.org/10.1007/11888116_23
  * [24] Jensen, K.: Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use - Volume 1. EATCS Monographs on Theoretical Computer Science, Springer (1992), https://doi.org/10.1007/978-3-662-06289-0
  * [25] Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robotics 25(6), 1370–1381 (2009), https://doi.org/10.1109/TRO.2009.2030225
  * [26] Kupferman, O., Vardi, M.Y.: Synthesizing distributed systems. In: Proc. LICS 2001\. pp. 389–398 (2001), https://doi.org/10.1109/LICS.2001.932514
  * [27] Lindquist, M.: Parameterized reachability trees for predicate/transition nets. In: Proc. Petri Nets (ICATPN) 1991. pp. 301–324 (1991), https://doi.org/10.1007/3-540-56689-9_49
  * [28] Madhusudan, P., Thiagarajan, P.S., Yang, S.: The MSO theory of connectedly communicating processes. In: Proc. FSTTCS 2005. pp. 201–212. LNCS3821 (2005), https://doi.org/10.1007/11590156_16
  * [29] Muscholl, A., Walukiewicz, I.: Distributed synthesis for acyclic architectures. In: Raman, V., Suresh, S.P. (eds.) Proc. FSTTCS 2014. pp. 639–651. LIPIcs29 (2014), https://doi.org/10.4230/LIPIcs.FSTTCS.2014.639
  * [30] Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proc. FOCS. pp. 746–757. IEEE Computer Society Press (1990), https://doi.org/10.1109/FSCS.1990.89597
  * [31] Reisig, W.: Petri Nets: An Introduction, EATCS Monographs on Theoretical Computer Science, vol. 4. Springer (1985), https://doi.org/10.1007/978-3-642-69968-9
  * [32] Rosner, R.: Modular Synthesis of Reactive Systems. Ph.D. thesis, Weizmann Institute of Science, Rehovot, Israel (1992)
  * [33] Starke, P.H.: Reachability analysis of Petri nets using symmetries. Syst. Anal. Model. Simul. 8(4–5), 293–303 (Aug 1991)
  * [34] Zielonka, W.: Asynchronous automata. In: Diekert, V., Rozenberg, G. (eds.) The Book of Traces, pp. 205–247. World Scientific (1995), https://doi.org/10.1142/9789814261456_0007

## Appendix

##  Appendix 0.A Proofs

In this appendix, we give the proofs of the lemmas and theorems in the paper.
In the main body we omitted the partition of basic color classes into so
called _static subclasses_ $C_{i}=\bigcup_{i=1}^{n_{i}}C_{i,q}$ in a symmetric
net $\mathit{N}$. The proofs will take this more general case into account.

The symmetries are restricted because they must respect the partition, i.e.,
$\forall s\in\xi_{\mathit{N}}:s_{i}(C_{i,q})=C_{i,q}$. A representation
$\mathscr{R}=(\mathcal{C},\mathcal{D})$ of a symbolic decision set is equipped
with a function $\mathit{stat}$ that assigns each dynamic subclass
$Z_{i}^{j}\in\mathcal{C}$ a static subclass $C_{i,q}$, i.e.,
$\mathit{stat}(Z_{i}^{j})=q\in\\{1,\dots,n_{i}\\}$. The function satisfies
$j<k\Rightarrow\mathit{stat}(Z_{i}^{j})<\mathit{stat}(Z_{i}^{k})$ (i.e., the
dynamic subclasses are grouped by assigned static subclass). With the
condition $\forall
i,q:\sum_{\mathit{stat}(Z_{i}^{j})=q}|Z_{i}^{j}|=|C_{i,q}|$, each valid
assignment of values to the variables in the dynamic subclasses gives a
partition of the static subclasses $C_{i,q}$. A valid assignment is a function
$\mathit{va}:\bigcup_{i=1}^{n}C_{i}\to\mathcal{C}$ that maps colors $c\in
C_{i}$ to dynamic subclasses $Z_{i}^{j}$ and is consistent with the static
subclasses (function $\mathit{stat}$), and cardinality of colors and dynamic
subclasses.

A permutation of the dynamic subclasses is a tuple
$\rho=(\rho_{1},\dots,\rho_{n})$ of permutations on $\\{Z_{i}^{j}\,|\,1\leq
j\leq n_{i}\\}$ that respects the function $\mathit{stat}$, i.e.,
$\mathit{stat}(Z_{i}^{j})=\mathit{stat}(\rho_{i}(Z_{i}^{j}))$. We apply a
permutation to a representation $\mathscr{R}=(\mathcal{C},\mathcal{D})$ by
keeping $\mathcal{C}$ and replacing every occurrence of $Z_{i}^{j}$ in
$\mathcal{D}$ by $\rho_{i}(Z_{i}^{j})$, and changing the cardinality
$|Z_{i}^{j}|$ accordingly. The function $\mathit{stat}$ does not change. We
denote the new representation by $\rho(\mathscr{R})$.

Lemma 1 states that minimal representations are unique up to a permutation. In
the general case, minimal representations contain no two subclasses
$Z_{i}^{j},Z_{i}^{k}$ such that
$\mathit{stat}(Z_{i}^{j})=\mathit{stat}(Z_{i}^{j})$ and
$\operatorname{con}(Z_{i}^{j})=\operatorname{con}(Z_{i}^{k})$ (such dynamic
subclasses can be merged).

######  Proof (Lemma 1)

It follows directly from the definition that if $\mathscr{R}$ is minimal, so
is $\rho(\mathscr{R})$ for any permutation $\rho$. Let now $\mathscr{R}$ and
$\mathscr{R}^{\prime}$ be two minimal representations of the same symbolic
decision set. We show there is a permutation between $\mathscr{R}$ and
$\mathscr{R}^{\prime}$. There exist two corresponding representations
$\mathscr{R}_{p}$ and $\mathscr{R}_{p}^{\prime}$, where all dynamic subclasses
are split into dynamic subclasses of cardinality $1$. This means that
$\mathscr{R}$ can be reached from $\mathscr{R}_{p}$ by merging all subclasses
$Z_{i}^{j_{1}},\dots,Z_{i}^{j_{N}}$ such that each pair
$Z_{i}^{j_{k}},Z_{i}^{j_{\ell}}$ satisfies
$\mathit{stat}(Z_{i}^{j_{k}})=\mathit{stat}(Z_{i}^{j_{\ell}})\land\operatorname{con}(Z_{i}^{j_{k}})=\operatorname{con}(Z_{i}^{j_{\ell}})$,
and analogously for $\mathscr{R}^{\prime}$ and $\mathscr{R}_{p}^{\prime}$. All
representations of a fixed symbolic decision set that only contain dynamic
subclasses of cardinality $1$ can trivially transformed into each other by a
permutation. Furthermore, we can pick a permutation $\rho$ from
$\mathscr{R}_{p}$ to $\mathscr{R}_{p}^{\prime}$ such that if $Z_{i}^{j_{k}}$
and $Z_{i}^{j_{\ell}}$ are merged in $\mathscr{R}_{p}$, then
$\rho(Z_{i}^{j_{k}})$ and $\rho(Z_{i}^{j_{\ell}})$ are merged in
$\mathscr{R}_{p}^{\prime}$. This implies a corresponding permutation between
$\mathscr{R}$ and $\mathscr{R}^{\prime}$.

Now that we proved that minimal representations are unique up to a
permutation, the next task is to prove that ordering a minimal representation
makes it unique, and we can therefore speak of a canonical representation.
This is formally stated in Theorem 3.1. To prove the theorem, we introduce
Lemma 2. It states that if two representations are ordered and equivalent
(i.e., can be reached from another via a permutation), then they have the same
symbolic decision set $\mathcal{D}$.

###### Lemma 2

Let $\mathscr{R}_{1}=(\mathcal{C}_{1},\mathcal{D}_{1})$ and
$\mathscr{R}_{2}=(\mathcal{C}_{2},\mathcal{D}_{2})$ be two ordered
representations of the same symbolic decision set, and $\rho$ be a permutation
such that $\mathscr{R}_{2}=\rho(\mathscr{R}_{1})$. Then
$\mathcal{D}_{1}=\mathcal{D}_{2}$.

######  Proof (Lemma 2)

We denote the matrix of a representation $\mathscr{R}_{i}$ by
$\mathit{mat}_{i}$. Since $\mathscr{R}_{1}$ is ordered, $\rho$ cannot
transform $\mathit{mat}_{1}$ into a (lexicographically) smaller matrix. Aiming
a contradiction, assume that $\rho$ transforms $\mathit{mat}_{1}$ into a
bigger matrix $\rho(\mathit{mat}_{1})$. Since
$\rho(\mathit{mat}_{1})=\mathit{mat}_{2}$, this would mean that $\rho^{-1}$
transforms $\mathit{mat}_{2}$ into a smaller matrix, implying that
$\mathscr{R}_{2}$ is not ordered. Contradiction. Therefore,
$\mathit{mat}_{1}=\rho(\mathit{mat}_{1})=\mathit{mat}_{2}$. Since
$\mathit{mat}_{i}$ is just another presentation of $\mathcal{D}_{i}$, we
follow $\mathcal{D}_{1}=\mathcal{D}_{2}$.

Now we are equipped with all tools to prove Theorem 3.1, which states that
there is exactly one minimal and ordered representation for each symbolic
decision set.

######  Proof (Theorem 3.1)

The statement follows from Lemma 1 and Lemma 2. Let
$\mathscr{R}_{1}=(\mathcal{C}_{1},\mathcal{D}_{1})$ and
$\mathscr{R}_{2}=(\mathcal{C}_{2},\mathcal{D}_{2})$ be two minimal and ordered
representations of the same symbolic decision set. Lemma 1 gives us that there
is a permutation $\rho$ such that $\mathscr{R}_{2}=\rho(\mathscr{R}_{1})$.
Then we have by Lemma 2 that $\mathcal{D}_{1}=\mathcal{D}_{2}$. This means for
all $Z_{i}^{j}$ that
$\operatorname{con}_{1}(Z_{i}^{j})=\operatorname{con}_{2}(\rho_{i}(Z_{i}^{j}))$
($\operatorname{con}_{i}$ is the context in $\mathcal{D}_{i}$). $\rho$ is a
permutation, so by definition
$\mathit{stat}(\rho_{i}(Z_{i}^{j}))=\mathit{stat}(Z_{i}^{j})$.
$\mathscr{R}_{1}$ is minimal, therefore it must hold that
$\rho_{i}(Z_{i}^{j})=Z_{i}^{j}$, else we could merge the subclasses
$\rho_{i}(Z_{i}^{j})$ and $Z_{i}^{j}$. This holds for all $i,j$, such that we
finally have $\forall i:\rho_{i}=\mathit{id}_{\\{Z_{i}^{j}\,|\,1\leq j\leq
m_{i}\\}}$ and therefore,
$\mathscr{R}_{1}=\rho(\mathscr{R}_{1})=\mathscr{R}_{2}$.

Theorem 3.2 states that each relation between two decision sets is represented
by exactly one relation between the corresponding canonical representations of
the symbolic decision sets.

######  Proof (Theorem 3.2)

Consider the valid assignment
$\mathit{va}_{D}:\bigcup_{i=1}^{n}C_{i}\to\mathcal{C}$ with
$\mathscr{R}=(\mathcal{C},\mathcal{D})$ and
$\mathit{va}_{\mathcal{D}}^{-1}(D)=D$. Applying $\mathit{va}_{D}$ to a
valuation $v$ gives a tuple of dynamic subclasses in $\mathcal{C}$. Splitting
the contained elements in this tuple into dynamic subclasses $Z_{i}^{j,k}$ of
cardinality $1$ with respect to the different colors in $v$, gives a tuple $Z$
of instantiated subclasses. This splitting is possible since $\mathit{va}_{D}$
is valid. In the firing of $t.Z$, the dynamic subclasses replace colors, which
means that the reached dynamic representation represents the symbolic decision
set of $D^{\prime}$. Making it canonical therefore results in
$\mathscr{R}^{\prime}$. Assuming that $D[t.v\rangle D^{\prime}$ is represented
by two different symbolic relations
$\mathscr{R}[t.Z\rangle\mathscr{R}^{\prime}$ and
$\mathscr{R}[t.Z^{\prime}\rangle\mathscr{R}^{\prime}$ contradicts the fact
that $\mathscr{R}$ is ordered. The proof for the $\top$-resolution follows
analogously.

Theorem 4.1 states that the existence of a winning strategy for the system
players in a game $\mathsf{G}=\mathsf{L}(\mathit{G})$ is equivalent to the
existence of a winning strategy for player 0 in the two-player Büchi game
$\mathcal{G}(\mathit{G})^{c}$.

######  Proof (Theorem 4.1)

This theorem follows directly from the fact that the game
$\mathcal{G}(\mathit{G})^{c}$ is built exactly as the game
$\mathcal{G}(\mathit{G})$ in [18], with the difference that the nodes are now
canonical representations instead of arbitrary representatives of symbolic
decision sets (cf. Fig. 1).

Theorem 4.1 only states the equivalence of existence of strategies in the
games. We now prove that the algorithm for generating strategies is correct.
For the sake of completion we formally introduce Petri net unfoldings and
strategies in Petri games (1). Then we give a more detailed version of the
algorithm presented in Sec. 4 (2b), taking the general case (partition of
basic color classes) into account. For this, we first formally define the
relations between canonical representations that the game is built from (2a).
Finally, we prove the correctness of the algorithm (3).

(1) First, we must define concurrency and conflicts in Petri nets. Consider a
Petri net
$\mathsf{N}=(\mathsf{P},\mathsf{T},\mathsf{F},\mathsf{M}_{\mathsf{0}})$ and
two nodes $\mathsf{x},\mathsf{y}\in\mathsf{P}\cup\mathsf{T}$. We write
$\mathsf{x}<\mathsf{y}$, and call $\mathsf{x}$ _causal predecessor_ of
$\mathsf{y}$, if $\mathsf{x}\mathsf{F}^{+}\mathsf{y}$. Additionally, we write
$\mathsf{x}\leq\mathsf{y}$ if $\mathsf{x}<\mathsf{y}$ or
$\mathsf{x}=\mathsf{y}$, and call $\mathsf{x}$ and $\mathsf{y}$ _causally
related_ if $\mathsf{x}\leq\mathsf{y}$ or $\mathsf{y}\leq\mathsf{x}$. The
nodes $\mathsf{x}$ and $\mathsf{y}$ are said to be _in conflict_ , denoted by
$\mathsf{x}\sharp\mathsf{y}$, if
$\exists\mathsf{p}\in\mathsf{P}\,\exists\mathsf{t_{1}}\neq\mathsf{t_{2}}\in\mathit{post}(p):\mathsf{t_{1}}\leq\mathsf{x}\land\mathsf{t_{2}}\leq\mathsf{y}$.
Two nodes are called _concurrent_ , if they are neither in conflict, nor
causally related. A set $\mathsf{X}\subseteq\mathsf{P}\cup\mathsf{T}$ is
called concurrent, if each two elements in $\mathsf{X}$ are concurrent.

$\mathsf{N}$ is called an _occurrence net_ if: i) every place has at most one
transition in its preset, i.e.,
$\forall\mathsf{p}\in\mathsf{P}:|\mathit{pre}(\mathsf{p})|\leq 1$; ii) no
transition is in self conflict, i.e.,
$\forall{\mathsf{t}\in\mathsf{T}:}\neg(\mathsf{t}\sharp\mathsf{t})$; iii) no
node is its own causal predecessor, i.e.,
$\forall\mathsf{x}\in\mathsf{P}\cup\mathsf{T}:{\neg(\mathsf{x}<\mathsf{x})}$;
iv) the initial marking contains exactly the places with no transition in
their preset, i.e.,
$\mathsf{M}_{\mathsf{0}}=\\{\mathsf{p}\in\mathsf{P}\,|\,\mathit{pre}(\mathsf{p})=\emptyset\\}$.
An occurrence net is called a _causal net_ if additionally v) from every place
there is at most one outgoing transition, i.e.,
$\forall\mathsf{p}\in\mathsf{P}:|\mathit{post}(\mathsf{p})|\leq 1$.

For a superscripted net $\mathsf{N}^{x}$, we implicitly also equip its
components with the superscript, i.e.,
$\mathsf{N}^{x}=(\mathsf{P}^{x},\mathsf{T}^{x},\mathsf{F}^{x},\mathsf{M}_{\mathsf{0}}^{x})$,
as well as the corresponding pre- and postset function
$\mathit{pre}^{x},\mathit{post}^{x}$. Let $\mathsf{N}$ and
$\mathsf{N}^{\prime}$ be two Petri nets. A function
$h:\mathsf{P}\cup\mathsf{T}\to\mathsf{P}^{\prime}\cup\mathsf{T}^{\prime}$ is
called a _Petri net homomorphism_ , if: i) it maps places and transitions in
$\mathsf{N}$ into the corresponding sets in $\mathsf{N}^{\prime}$, i.e.,
$\forall\mathsf{p}\in\mathsf{P}:{h(\mathsf{p})\in\mathsf{P}^{\prime}}\land\forall{\mathsf{t}\in\mathsf{T}}:h(\mathsf{t})\in\mathsf{T}^{\prime}$;
ii) it maps the pre- and postset correspondingly, i.e.,
$\forall{\mathsf{t}\in\mathsf{T}}:\mathit{pre}^{\prime}(h(\mathsf{t}))=h(\mathit{pre}(\mathsf{t}))\land\mathit{post}^{\prime}(h(\mathsf{t}))=h(\mathit{post}(\mathsf{t}))$.
The homomorphism is called _initial_ if additionally iii) it maps the initial
marking of $\mathsf{N}$ to the initial marking of $\mathsf{N}^{\prime}$, i.e.,
$h(\mathsf{M}_{\mathsf{0}})=\mathsf{M}_{\mathsf{0}}^{\prime}$.

A(n _initial_) _branching process_ $\beta=(\mathsf{N}^{U},\lambda^{U})$ of
$\mathsf{N}$ consists of an occurrence net $\mathsf{N}^{U}$ and a(n initial)
homomorphism
$\lambda^{U}:\mathsf{P}^{U}\cup\mathsf{T}^{U}\to\mathsf{P}\cup\mathsf{T}$ that
is injective on transitions with same preset, i.e.,
$\forall\mathsf{\mathsf{t_{1}}},\mathsf{t_{2}}\in\mathsf{T}^{U}:(\mathit{pre}^{U}(\mathsf{t_{1}})=\mathit{pre}^{U}(\mathsf{t_{2}})\land\lambda^{U}(\mathsf{t_{1}})=\lambda^{U}(\mathsf{t_{2}}))\Rightarrow\mathsf{t_{1}}=\mathsf{t_{2}}$.
If $\beta_{R}=(\mathsf{N}^{R},\rho)$ is an initial branching process of
$\mathsf{N}$ with a causal net $\mathsf{N}^{R}$, $\beta_{R}$ is called an
_initial (concurrent) run of $\mathsf{N}$_. A run formalizes a single
concurrent execution of the net. For two branching processes
$\beta=(\mathsf{N}^{U},\lambda^{U})$ and
$\beta^{\prime}=({\mathsf{N}^{V}},{\lambda^{V}})$ we call $\beta$ a
_subprocess_ of $\beta^{\prime}$, if i) $\mathsf{N}^{U}$ is a _subnet_ of
${\mathsf{N}^{V}}$, i.e.,
$\mathsf{P}^{U}\subseteq{\mathsf{P}^{V}},\mathsf{T}^{U}\subseteq{\mathsf{T}^{V}},\mathsf{F}^{U}\subseteq{\mathsf{F}^{V}},\mathsf{M}_{\mathsf{0}}^{U}={\mathsf{M}_{\mathsf{0}}^{V}}$;
ii) ${\lambda^{V}}$ acts on $\mathsf{P}^{U}\cup\mathsf{T}^{U}$ as
$\lambda^{U}$ does, i.e.,
${\lambda^{V}}|_{\mathsf{P}^{U}\cup\mathsf{T}^{U}}=\lambda^{U}$.

A branching process $\beta=(\mathsf{N}^{U},\lambda^{U})$ is called an
_unfolding of $\mathsf{N}$_, if for every transition that can occur in the
net, there is a transition in the unfolding with corresponding label, i.e.,
$\forall\mathsf{t}\in\mathsf{T}\,\forall X\subseteq\mathsf{P}^{U}:X\text{
concurrent}\land\mathit{pre}(\mathsf{t})=\lambda^{U}(X)\Rightarrow\exists\mathsf{t}^{U}\in\mathsf{T}^{U}:\lambda^{U}(\mathsf{t}^{U})=\mathsf{t}\land\mathit{pre}^{U}(\mathsf{t}^{U})=X$.
The unfolding of a net is unique up to isomorphism. The unfolding of a Petri
game
$\mathsf{G}=(\mathsf{P}_{\mathsf{S}},\mathsf{P}_{\mathsf{E}},\mathsf{T},\mathsf{F},\mathsf{M}_{0},\mathsf{P}_{\mathsf{B}})$
with underlying net $\mathsf{N}$ is the unfolding of $\mathsf{N}$, where the
distinction of system-, environment-, and bad places is lifted to the
branching process:
$\mathsf{P}_{\mathsf{S}}^{U}=\\{\mathsf{p}\in\mathsf{P}^{U}\,|\,\lambda^{U}(\mathsf{p})\in\mathsf{P}_{\mathsf{S}}\\}$,
$\mathsf{P}_{\mathsf{E}}^{U}=\\{\mathsf{p}\in\mathsf{P}^{U}\,|\,\lambda^{U}(\mathsf{p})\in\mathsf{P}_{\mathsf{E}}\\}$,
and
$\mathsf{P}_{\mathsf{B}}^{U}=\\{\mathsf{p}\in\mathsf{P}^{U}\,|\,{\lambda^{U}(\mathsf{p})\in\mathsf{P}_{\mathsf{B}}}\\}$.

A _strategy_ for the system players in $\mathsf{G}$ is a subprocess
$\sigma=(\mathsf{N}^{\sigma},\lambda^{\sigma})$ of the unfolding of
$\mathsf{G}$ satisfying the following conditions:
_Justified refusal:_ If a transition is forbidden in the strategy, then a
system player in its preset uniformly forbids all occurrences in the strategy,
i.e.,
$\forall\mathsf{t}\in\mathsf{T}^{U}:({\mathsf{t}\notin\mathsf{T}^{\sigma}}\land\mathit{pre}^{U}(t)\subseteq\mathsf{P}^{\sigma})\Rightarrow(\exists\mathsf{p}\in\mathit{pre}^{U}(\mathsf{t})\cap\mathsf{P}_{\mathsf{S}}^{\sigma}\,\forall\mathsf{t^{\prime}}\in\mathit{post}^{U}(\mathsf{p}):\lambda^{U}(\mathsf{t^{\prime}})=\lambda^{U}(\mathsf{t})\Rightarrow\mathsf{t^{\prime}}\notin\mathsf{T}^{\sigma})$.
This also implies that no pure environment transition is forbidden.
_Determinism:_ In no reachable marking (cut) in the strategy does a system
player allow two transitions in his postset that are both enabled, i.e.,
$\forall\mathsf{p}\in\mathsf{P}_{\mathsf{S}}^{\sigma}\
\forall\mathsf{M}\in\mathcal{R}(\mathsf{N}^{\sigma}):\mathsf{p}\in\mathsf{M}\Rightarrow\exists^{\leq
1}\mathsf{t}\in\mathit{post}^{\sigma}(\mathsf{p}):\mathsf{M}[\mathsf{t}\rangle$.
The set $\mathcal{R}(\mathsf{N}^{\sigma})$ are all reachable markings in the
strategy.
_Deadlock freedom:_ Whenever the system can proceed in $\mathsf{G}$, the
strategy must also give the possibility to continue, i.e.,
$\forall\mathsf{M}\in\mathcal{R}(\mathsf{N}^{\sigma}):(\exists\mathsf{t}\in\mathsf{T}^{U}:\mathsf{M}[\mathsf{t}\rangle)\Rightarrow{\exists\mathsf{t^{\prime}}\in\mathsf{T}^{\sigma}:\mathsf{M}[\mathsf{t^{\prime}}\rangle}$.

An initial concurrent run $\pi=(\mathsf{N}^{R},\rho)$ of the underlying net
$\mathsf{N}$ of a Petri game $\mathsf{G}$ is called a _play_ in $\mathsf{G}$.
The play $\pi$ _conforms_ to $\sigma$ if it is a subprocess of $\sigma$. The
system players win $\pi$ if $\mathsf{P}_{\mathsf{B}}^{R}=\emptyset$, otherwise
the environment players win $\pi$. The strategy $\sigma$ is called _winning_ ,
if all plays that conform to $\sigma$ are won by the system players. This is
equivalent to $\mathsf{P}_{\mathsf{B}}^{\sigma}=\emptyset$.

(2a) We give more in-depth details on the generation of a Petri game strategy
$\sigma$ from a Büchi game strategy $f$. Since the edges in
$\mathcal{G}(\mathit{G})^{c}$ are built from relations
$\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$ and
$\mathscr{R}[t.Z\rangle\mathscr{R}^{\prime}$ between canonical representations
$\mathscr{R},\mathscr{R}^{\prime}$, we first have to explain these relations
more formally then in the main body of the paper.

With the canonical representations of symbolic decision sets, we must also
adapt the relations between these objects, namely the transition firing and
the $\top$-resolution. For that, we now introduce symbolic versions of these
relations. In the _symbolic transition firing_ , we consider _symbolic
instances_ of a transition $t$, where the parameters are assigned elements in
dynamic subclasses instead of specific colors in basic color classes. For a
representation $\mathscr{R}$ we group the dynamic subclasses by $\forall 1\leq
i\leq n:\mathcal{C}_{i}=\\{Z_{i}^{j}\,|\,1\leq j\leq m_{i}\\}$. For a
transition $t\in\mathit{T}$ we then define
$\mathit{Val}_{\mathscr{R}}(t)=\mathcal{C}_{1}^{t_{1}}\\!\times\\!\cdots\\!\times\\!\mathcal{C}_{n}^{t_{n}}$
(analogously to
$\mathit{Val}(t)=C_{1}^{t_{1}}\\!\times\\!\cdots\\!\times\\!C_{n}^{t_{n}}$).
The instance of the $x$-th parameter of type $\mathcal{C}_{i}$ in
$\mathit{Val}_{\mathscr{R}}(t)$ can be specified by a pair
$(\varphi_{i}(x),\psi_{i}(x))=(j,k)$, meaning that the parameter represents
the $k$-th (arbitrarily chosen) element of $Z_{i}^{j}$. Since we maximally
have $|Z_{i}^{j}|$ different instances of $Z_{i}^{j}$, $k<|Z_{i}^{j}|$ must
hold. Furthermore, $k$ must be less than the number of parameters instanced to
$Z_{i}^{j}$. A _symbolic mode_ $[\varphi,\psi]$ of $t$ is defined by two
families of functions
$\varphi=\\{\varphi_{i}:\\{1,\dots,t_{i}\\}\to\mathbb{N}^{+}\\}$ and
$\psi=\\{\psi_{i}:\\{1,\dots,t_{i}\\}\to\mathbb{N}^{+}\\}$ satisfying the
conditions above. We denote
$Z^{[\varphi,\psi]}=((Z_{i}^{\varphi_{i}(x),\psi_{i}(x)})_{x=1}^{t_{i}})_{i=1}^{n}$,
and $t.Z^{[\varphi,\psi]}$ is called a _symbolic instance of_ $t$.

To fire a symbolic instance $t.Z^{[\varphi,\psi]}$ from a representation
$\mathscr{R}=(\mathcal{C},\mathcal{D})$, we have to _split_ the dynamic
subclasses $Z_{i}^{j}$ such that the (by $\varphi_{i}$ and $\psi_{i}$)
instantiated elements are represented by new subclasses $Z_{i}^{j,k}$ of
cardinality $1$. The possibly remaining (non-instantiated) elements are
collected in the additional subclass $Z_{i}^{j,0}$. The new dynamic decision
set can be naturally derived from $\mathcal{D}$: since the subclasses
$Z_{i}^{j}$ are split into $\\{Z_{i}^{j,k}\\}_{k}$, every tuple
$(p.Z,\mathsf{C})\in\mathcal{D}$ in which the original subclasses appeared is
replaced by all possible tuples containing the new subclasses instead. This
_split representation_ is denoted by $\mathscr{R}[\varphi,\psi]$.

A symbolic instance $t.Z^{[\varphi,\psi]}$ can be _fired_ from the
representation
$\mathscr{R}[\varphi,\psi]=:\mathscr{R}_{s}=(\mathcal{C}_{s},\mathcal{D}_{s})$
analogously to the ordinary case $D[t.c\rangle$ with the dynamic subclasses
$Z_{i}^{j,k}$ replacing the explicit colors $c\in C_{i}$ in guards and arc
expressions. This leads to a new representation $\mathscr{R}_{s}^{\prime}$
with same dynamic subclasses $\mathcal{C}_{s}^{\prime}=\mathcal{C}_{s}$ and
the dynamic decision set $\mathcal{D}_{s}^{\prime}$ that results from firing
$t.Z^{[\varphi,\psi]}$ from $\mathcal{D}_{s}$ (w.r.t the flow function
$\mathsf{F}$). Finally, the canonical representation $\mathscr{R}^{\prime}$ of
$\mathscr{R}_{s}^{\prime}$ is found. The symbolic firing is denoted by
$\mathscr{R}[t.Z^{[\varphi,\psi]}$ and can be described by

$\mathscr{R}\xrightarrow{\text{splitting w.r.t
}[\varphi,\psi]}\mathscr{R}_{s}\xrightarrow{\text{firing
}t.Z^{[\varphi,\psi]}}\mathscr{R}_{s}^{\prime}\xrightarrow{\text{canon.
rep.}}\mathscr{R}^{\prime}.$

The symbolic instances of a transition $t$ form a partition of the regular
instances $t.c$, $c\in\mathit{Val}(t)$.

The idea of _symbolic $\top$-resolution_ is similar to the symbolic firing. A
canonical representation which contains a tuple $(p.Z,\top)$ is partitioned
into a finer representation. The symbol $\top$ gets resolved as before, and
finally, the new canonical representation is built. Partitioning is a more
general case of splitting. While in the $\mathscr{R}[\varphi,\psi]$ only
dynamic subclasses of cardinality $1$ are split off, the _partitions_
$\mathscr{R}_{p}$ of a representation $\mathscr{R}$ are exactly the
representations from which $\mathscr{R}$ can be reached by merging dynamic
subclasses.

This gives, for a canonical representation $\mathscr{R}$, that
$\mathscr{R}[\top\rangle$ iff $\exists(p.Z,\top)\in\mathcal{D}$, and
$\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$ iff there is a partition
$\mathscr{R}_{p}$ of $\mathscr{R}$ such that $\mathscr{R}^{\prime}$ is the
canonical representation of $\mathscr{R}_{p}^{\prime}$. In
$\mathscr{R}_{p}^{\prime}$ the dynamic subclasses are copied from
$\mathscr{R}_{p}$, and in $\mathcal{D}_{p}^{\prime}$ every
$(p.Z,\top)\in\mathcal{D}_{p}$ chooses a new commitment set $\mathsf{C}$. The
symbolic $\top$-resolution is denoted by
$\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$ and can be described by

$\mathscr{R}\xrightarrow{\text{\text{partitioning}}}\mathscr{R}_{p}\xrightarrow{\top\text{-resolution}}\mathscr{R}_{p}^{\prime}\xrightarrow{\text{canon.
rep.}}\mathscr{R}^{\prime}.$

(2b) Now we describe the algorithm: Initially, the strategy $\sigma$ contains
places corresponding to the initial marking $\mathsf{M}_{0}$ in the Petri
game, i.e., places labeled with $p.c$ for every $p.c\in\mathsf{M}_{0}$, each
with a token on them. They constitute the initial marking of $\sigma$. Every
node $r$ in $T_{f}$, labeled with $\mathscr{R}=(\mathcal{C},\mathcal{D})$, is
now associated to a set $\mathit{K}_{r}$ of _cuts_ – reachable markings in the
strategy/unfolding. The set $\mathit{K}_{r_{0}}$, associated to the root
$r_{0}$, contains only the cut $\kappa_{0}$ consisting of the places in the
initial marking described above. Every cut $\kappa$ is equipped with a valid
assignment $\mathit{va}_{\kappa}$ that maps $\kappa$ to places in the dynamic
decision set $\mathcal{D}$. Every edge $(r,r^{\prime})$ in $T_{f}$ corresponds
to an edge $(\mathscr{R},\mathscr{R}^{\prime})$ in
$\mathcal{G}(\mathit{G})^{c}$, and the edges there again can correspond to
either relations $\mathscr{R}[t.Z^{[\varphi,\psi]}\rangle\mathscr{R}^{\prime}$
or $\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$.

Suppose in the breadth-first traversal of $T_{f}$ we reach a node $r$ with
label $\mathscr{R}$ and set of associated cuts $\mathit{K}_{r}$. Further
suppose there is an edge in $T_{f}$ from $r$ to a node $r^{\prime}$ labeled
with $\mathscr{R}^{\prime}$. From there, we distinguish three cases:

1) The edge $(r,r^{\prime})$ in $T_{f}$ corresponds to a relation
$\mathscr{R}[\top\rangle\mathscr{R}^{\prime}$ in $\mathit{G}$. As we know,
this can be depicted as $\mathscr{R}\xrightarrow{\text{\text{partition
}}\phi}\mathscr{R}_{p}\xrightarrow{\top\text{-resolution}}\mathscr{R}_{p}^{\prime}\xrightarrow{\text{canon.
rep. }}\mathscr{R}^{\prime}$. We now describe how $\mathit{K}_{r}$ changes in
these three steps. In the first step, the partition $\mathscr{R}_{p}$, there
is a family $\phi$ of functions
$\phi_{i}:({\mathcal{C}_{p}})_{i}\to\mathcal{C}_{i}$ describing the partition.
For every $(\kappa,\mathit{va}_{\kappa})\in\mathit{K}_{r}$, we change the
assignment to a function
$\mathit{va}_{\kappa}^{\prime}:\bigcup_{i}C_{i}\to\mathcal{C}_{p}$ such that
$\mathit{va}_{\kappa}=\phi\circ\mathit{va}_{\kappa}^{\prime}$. In the second
step, the resolution of $\top$, the set $\mathit{K}_{r}$ does not change (and
we now denote
$\mathit{va}_{\kappa}^{\prime}:\bigcup_{i}C_{i}\to\mathcal{C}_{p}^{\prime}$) .
For the third step (the canonical representation) there again is a partition
function $\phi^{\prime}:\mathcal{C}_{p}^{\prime}\to\mathcal{C}^{\prime}$. We
again change the assignment for every cut $\kappa$ to
$\mathit{va}_{\kappa}^{\prime\prime}=\phi^{\prime}\circ\mathit{va}_{\kappa}^{\prime}$.
Finally we assign to node $r^{\prime}$ the set
$\mathit{K}_{r^{\prime}}=\\{(\kappa,\mathit{va}_{\kappa}^{\prime\prime})\,|\,(\kappa,\mathit{va}_{\kappa})\in\mathit{K}_{r}\\}$.

2) The edge $(r,r^{\prime})$ in $T_{f}$ corresponds to a relation
$\mathscr{R}[t.Z^{[\varphi,\psi]}\rangle\mathscr{R}^{\prime}$ in $\mathit{G}$
and $t$ is an system transition. The relation can be described by
$\mathscr{R}\xrightarrow{\text{splitting w.r.t
}[\varphi,\psi]}\mathscr{R}_{s}\xrightarrow{\text{firing
}t.Z^{[\varphi,\psi]}}\mathscr{R}_{s}^{\prime}\xrightarrow{\text{canon. rep.
}}\mathscr{R}^{\prime}$. Since the first step (splitting) is a special case of
partition, we proceed as in the first case, and get the same cuts $\kappa$
with altered assignments
$\mathit{va}_{\kappa}^{\prime}:\bigcup_{i}C_{i}\to\mathcal{C}_{s}$. Since
after the process of splitting, the dynamic subclasses appearing in
$Z^{[\varphi,\psi]}$ are all of cardinality $1$, there is for each cut
$\kappa$ only one mode
$v_{\kappa}=((c_{i,j})_{j=1}^{t_{i}})_{i=1}^{n}\in\mathit{Val}(t)$ such that
$\mathit{va}_{\kappa}(v_{\kappa})=Z^{[\varphi,\psi]}$. For every cut $\kappa$
we add a transition with label $t.d$ to the strategy, the places labeled with
$p.c$ from $\kappa$ in its preset such that $c\in v(p,t)$, and we add places
labeled with $p^{\prime}.c^{\prime}$ to the strategy in the postset of the
transition if $c^{\prime}\in v(t,p^{\prime})$. We then delete the places in
the preset of the new transition from $\kappa$ and add the places in the
postset, to get the cut $\kappa^{\prime}$ with the same assignment
$\mathit{va}_{\kappa^{\prime}}=\mathit{va}_{\kappa}^{\prime}:\bigcup_{i}C_{i}\to\mathcal{C}_{s}^{\prime}$.
In the third step (canonical representation) we can again proceed as in the
first case, which results in
$\mathit{K}_{r^{\prime}}=\\{(\kappa^{\prime},\mathit{va}_{\kappa}^{\prime\prime})\,|\,(\kappa,\mathit{va}_{\kappa})\in\mathit{K}_{r}\\}$.

3) The edge $(r,r^{\prime})$ in $T_{f}$ corresponds to a relation
$\mathscr{R}[t.Z^{[\varphi,\psi]}\rangle\mathscr{R}^{\prime}$ in $\mathit{G}$
and $t$ is an environment transition. In this case, we proceed exactly as in
the second case, but with one crucial change in the first step (splitting
w.r.t $[\varphi,\psi]$): instead of choosing _one_ function
$\mathit{va}_{\kappa}^{\prime}:\bigcup_{i}C_{i}\to\bigcup_{i}\mathscr{R}_{p}.\hat{C}_{i}$
such that $\mathit{va}_{\kappa}=\phi\circ\mathit{va}_{\kappa}^{\prime}$, we
add a pair $(\kappa,\mathit{va}_{\kappa}^{\prime})$ for _all_ such assignments
and all corresponding $t.Z^{[\varphi,\psi]}$. The rest of the procedure
remains the same.

(3) Finally, we prove that the algorithm is correct. This proof works
analogous to [13], where Finkbeiner and Olderog consider the case of P/T Petri
games. The crucial difference is that we associate multiple cuts in $\sigma$
to a node in the tree $T_{f}$. We have to prove that the generated strategy
$\sigma$ is satisfying the conditions justified refusal, determinism and
deadlock freedom defined above. Then, $\sigma$ is _winning_ , since $f$ does
not reach representations that contain a bad place.

_Justified refusal:_ Assume there is a transition $\mathsf{t}$ in the
unfolding that is not in the strategy, but the preset of the transition is (so
$\mathsf{t}$ would be enabled in the strategy). Let $t.c=\lambda(\mathsf{t})$.
Then, the reason for $\mathsf{t}$’s absence is that there is a system place
$\mathsf{p}$ in the preset of $\mathsf{t}$ such that on all traversals that
reach a representation $\mathscr{R}=(\mathcal{C},\mathcal{D})$ and a cut with
valid assignment $(\kappa,\mathit{va}_{\kappa})$ such that $\mathsf{t}$ is
enabled in $\kappa$, $\mathcal{D}$ forbids
$\mathit{va}_{\kappa}(\lambda(\mathsf{t}))=t.\mathit{va}_{\kappa}(c)$, and
hence also no transition $\mathsf{\mathsf{t}^{\prime}}$ with
$\lambda(\mathsf{t^{\prime}})=\lambda(\mathsf{t})$ (implying
$\mathit{va}_{\kappa}(\lambda(\mathsf{t}))=\mathit{va}_{\kappa}(\lambda(\mathsf{\mathsf{t}^{\prime}}))$)
is in the strategy.

_Deadlock freedom:_ The generated strategy is deadlock free because in every
branch in the tree $T_{f}$ either infinitely many transitions are fired, or at
some point it loops in a terminating state. The strategy $f$ does not contain
representations that are deadlocks.

_Determinism:_ Aiming a contradiction, assume that there are two transitions
$\mathsf{t_{1}}$ and $\mathsf{t_{2}}$ in the strategy that have a shared
system place $\mathsf{p}$ in their preset. and are both enabled at the same
cut $\kappa$ in the strategy.
_Case 1._ Suppose that during the construction of $\sigma$, $\kappa$ is
encountered as a cut $(\kappa,\mathit{va}_{\kappa})\in\mathit{K}_{r}$
associated to node $r$ labeled with representation
$\mathscr{R}=(\mathcal{C},\mathcal{D})$. Then $\mathscr{R}$ is
nondeterministic. Contradiction (the strategy does not contain
nondeterministic representations).
_Case 2._ Suppose there exist two cuts
$(\kappa_{1},\mathit{va}_{\kappa_{1}})\in\mathit{K}_{r_{1}}$ and
$(\kappa_{2},\mathit{va}_{\kappa_{2}})\in\mathit{K}_{r_{2}}$ such that during
the construction of $\sigma$, first $\mathsf{t_{1}}$ was introduced at
$\kappa_{1}$ and then $\mathsf{t_{2}}$ was introduced at $\kappa_{2}$, with
$\mathit{pre}(\mathsf{t_{i}})\subseteq\kappa_{i}$ but
$\mathit{pre}(\mathsf{t_{1}})\nsubseteq\kappa_{2}$ and
$\mathit{pre}(\mathsf{t_{2}})\nsubseteq\kappa_{1}$. We again distinguish two
cases.
_Case 2a_ concerns the situation that $r_{2}$ is _below_ $r_{1}$ in $T_{f}$.
Suppose in the Büchi game the symbolic instances
$t_{1}.Z^{[\varphi^{1},\psi^{1}]},\dots,t_{n}.Z^{[\varphi^{n},\psi^{n}]}$,
with $n\geq 1$, are fired between $r_{1}$ and $r_{2}$, corresponding to a
sequence
$\kappa_{1}=\kappa_{0}^{\prime}[\mathsf{\mathsf{t}_{1}^{\prime}}\rangle\dots[\mathsf{\mathsf{t}_{n}^{\prime}}\rangle\kappa_{n}^{\prime}=\kappa_{2}$.
If this sequence removes a token from a place
$\mathsf{p}\in\mathit{pre}(\mathsf{\mathsf{t}_{1}})$ and puts it on
$\mathit{pre}(\mathsf{\mathsf{t}_{2}})$ then place
$\mathit{pre}(\mathsf{\mathsf{t}_{1}})$ and
$\mathit{pre}(\mathsf{\mathsf{t}_{2}})$ are in conflict, therefore there
cannot exist a cut $\kappa$ in which both $\mathsf{\mathsf{t}_{1}}$ and
$\mathsf{\mathsf{t}_{2}}$ are enabled. Contradiction. Thus, a transition that
takes a token from a place in $\mathit{pre}(\mathsf{\mathsf{t}_{1}})$ puts it
outside of $\mathit{pre}(\mathsf{\mathsf{t}_{2}})$. Consider the first
transition $\mathsf{\mathsf{t}_{j}}$ that removes a token from
$\mathit{pre}(\mathsf{\mathsf{t}_{1}})$. Then the representation
$\mathscr{R}=(\mathcal{C},\mathcal{D})$, label of the node $r$ that introduces
$\kappa_{j-1}$ is nondeterministic, as two instances $t.Z^{[\varphi,\psi]}$
and $t_{j}.Z^{[\varphi^{i},\psi^{i}]}$, corresponding to
$\mathsf{\mathsf{t}_{1}}$ and $\mathsf{\mathsf{t}_{j}}$ are enabled in
$\mathcal{D}$. Then proceed as in Case 1.
_Case 2b_ concerns the situation that $r_{1}$ and $r_{2}$ are on different
branches in $T_{f}$. Let $r$ be their last common ancestor. Let $\mathsf{p}$
be the environment place contained in the cut
$(\kappa,\mathit{va}_{\kappa})\in\mathit{K}_{r}$ that such that
$\kappa\leq\kappa_{i}$. Let $\mathsf{\mathsf{t}_{i}^{\prime}}$ be the
transition from $\mathsf{p}$ in the path from $r$ to $r_{i}$. Then all
transitions added in branches after $\mathsf{t_{1}^{\prime}}$ are in conflict
with all transitions added in branches after $\mathsf{t_{2}^{\prime}}$. In
particular, $\mathsf{t_{1}}$ and $\mathsf{t_{2}}$ are in conflict, and
therefore cannot be enabled at the same marking. Contradiction.

##  Appendix 0.B Experimental Data

In this section of the appendix we present additional data of our experimental
results. The results are obtained on an AMD Ryzen™ 7 3700X CPU with 4.4 GHz
and 64 GB RAM and a timeout (TO) of 30 minutes. The running times are given in
seconds.

|  | Explicit Approach |  | Reduced State Space | Memb. | Canon.
---|---|---|---|---|---|---
Ben. | Par. | $|\mathsf{V}|$ | $|\mathsf{E}|$ | Time | $\models$ | $|V|$ | $|E|$ | $|\xi|$ | Time | Time
PD | 1/1 | 30 | 31 | .39 | ✗ | 30 | 31 | 1 | .38 | .40
| 1/2 | 287 | 390 | .64 | ✗ | 152 | 207 | 2 | .54 | .54
| 1/3 | 2510 | 4157 | 2.37 | ✗ | 516 | 885 | 6 | 1.06 | 1.21
| 1/4 | 20765 | 39596 | 38.46 | ✗ | 1376 | 2859 | 24 | 3.55 | 4.34
| 1/5 | _307604.0_ | - | TO | ✗ | 3123 | 7630 | 120 | 6.06 | 6.94
| 1/6 | _3286707.0_ | - | - | ✗ | 6315 | 17738 | 720 | 29.71 | 29.46
| 1/7 | _3.59159e7_ | - | - | ✗ | 11707 | 37158 | 5040 | 373.48 | 405.21
| 1/8 | _3.97631e8_ | - | - | - | - | - | 40320 | TO | TO
2-11 | 2/1 | 277 | 316 | .64 | ✗ | 140 | 161 | 2 | .49 | .51
| 2/2 | 25940 | 39480 | 52.37 | ✓ | 6540 | 9912 | 4 | 4.46 | 4.83
| 2/3 | _2891324.0_ | - | TO | ✗ | 200851 | 325481 | 12 | 34.29 | 31.13
| 2/4 | _3.04624e8_ | - | - | ✗ | 3773484 | 5986550 | 48 | 2665.57 | 1716.67
| 2/5 | _-_ | - | - | - | - | - | 240 | TO | TO
2-11 | 3/1 | 1821 | 2360 | 1.89 | ✗ | 344 | 460 | 6 | .83 | .75
| 3/2 | _1110773.0_ | - | TO | ✓ | 87014 | 194168 | 12 | 21.50 | 20.77
| 3/3 | _7.79483e8_ | - | - | - | - | - | 36 | TO | TO
2-11 | 4/1 | 11089 | 15440 | 7.39 | ✗ | 692 | 1013 | 24 | 2.21 | 1.92
| 4/2 | _3.54425e7_ | - | TO | ✓ | 728983 | 2090860 | 48 | 393.00 | 267.28
| 4/3 | _-_ | - | - | - | - | - | 144 | TO | TO
2-11 | 5/1 | 64433 | 93152 | 466.16 | ✗ | 1230 | 1913 | 120 | 4.43 | 4.99
| 5/2 | _-_ | - | TO | - | - | - | 240 | TO | TO
AS | 2 | 7383 | 14482 | 6.85 | ✓ | 3713 | 7316 | 2 | 2.85 | 3.49
| 3 | _5.80273e7_ | - | TO | - | - | - | 6 | TO | TO
CM | 2/1 | 155 | 178 | .54 | ✓ | 79 | 92 | 2 | .49 | .52
| 2/2 | 2883 | 4128 | 2.33 | ✗ | 760 | 1067 | 4 | 1.07 | 1.08
| 2/3 | 58501 | 101108 | 661.98 | ✗ | 5548 | 9032 | 12 | 4.38 | 5.94
| 2/4 | _1437319.0_ | - | TO | ✗ | 33250 | 60771 | 48 | 15.12 | 14.40
| 2/5 | _3.41983e7_ | - | - | ✗ | 170100 | 340898 | 240 | 296.05 | 185.81
| 2/6 | _8.37675e8_ | - | - | - | - | - | 1440 | TO | TO
2-11 | 3/1 | 702 | 1097 | 1.11 | ✓ | 147 | 219 | 6 | .71 | .58
| 3/2 | 45071 | 137701 | 552.30 | ✓ | 4048 | 10562 | 12 | 4.46 | 4.99
| 3/3 | _3431991.0_ | - | TO | ✗ | 91817 | 420717 | 36 | 89.35 | 49.90
| 3/4 | _2.62284e8_ | - | - | - | - | - | 144 | TO | TO
2-11 | 4/1 | 2917 | 7396 | 3.39 | ✓ | 239 | 464 | 24 | 1.24 | 1.42
| 4/2 | _658721.0_ | - | TO | ✓ | 16012 | 116542 | 48 | 25.42 | 14.09
| 4/3 | _1.54628e8_ | - | - | - | - | - | 144 | TO | TO
DW | 1 | 57 | 69 | .41 | ✓ | 57 | 69 | 1 | .40 | .39
| 2 | 457 | 600 | .80 | ✓ | 241 | 314 | 2 | .67 | .62
| 3 | 3385 | 4640 | 2.95 | ✓ | 1145 | 1568 | 3 | 1.40 | 1.48
| 4 | 22305 | 31296 | 33.19 | ✓ | 5613 | 7878 | 4 | 3.73 | 5.08
| 5 | _134186.0_ | - | TO | ✓ | 26857 | 38192 | 5 | 6.93 | 7.41
| 6 | _755762.0_ | - | - | ✓ | 126065 | 180772 | 6 | 19.53 | 18.93
| 7 | _4055098.0_ | - | - | ✓ | 579321 | 835056 | 7 | 100.67 | 75.24
| 8 | _2.09715e7_ | - | - | ✓ | 2621677 | 3793406 | 8 | 986.77 | 671.04
| 9 | _1.05381e8_ | - | - | - | - | - | 9 | TO | TO
DWs | 1 | 61 | 64 | .39 | ✓ | 61 | 64 | 1 | .37 | .38
| 2 | 1835 | 2058 | 1.85 | ✓ | 926 | 1053 | 2 | 1.16 | .93
| 3 | 42851 | 48658 | 191.02 | ✓ | 14295 | 16262 | 3 | 6.19 | 5.74
| 4 | _908413.0_ | - | TO | ✓ | 224144 | 255839 | 4 | 34.64 | 34.94
| 5 | _1.79271e7_ | - | - | ✓ | 3536069 | 4039956 | 5 | 1935.66 | 4230.29
| 6 | _3.40931e8_ | - | - | - | - | - | 6 | TO | TO
CS | 1 | 21 | 20 | .38 | ✓ | 21 | 20 | 1 | .38 | .36
| 2 | 639 | 812 | .80 | ✓ | 326 | 425 | 2 | .63 | .64
| 3 | 45042 | 71273 | 358.69 | ✓ | 7738 | 12362 | 6 | 5.20 | 6.05
| 4 | _7225357.0_ | - | TO | ✓ | 310076 | 544733 | 24 | 151.62 | 148.08
| 5 | _3.15402e9_ | - | - | - | - | - | 120 | TO | TO