# (Un)Decidability Bounds of the Synthesis Problem
for Petri Games

Paul Hannibal University of Oldenburg,
Lower Saxony, Germany<EMAIL_ADDRESS>
###### Abstract

Petri games are a multi-player game model for the automatic synthesis of
distributed systems, where the players are represented as tokens on a Petri
net and are grouped into environment players and system players. As long as
the players move in independent parts of the net, they do not know of each
other; when they synchronize at a joint transition, each player gets informed
of the entire causal history of the other players.

We show that the synthesis problem for two-player Petri games under a global
safety condition is NP-complete and it can be solved within a non-
deterministic exponential upper bound in the case of up to 4 players.
Furthermore, we show the undecidability of the synthesis problem for Petri
games with at least 6 players under a local safety condition.

##  1 Introduction

A Petri game is a model for distributed, reactive systems. It is played on a
Petri net where each place is either a system place or an environment place.
The tokens on system places are system players and they control which
transitions to take next. The tokens on environment places are uncontrollable
environment players. Essential for Petri games is the informedness of the
players. As long as the players move in independent parts of the net, they do
not know of each other; when taking a joint transition they exchange
information about their complete causal history.

A winning strategy of the system players reacts to all options of the
environment players while satisfying a winning condition. Thereby, a decision
of a system player is based on its causal history, which grows infinitely in a
Petri net with loops. Different causal histories allow different decisions.
The _synthesis problem_ asks whether there is a winning strategy of the system
players. There have been several positive results on deciding the synthesis
problem for Petri games, obtained by restricting the number of players [9, 8]
or restricting the concurrent behaviour [14]. Also, an approach to bounded
synthesis has been proposed [7]. These papers considered as winning conditions
either local safety conditions where some ‘bad’ places must be avoided or
global safety conditions requiring that some sets of places are considered as
‘bad’ markings that must not be reached simultaneously.

Petri games are related to the model of control games played by multiple
processes on Zielonka automata. These games are also based on the causal
memory of their processes. A control game is a composition of local processes.
The processes communicate via shared actions that are either controllable or
uncontrollable. A strategy consists of one local controller for each process
that can restrict controllable actions based on the causal past of the
process. As in Petri games, a strategy must take into account all
uncontrollable behaviour in order to win. Unlike Petri games, one of the most
common winning conditions is a local termination condition. A formal
relationship of the two models has been presented in [2], where translations
from Petri games into control games and back have been presented such that
there is a weak bisimulation between the winning strategies of the two models.
When translating a control game into a Petri game, the processes are turned
one-by-one into players. These players switch between system and environment
players. The winning condition stays the same. The number of places (or
states) blows up exponentially when a game is translated in either direction.

Decidability results for control games have been obtained by restricting the
communication architecture [18, 11] or restricting the concurrent behaviour
[16, 17]. Another class of decidable control games are decomposable games [12]
that come with a local termination condition. Decomposable games are decidable
with up to 4 players [12]. In Sec. 3, we show that the synthesis problem for
Petri games under a global safety condition with up to 4 players is decidable
within an exponential upper time bound, and for two-player Petri games this
problem is NP-complete.

In [13], it has been shown that the synthesis problem is undecidable for
control games with at least 6 processes under a local termination condition.
This result, together with the translation into Petri games in [2], implies
that there are 6-player Petri games that are equipped with a local termination
condition for which the synthesis problem is undecidable. In Sec. 4, we show
in a direct proof that the synthesis problem for Petri games with 6 players is
also undecidable under a local safety condition.

The synthesis problem is of great interest because it automates the error-
prone implementation process while delivering implementations that are correct
by construction. It was first introduced in [4]. Pnueli and Rosner introduced
a setting of synchronous processes that communicate via shared variables [20].
For a single process, this setting is known to be decidable [3, 19]. For
multiple processes, the setting of Pnueli and Rosner is known to be
undecidable [20]. There have been positive decidability results on specific
architectures with multiple processes, including pipelines [21], rings [15],
and acyclic architectures [10]. However, all the positive results for multiple
processes have non-elementary complexity.

##  2 Foundations

In this section, we define branching processes and unfoldings as in [5]. Also,
we define Petri games and their winning strategies as in [9].

Some notation: the _power set_ of a set $A$ is denoted by $2^{A}=\\{B\mid
B\subseteq A\\}$, the _set of nonempty finite subsets_ of $A$ by
$2_{\mathit{nf}}^{A}=\\{B\mid B\subseteq A\land B\neq\emptyset\land B\text{ is
finite}\\}$, and the _set of finite subsets_ of $A$ by $2_{\mathit{f}}^{A}$.

A _Petri net_ or simply _net_ is a structure
$N=\mathcal{(P,T},\mathit{pre},\mathit{post},\mathit{In})$, where
$\mathcal{P}$ is the (possibly infinite) set of _places_ , $\mathcal{T}$ is
the (possibly infinite) set of _transitions_ , $\mathit{pre}$ and
$\mathit{post}$ are _flow mappings_ , $\mathit{In}\subseteq\mathcal{P}$ is the
_initial marking_ , and the following properties hold:
$\mathcal{P}\cap\mathcal{T}=\emptyset$, $\mathit{pre}:\mathcal{T}\to
2_{\mathit{nf}}^{\mathcal{P}}$, $\mathit{post}:\mathcal{T}\to
2_{\mathit{f}}^{\mathcal{P}}$. A Petri net is called finite if
$\mathcal{P}\cup\mathcal{T}$ is a finite set. The flow mappings $\mathit{pre}$
and $\mathit{post}$ are extended to places as usual: $\forall
p\in\mathcal{P}:\mathit{pre}(p)=\\{t\in\mathcal{T}\mid
p\in\mathit{post}(t)\\}$ and $\forall
p\in\mathcal{P}:\mathit{post}(p)=\\{t\in\mathcal{T}\mid
p\in\mathit{pre}(t)\\}$. A _marking_ $M$ of a Petri net $N$ is a _multiset_
over $\mathcal{P}$. In particular, $\mathit{In}$ is a marking. By convention,
a net named $N$ has the components
$\mathcal{(P,T},\mathit{pre},\mathit{post},\mathit{In})$, and analogously for
net with decorated names like $N_{0},N_{1},N_{2}$, where the components are
equally decorated.

A transition $t\in\mathcal{T}$ is _enabled_ at marking $M$ if
$\mathit{pre}(t)\subseteq M$. If $t$ is enabled, the transition $t$ can be
_fired_ , such that the new marking is
$M^{\prime}=M-\mathit{pre}(t)+\mathit{post}(t)$. This is denoted as
$M|t\rangle M^{\prime}$. This notation is extended to sequences of enabled
transitions $M|t_{1}\ldots t_{n}\rangle M^{\prime}$. A marking $M$ is
_reachable_ if there exists a sequence of successively enabled transitions
$(t_{k})_{k\in\\{1,\dots,n\\}}$ and $\mathit{In}|t_{1}\ldots t_{n}\rangle M$.
This sequence can be empty. The set of all reachable markings of a net $N$ is
denoted as $\mathcal{R}(N)$. A Petri net $N$ is called _safe_ , if for all
reachable markings $M(p)\leq 1$ holds for all $p\in\mathcal{P}$. Then, $M$ is
a subset of $P$. All Petri nets considered in this paper are safe.

A _node_ $x$ is a place or a transition $x\in\mathcal{P}\cup\mathcal{T}$. The
binary _flow relation_ $\mathcal{F}$ on nodes is defined as follows:
$x\,\mathcal{F}\,y$ if $x\in\mathit{pre}(y)$. A node $x$ is a _causal
predecessor_ of $y$, denoted as $x\leq y$, if $x\mathcal{F}^{+}y$.
Furthermore, $x\leq x$ holds for all $x\in\mathcal{P}\cup\mathcal{T}$. Two
nodes $x,y\in\mathcal{P}\cup\mathcal{T}$ are _causally related_ , if $x\leq y$
or $y\leq x$ holds. We say $x$ is a _causal successor_ of $y$, if $y\leq x$
holds.

Two nodes $x_{1},x_{2}\in\mathcal{P}\cup\mathcal{T}$ are _in conflict_ ,
denoted $x_{1}\\#x_{2}$, if there exist two transitions
$t_{1},t_{2}\in\mathcal{T}$, $t_{1}\neq t_{2}$ with $pre(t_{1})\cap
pre(t_{2})\neq\emptyset$ and $t_{i}\leq x_{i}$, $i=1,2$. A node
$x\in\mathcal{P}\cup\mathcal{T}$ is in self-conflict if $x\\#x$. Informally
speaking, two nodes are in conflict if two transitions exist that share some
place in their presets and each node is a causal successor of one of those
transitions. Two nodes $x,y\in\mathcal{P}\cup\mathcal{T}$ are _concurrent_ ,
denoted $x||y$, if they are neither causally related nor in conflict.

A Petri net $N$ is _finitely preceded_ , if for every node
$x\in\mathcal{P}\cup\mathcal{T}$ the set
$\\{y\in\mathcal{P}\cup\mathcal{T}\mid y\leq x\\}$ is finite. That set is the
causal history of a node. A Petri net $N$ is _acyclic_ , if the directed graph
$(\mathcal{P}\cup\mathcal{T},\mathcal{F})$ is acyclic. The following
definitions lead to the definition of a branching process.

An _occurrence net_ is a Petri net $N$ with the following properties: $N$ is
acyclic, finitely preceded, $\forall p\in\mathcal{P}:|\mathit{pre}(p)|\leq 1$,
no transition $t\in\mathcal{T}$ is in self-conflict, and
$\mathit{In}=\\{p\in\mathcal{P}\mid\,\mathit{pre}(p)=\emptyset\\}$.

A homomorphism from one Petri net to another maps each node to a node such
that the preset and postset relations are preserved including the initial
marking. Formally, let $N_{1}$ and $N_{2}$ be two Petri nets. Then a
_homomorphism_ from $N_{1}$ to $N_{2}$ is a mapping
$h:\mathcal{P}_{1}\cup\mathcal{T}_{1}\rightarrow\mathcal{P}_{2}\cup\mathcal{T}_{2}$
with following properties: $h(\mathcal{P}_{1})\subseteq\mathcal{P}_{2}$ and
$h(\mathcal{T}_{1})\subseteq\mathcal{T}_{2}$, for all transitions
$t\in\mathcal{T}_{1}$, $h$ restricted to $\mathit{pre}_{1}(t)$ is a bijection
between $\mathit{pre}_{1}(t)$ and $\mathit{pre}_{2}(h(t))$, for all
transitions $t\in\mathcal{T}_{1}$, $h$ restricted to $\mathit{post}_{1}(t)$ is
a bijection between $\mathit{post}_{1}(t)$ and $\mathit{post}_{2}(h(t))$, and
the restriction of $h$ to $\mathit{In}_{1}$ is a bijection between
$\mathit{In}_{1}$ and $\mathit{In}_{2}$. An _isomorphism_ is a bijective
homomorphism.

A run is represented by a (possibly infinite) firing sequence of transitions.
A branching process of a Petri net represents (possibly) multiple runs of the
underlying Petri net.

Branching process. A _branching process_ of a net $N_{0}$ is a pair
$B=(N,\pi)$, where $N$ is an occurrence net and $\pi$ a homomorphism from $N$
to $N_{0}$ such that: $(*)$ For all $t_{1},t_{2}\in\mathcal{T}$: if
$\mathit{pre}(t_{1})=\mathit{pre}(t_{2})$ and $\pi(t_{1})=\pi(t_{2})$, then
$t_{1}=t_{2}$.

An example of a Petri net and a branching process is shown in Fig. 1.

The notion of the set of all reachable markings of a branching process
$B=(N,\pi)$ is extended to $\mathcal{R}(B)=\mathcal{R}(N)$. By convention, a
branching Process $B$ has the components $(N_{B},\pi_{B})$. Throughout this
paper, $B_{1}$ and $B_{2}$ are branching processes of an underlying net
$N_{0}$. The property $(*)$ of the definition of a branching process ensures
that every run of the Petri net is represented at most once. Informally
speaking, a run only consists of concurrent and causally related nodes and a
node can be part of multiple runs. Nodes that are in conflict, cannot belong
to the same run.

$e_{1}$$t_{1}$$e_{2}$$t_{2}$$t_{3}$$e_{3}$$e_{4}$$N_{0}:$

$e^{1}_{1}$$t^{1}_{1}$${e^{2}_{1}}$$e^{1}_{2}$$t^{1}_{2}$${t^{2}_{2}}$$t^{1}_{3}$$e^{1}_{3}$${e^{2}_{3}}$$e^{1}_{4}$$\bullet$$\bullet$$\bullet$$B=(N,\pi):$

Figure 1: A Petri net $N_{0}$ on the left and a branching process $B=(N,\pi)$
of $N_{0}$ on the right. Places are shown as circles, transitions as boxes and
the preset and postset relations as arrows. The initial marking
$\\{e_{1},e_{2}\\}$ is represented by the black dots, the _tokens_. The
homomorphism $\pi$ from $N$ to $N_{0}$ is given as $\pi(e^{i}_{j})=e_{j}$ and
$\pi(t^{i}_{j})=t_{j}$. The transitions $t^{1}_{1}$ and $t^{1}_{2}$ are in
conflict, i.e., $t^{1}_{1}\\#t^{1}_{2}$, and also $t^{2}_{2}\\#t^{1}_{2}$,
$t^{1}_{3}\\#t^{1}_{2}$, $t^{2}_{2}\\#t^{1}_{3}$.

Homomorphism on branching processes. A _homomorphism_ from $B_{1}$ to $B_{2}$
is a homomorphism $h$ from $N_{1}$ to $N_{2}$ such that $\pi_{2}\circ
h=\pi_{1}$. The branching processes $B_{1}$ and $B_{2}$ are isomorphic if
there exists an isomorphism from $B_{1}$ to $B_{2}$ which is denoted as
$B_{1}\cong B_{2}$.

A natural partial order on branching processes is defined in the following.

Subprocess relation of branching processes. $B_{1}$ approximates $B_{2}$,
denoted by $B_{1}\leq B_{2}$, if there exists an injective homomorphism from
$B_{1}$ to $B_{2}$.

Now we define the unfolding of a net as the maximal branching process that
contains all (possibly infinite) runs of a net. Loosely speaking, the
unfolding of a net is an acyclic net with the same behaviour as the original
net, but where each place and transition has a unique causal history.

Unfolding. The _unfolding_ $\textit{unf}(N_{0})$ of a Petri net $N_{0}$ is the
maximal branching process with respect to the subprocess relation $\leq$ of
branching processes. This definition is unique up to isomorphism. We refer to
the components of the unfolding as $\mathcal{T}_{\textit{unf}(N_{0})}$,
$\mathcal{P}_{\textit{unf}(N_{0})}$, $\mathit{pre}_{\textit{unf}(N_{0})}$,
$\mathit{post}_{\textit{unf}(N_{0})}$, and
$\mathit{In}_{\textit{unf}(N_{0})}$.

In Fig. 1, the branching process $B$ is the unfolding of the Petri net $N_{0}$
assuming that the dots to the left of the place ${e^{2}_{1}}$ indicate that
the branching process continues infinitely in the same way.

We continue with the definition of a Petri game. A Petri game is played on a
finite and safe Petri net. Tokens may transit from a system place to an
environment place and vice versa.

Petri game. A _Petri game_ on an underlying finite and safe Petri net $N_{0}$
is a tuple $G=(\mathcal{P}^{S}_{0},\mathcal{P}^{E}_{0},\mathcal{T}_{0},$
$\mathit{pre}_{0},\mathit{post}_{0},\mathit{In}_{0},\mathcal{B})$, where the
set $\mathcal{P}_{0}$ of places of $N_{0}$ is partitioned into disjoint sets
of _system places_ $\mathcal{P}^{S}_{0}$, and _environment places_
$\mathcal{P}^{E}_{0}$, and where $\mathcal{B}\in 2^{\mathcal{P}_{0}}$ is the
set of _bad markings_.

A winning strategy of a Petri game is a branching process of the underlying
Petri net of the game. A strategy must satisfy 4 properties that are
reasonable properties of implementations of processes. Beside a _safety_
property, each process must act deterministically, _determinism_ , and at
least one process must enable a transition if possible, _deadlock avoiding_.
Loosely speaking, the _justified refusal_ property forces the system players
to commit to transitions that are always allowed on their current place.
Strategies for Petri games are obtained by cutting out parts of the unfolding.

Winning strategy A _winning strategy_ $\sigma$ of a Petri-game
$G=(\mathcal{P}^{S}_{0},\mathcal{P}^{E}_{0},\mathcal{T}_{0},\mathit{pre}_{0},\mathit{post}_{0},\mathit{In_{0}},\mathcal{B})$
with underlying Petri-net $N_{0}$ is a branching process $\sigma=(N,\pi)$ of
$N_{0}$ satisfying the following properties:

  1. 1.

Justified refusal: Let $C\subseteq\mathcal{P}$ be a set of pairwise concurrent
places and $t\in\mathcal{T}_{0}$ a transition with
$\pi(C)=\mathit{pre}_{0}(t)$. If no $t^{\prime}\in\mathcal{T}$ with
$\pi(t^{\prime})=t$ and $\mathit{pre}(t^{\prime})=C$ exists, then there exists
a place $p\in C$ with $\pi(p)\in\mathcal{P}^{S}_{0}$, such that
$t\notin\pi(\mathit{post}(p))$.

  2. 2.

Safety: For all reachable markings $M\in\mathcal{R}(N)$ it holds that
$\pi(M)\notin\mathcal{B}$.

  3. 3.

Determinism: For all $p\in\mathcal{P}$ with $\pi(p)\in\mathcal{P}^{S}_{0}$ and
for all reachable markings $M$ in $N$ with $p\in M$ there exists at most one
transition $t\in\mathit{post}(p)$, which is enabled in $M$.

  4. 4.

Deadlock avoiding: For all reachable markings $M$ in $N$ there exists an
enabled transition, if a transition is enabled in $\pi(M)$ in the underlying
Petri-net $N_{0}$.

We refer to a token on a system place as a system player, and a token on an
environment place as an environment player. The _justified refusal_ property
ensures that a system player allows all instances of an outgoing transition or
no instance at all. The global _safety_ property ensures that no bad markings
are reachable. The _determinism_ property ensures that for each system place
at most one transition is enabled in every reachable marking. The _deadlock
avoiding_ property ensures that the system allows at least one transition in
every reachable marking if an enabled transition exists in that marking, e.g.
the system players cannot add deadlocks to the existing deadlocks in the Petri
net by forbidding transitions.

The _unfolding_ $\textit{unf}(G)$ of a Petri game $G$ is like the unfolding
$\textit{unf}(N_{0})=(N,\pi)$ of the underlying Petri net $N_{0}$ of $G$,
additionally keeping the distinction between system and environment: a place
$p$ in $N$ is a system place if $\pi(p)\in\mathcal{P}^{S}_{0}$ and an
environment place if $\pi(p)\in\mathcal{P}^{E}_{0}$. A winning strategy
$\sigma_{G}$ of $G$ can be seen as a subprocess of $\textit{unf}(G)$.

Fig. 2 shows a Petri game with 4 players modelling the control of a room with
two doors that must not be opened at the same time so that the two places of
the bad marking $\\{{O^{1},O^{2}}\\}$ are not reached simultaneously. After
receiving a request to open door via transition $r^{1}$ the first system
player on place $S^{12}$ can decide to proceed with communicating (transition
$t$) or without communicating (transition $n^{1}$) to the second system
player, then on place $S^{22}$. On place $S^{13}$ the system player chooses
between opening the door ($o^{1}$) or denying the request ($d^{1}$) for the
environment player waiting on $W^{1}$. From place $S^{14}$ the system player
can close the door it has opened before ($c^{1}$). The second system player
has the same options after receiving a request via $r^{2}$. After that, if
both players open their doors the bad marking $\\{{O^{1},O^{2}}\\}$ is
reached. At least one system player has to deny the request to win the game.

$P^{1}$$p^{1}$$C^{1}$$r^{1}$$S^{11}$$S^{12}$$W^{1}$$n^{1}$$S^{13}$$d^{1}$$o^{1}$$O^{1}$$c^{1}$$S^{14}$$t$$S^{21}$$S^{22}$$r^{2}$$P^{2}$$p^{2}$$C^{2}$$W^{2}$$n^{2}$$S^{23}$$d^{2}$$o^{2}$$O^{2}$$c^{2}$$S^{24}$$G$:

Figure 2: A Petri game $G$: the grey places belong to the system players and
the white places to the environment players. There are two doors and two
system players taking requests to open the door. After a request the system
players decide whether to communicate and open their door afterwards. The bad
marking $\\{O^{1},O^{2}\\}$ is reached if the system players decide to open
both doors simultaneously.

Fig. 3 shows an initial part of the unfolding of the Petri game in Fig. 2. The
parts that are not greyed out are the initial parts of a winning strategy.
Here, the system player agree on communicating via $t_{1}$. The first player
decides to open its door via transition $o_{2}^{1}$ while the other door
remains closed via transition $d_{2}^{2}$. After the transition $c_{2}^{1}$
the first door is closed again. The following is not shown in Fig. 3 anymore:
after both players have received another opening request via $r^{1}_{2}$ and
$r^{2}_{2}$, respectively, the winning strategy could continue opening door 2
and keeping door 1 closed since the different causal histories allow different
decisions.

According to the definition of a winning strategy it is also possible that a
winning strategy denies all requests to open a door. The example is chosen
with foresight for the content in Section 3.

$P^{1}_{1}$$p^{1}_{1}$$C_{1}^{1}$$r_{1}^{1}$$S^{11}_{1}$$S^{12}_{1}$$W^{1}_{1}$$n^{1}_{1}$$S^{13}_{1}$$S^{13}_{2}$$d_{1}^{1}$$o_{1}^{1}$$O_{1}^{1}$$c_{1}^{1}$$S^{14}_{1}$$C_{3}^{1}$$S^{11}_{3}$$S^{11}_{2}$$C^{1}_{2}$$d^{1}_{2}$$o^{1}_{2}$$S^{11}_{4}$$C^{1}_{4}$$O^{1}_{2}$$S^{14}_{2}$$c^{1}_{2}$$C^{1}_{5}$$S^{11}_{5}$$t_{1}$$S^{21}_{1}$$S^{22}_{1}$$r_{1}^{2}$$P_{1}^{2}$$p^{2}_{1}$$C_{1}^{2}$$W_{1}^{2}$$n^{2}_{1}$$S^{23}_{2}$$S^{23}_{1}$$d_{1}^{2}$$o_{1}^{2}$$S^{24}_{1}$$O_{1}^{2}$$c_{1}^{2}$$C_{3}^{2}$$S^{21}_{3}$$S^{21}_{2}$$C^{2}_{2}$$d_{2}^{2}$$o_{2}^{2}$$S^{21}_{4}$$C_{4}^{2}$$O^{2}_{2}$$s^{24}_{2}$$c_{2}^{2}$$C_{5}^{2}$$S^{21}_{5}$$\sigma_{G}=(N,\pi)$:

Figure 3: An initial part of the unfolding of the Petri game $G$ in Fig. 2.
The nodes that are not greyed out form an initial part of a winning strategy
$\sigma_{G}$ where door 1 gets opened and door 2 remains closed after the
system players have communicated. The homomorphism $\pi$ is defined
analogously to that in Fig. 1.

##  3 Decidability Results

In this section, we show that the synthesis problem for Petri games with up to
4 players under a global safety condition is decidable in non-deterministic
exponential time (NEXP), and NP-complete in the 2-player case. In [12], a
related result is shown that the synthesis problem for 4-process control games
with a local termination condition is decidable. The translation [2] of this
result to Petri games gives a decidability result for Petri games with 4
players with a local termination condition, without process generation and
deletion. There are no complexity bounds for the 4-player case given in [12],
and the translation to Petri games already generates an exponential blow up in
the number of nodes [2].

A Petri game $G$ is called a _K-player Petri game_ , $K\in\mathbb{N}$, if and
only if for all reachable markings $M\in\mathcal{R}(G)$ it holds that $|M|\leq
K$. Two-player Petri games can be seen as a natural generalisation of infinite
games on graphs with a safety winning condition. NP-hardness is established by
a reduction of the 3-SAT problem to 2-player Petri games.

######  Lemma 3.1.

There exists a polynomial-time reduction of the 3-SAT problem to the synthesis
problem of two-player Petri games.

###### Proof.

Let $F=(x^{1}_{1}\lor x^{1}_{2}\lor x^{1}_{3})\land\ldots\land(x^{n}_{1}\lor
x^{n}_{2}\lor x^{n}_{3})$ be an instance of the 3-SAT problem in conjunctive
normal form where all clauses consist of exactly three literals and where
$x^{i}_{j}$, $i=1,\ldots,n$ and $j=1,2,3$, is a positive or negative (with
overline) literal from the set $\\{x_{1},\bar{x}_{1},\ldots
x_{m},\bar{x}_{m}\\}$.

$x_{1}$$\bar{x}_{1}$$\bullet$$\bullet$$\bullet$$x_{n}$$\bar{x}_{n}$$x^{1}_{2}$$x^{1}_{1}$$x^{1}_{3}$$\bullet$$\bullet$$\bullet$$x^{n}_{2}$$x^{n}_{1}$$x^{n}_{3}$

Figure 4: 3-SAT problem $F$ as a Petri game. The top system player chooses
sequentially the truth value for $x_{1},\ldots x_{n}$. The bottom system
player has to choose a literal for each clause according to the truth values
chosen by the top player. The bad markings are $\\{\\{x_{k},x^{i}_{j}\\}\mid
x^{i}_{j}=\bar{x}_{k}\\}\cup\\{\\{\bar{x}_{k},x^{i}_{j}\\}\mid
x^{i}_{j}=x_{k}\\}$. So every time the bottom player chooses a literal that is
not chosen by the top system player a bad marking is reached, e.g. the top
player chooses $x_{1}$ and the bottom player $x^{1}_{3}$ where
$x^{1}_{3}=\bar{x}_{1}$.

Fig. 4 shows the Petri game of $F$. If $F$ is satisfiable, the top system
player chooses the transitions according to the boolean assignment that
satisfies $F$, for example $\bar{x}_{1}$ if the truth value of $x_{1}$ is
false under the boolean assignment. The bottom system player chooses the
literal that is true under the boolean assignment in each clause, for example
if $x^{1}_{1}=\bar{x}_{1}$, she may choose $x^{1}_{1}$ since the top system
player chooses it. Both system players do not know how when the transition of
the other player are fired such that it has to be correct for all possible
orders of execution, for example the top player could have chosen the truth
value for $x_{n}$ already before the bottom player chose the literal for the
first clause.

Conversely, the top player’s choices yield a boolean assignment that satisfies
$F$ if the Petri game shown has a winning strategy since the bottom player
chooses one literal of each clause that must be true under the boolean
assignment. ∎

Note that the 2-player case is NP-hard even without an environment player. The
matching upper bound is established later, along with the complexity of the
4-player case.

The idea of solving 4-player Petri games is to find game states where a
winning strategy can be repeated and still win. A few definitions are
necessary to formalise repeating a part of a winning strategy. The following
definitions about branching processes are equivalent to those in [6].

Cut. The reachable markings in a branching process $B$ are called _cuts_. A
cut is a maximal set of pairwise concurrent places [8].

Future of a cut. We define the branching process $\mathit{Fut}(B,C)$ of a cut
$C\subseteq\mathcal{P}_{B}$ as follows:
$\mathcal{P}_{\mathit{Fut}(B,C)}\cup\mathcal{T}_{\mathit{Fut}(B,C)}=\\{x\in\mathcal{P}_{B}\cup\mathcal{T}_{B}\mid\forall
p\in C:p\leq x\lor p||x\\}$, the mappings $preset$ and $\mathit{post}$ are the
mappings $\mathit{pre}_{B}$ and $\mathit{post}_{B}$ restricted to
$\mathcal{T}_{\mathit{Fut}(B,C)}$, and $\mathit{In}_{\mathit{Fut}(B,C)}=C$.
Generally, the _future_ $\mathit{Fut}(B,C)$ is not a branching process of the
underlying net $N_{0}$ of $B$ (i.e.
$\pi_{B}:\mathcal{T}_{B}\cup\mathcal{P}_{B}\to\mathcal{T}_{0}\cup\mathcal{P}_{0})$
but it is a branching process of the net
$(\mathcal{P}_{0},\mathcal{T}_{0},\mathit{pre}_{0},\mathit{post}_{0},\pi_{B}(C))$,
i.e. $\mathit{Fut}(B,C)$ is a branching process of $N_{0}$ if
$\pi_{B}(C)=\mathit{In}_{0}$. (This definition is equal to the definition of
${\Uparrow}\mathit{Configuration}$ in [6].)

Informally speaking, the definition of the future of a cut coincides with the
intuition that it is the branching process that follows after that cut.

Last known cut and last known marking. The _last known cut_ $\mathit{lkc}(t)$
of a transition $t$ of a branching process $B$ is defined as
$\mathit{lkc}(t)=\\{p\in\mathcal{P}_{B}\mid p\nless t\land\forall
t^{\prime}\in\mathit{pre}_{B}(p):t^{\prime}\leq t\\}$. Informally speaking,
this cut is reached by firing all transitions that are causal predecessors of
$t$. The _last known marking_ $\mathit{lkm}(t)$ is defined as
$\pi_{B}(\mathit{lkc}(t))$, which is the marking reached in the underlying
Petri net. (The $\mathit{lkc}$ is the cut of a _local configuration_ [6])

A _cut_ and _glue_ operation formalises the process of copying the future of
one cut to another cut of a strategy. Later, the actual requirements for when
to copy are defined. In the following, $B$ and $B^{\prime}$ are branching
processes of (possibly different) nets.

Cut.
$B-B^{\prime}=(\mathcal{P}_{B}\setminus(\mathcal{P}_{B^{\prime}}\setminus\mathit{In}_{B^{\prime}}),\mathcal{T}_{B}\setminus\mathcal{T}_{B^{\prime}},\mathit{pre}_{B}\restriction_{\mathcal{T}_{B-B^{\prime}}},\mathit{post}_{B}\restriction_{\mathcal{T}_{B-B^{\prime}}},\mathit{In}_{B})$

If $B^{\prime}$ is the future of a cut of $B$, the cut operation removes
$B^{\prime}$ from $B$ leaving only the initial marking of $B^{\prime}$ in $B$.

Glue.
$B+B^{\prime}=(\mathcal{P}_{B}\cup\mathcal{P}_{B^{\prime}},\mathcal{T}_{B}\cup\mathcal{T}_{B^{\prime}},\mathit{pre}_{B+B^{\prime}},\mathit{post}_{B+B^{\prime}},\mathit{In}_{B})$,
where
$\mathit{pre}_{B+B^{\prime}}(t)=\begin{cases}\mathit{pre}_{B}(t)&t\in\mathcal{T}_{B}\\\
\mathit{pre}_{B^{\prime}}(t)&t\in\mathcal{T}_{B^{\prime}}\end{cases}$, and
analogously $\mathit{post}_{B+B^{\prime}}$.

If the initial marking of $B^{\prime}$ is a cut in $B$, $B^{\prime}$ gets
glued to that cut. Generally, $B-B^{\prime}$ and $B+B^{\prime}$ are not
branching processes. However, if there are two cuts
$C_{1},C_{2}\subseteq\mathcal{P}_{B}$ with $\pi_{B}(C_{1})=\pi_{B}(C_{2})$
cutting out the future of $C_{2}$ and glueing an isomorphic copy (this is just
a necessary renaming) of the future of $C_{1}$ to $C_{2}$ yields a branching
process.

Cut and glued branching process. Let ${\mathit{Fut}(B,C_{1})}^{\prime}$ be an
isomorphic copy of $\mathit{Fut}(B,C_{1})$, ${\mathit{Fut}(B,C_{1})}^{\prime}$
$\cong\mathit{Fut}(B,C_{1})$, such that
$\mathit{In}_{{\mathit{Fut}(B,C_{1})}^{\prime}}=C_{2}$ and
$(\mathcal{P}_{B}\cup\mathcal{T}_{B})\cap(\mathcal{P}_{{\mathit{Fut}(B,C_{1})}^{\prime}}\cup\mathcal{T}_{{\mathit{Fut}(B,C_{1})}^{\prime}})=C_{2}$.
The cut and glued branching process $B_{C_{1}\rightarrow C_{2}}$ is the
branching process $B_{C_{1}\rightarrow
C_{2}}=B-\mathit{Fut}(B,C_{2})+{\mathit{Fut}(B,C_{1})}^{\prime}$. This
definition is unique up to isomorphism.

######  Definition 3.1 (Imitable cuts).

Let $\sigma$ be a winning strategy of a Petri game $G$. A cut $C_{2}$ is
imitable by a cut $C_{1}$ if $\sigma_{C_{1}\rightarrow C_{2}}$ is a winning
strategy.

Now we define the actual cuts that are imitable. The first kind of these cuts
are cuts where a subset of players take transitions without communicating to
the remaining players until all players of this subset synchronise at a joint
transition for the second time. In the following, we fix $\sigma$ as a winning
strategy of a Petri game $G$.

######  Definition 3.2 (Partial repetition cuts).

Let $t_{1},t_{2}\in\mathcal{T}_{\sigma}$. The cuts $\mathit{lkc}(t_{1})$ and
$\mathit{lkc}(t_{2})$ are _partial repetition cuts_ , denoted
$\mathit{prc}(t_{1},t_{2})$, if
$\mathit{lkm}(t_{1})=\mathit{lkm}(t_{2})\land\mathit{lkc}(t_{1})\setminus\mathit{post}(t_{1})=\mathit{lkc}(t_{2})\setminus\mathit{post}(t_{2})$.
The partial repetitions cuts $\mathit{prc}(t_{1},t_{2})$ are called a _loop_ ,
denoted $\mathit{prc}_{\mathit{loop}}(t_{1},t_{2})$ if $t_{1}<t_{2}$.

######  Lemma 3.2 (Partial repetition cuts are imitable).

For transitions $t_{1},t_{2}\in\mathcal{T}_{\sigma}$,
$\mathit{prc}(t_{1},t_{2})$ implies that $\mathit{lkc}(t_{2})$ is imitable by
$\mathit{lkc}(t_{1})$ and vice versa.

###### Proof by contradiction.

We show that
$\sigma_{\mathit{lkc}(t_{1})\rightarrow\mathit{lkc}(t_{2})}=\sigma-\mathit{Fut}(\sigma,\mathit{lkc}(t_{2}))+{\mathit{Fut}(B,\mathit{lkc}(t_{1}))}^{\prime}$
is a winning strategy. Suppose that there exists a cut
$C\subseteq\mathcal{P}_{\sigma_{\mathit{lkc}(t_{1})\rightarrow\mathit{lkc}(t_{2})}}$
such that one of the properties of the winning strategy is violated.

We distinguish two cases: The first case is that there exists a place $p\in C$
such that $t_{2}\leq p$. Then,
$C\subseteq\mathcal{P}_{\mathit{Fut}(\sigma_{\mathit{lkc}(t_{1})\rightarrow\mathit{lkc}(t_{2})},\mathit{lkc}(t_{2})),}$
holds. Since
$\mathit{Fut}(\sigma_{\mathit{lkc}(t_{1})\rightarrow\mathit{lkc}(t_{2})},\mathit{lkc}(t_{2}))=\mathit{Fut}(\sigma,\mathit{lkc}(t_{1}))^{\prime}\cong\mathit{Fut}(\sigma,\mathit{lkc}(t_{1}))$
it follows directly that $\sigma$ is not a winning strategy if
$\sigma_{\mathit{lkc}(t_{1})\rightarrow\mathit{lkc}(t_{2})}$ is not winning.

The second case is that there exists no place $p\in C$ such that $t_{2}\leq
p$, i.e. $\forall p\in C:p\leq t_{2}\lor p\\#t_{2}\lor p||t_{2}$ holds. Since
the last known cuts of $t_{1}$ and $t_{2}$ are equal except for
$\mathit{post}(t_{1})$ and $\mathit{post}(t_{2})$ the branching processes
$\mathit{Fut}(\sigma,\mathit{lkc}(t_{2}))$ and
$\mathit{Fut}(\sigma,\mathit{lkc}(t_{1}))$ are isomorphic up to the nodes that
are causal successors of $t_{1}$ and $t_{2}$ respectively. This means that all
transitions and places that are not causal successors of $t_{2}$ are only
renamed by constructing
$\sigma_{\mathit{lkc}(t_{1})\rightarrow\mathit{lkc}(t_{2})}$. Since there is
no place in $C$ that is a causal successor of $t_{2}$ there is no transition
enabled in $C$ that could have been added or removed. It follows that $\sigma$
is not a winning strategy, if
$\sigma_{\mathit{lkc}(t_{1})\rightarrow\mathit{lkc}(t_{2})}$ is not a winning
strategy. ∎

$S^{21}_{1}$$S^{22}_{1}$$r_{1}^{2}$$P_{1}^{2}$$p^{2}_{1}$$C_{1}^{2}$$W_{1}^{2}$$n^{2}_{1}$$S^{23}_{1}$$d_{1}^{2}$$C^{2}_{2}$$S^{21}_{2}$$p^{2}_{2}$$P_{2}^{2}$$r_{2}^{2}$$W_{2}^{2}$$S^{22}_{2}$$S^{11}_{1}$$C^{1}_{1}$$\mathit{lkc}(r^{2}_{1})$$\mathit{lkc}(r^{2}_{2})$

Figure 5: Example of partial repetition cuts. Assume that this is a part of a
winning strategy where the second system player denies ($d^{2}_{1}$) the first
request ($r^{2}_{1}$) to open the door without communicating with the other
system player via transition $t$. Here, the last known cuts of $r^{2}_{1}$ and
$r^{2}_{2}$ are
$\mathit{lkc}(r^{2}_{1})=\\{C^{1}_{1},S^{11}_{1},S^{22}_{1},W^{2}_{1}\\}$ and
$\mathit{lkc}(r^{2}_{2})=\\{C^{1}_{1},S^{11}_{1},S^{22}_{2},W^{2}_{2}\\}$, so
$\mathit{lkm}(r^{2}_{1})=\mathit{lkm}(r^{2}_{2})$. Thus, a partial repetition
cut (that is a loop) occurs
$\mathit{prc}_{\mathit{loop}}(r^{2}_{1},r^{2}_{2})$.

In Fig. 5 is an example of partial repetition cuts. Note that not all of those
partial repetition cuts are loops as the players can reach the same places in
the underlying Petri net by taking different transitions. Partial repetition
cuts are defined regardless of the number of players in a Petri game, i.e,
these cuts are imitable in any Petri game.

Maximally repeated strategy. Since the nodes of a branching process are
countable we can construct by induction over the partial repetition cuts of a
winning strategy $\sigma$ a winning strategy $\sigma^{\mathit{pr}}$ where
$\mathit{prc}(t_{1},t_{2})$ implies that
$\mathit{Fut}(\sigma^{\mathit{pr}},t_{1})\cong\mathit{Fut}(\sigma^{\mathit{pr}},t_{2})$.
$\sigma^{\mathit{pr}}$ denotes a _maximally repeated strategy_ of $\sigma$.

The partial repetition cuts have a useful implication for the case with up to
4 players: if two players do not take any joint transition with one of the two
remaining players they will get to a partial repetition cut eventually. The
idea of the following definition of a synchronisation segment is based on this
implication. Informally speaking, a synchronisation segment describes the part
starting from the last known cut of a transition $t$ until all other players
are causal successors of this transition or the strategy can be repeated due
to the partial repetition cuts. Here, the idea of when to repeat a strategy is
that if all players play identically starting from the last known cut of
transition $t$ until they get to know of transition $t$ the strategy can be
repeated after transition $t$.

######  Definition 3.3 (Synchronisation segment).

The _synchronisation segment_ $\mathit{Seg}(t)$ of a transition
$t\in\mathcal{T}_{B}$ of a branching process $B$ is defined as a smallest
branching process (with respect to $\leq$) such that
(1.) $\mathit{Seg}(t)\leq\mathit{Fut}(B,\mathit{lkc}(t))$ and
(2.) $\forall
t^{\prime}\in\mathcal{T}_{\mathit{Fut}(B,\mathit{lkc}(t))}:t^{\prime}\notin\mathcal{T}_{\mathit{Seg}(t)}\Rightarrow$
(a) ${(\forall p\in\mathit{pre}_{B}(t^{\prime}):t\leq p})\lor$
(b) ${(\exists
t_{1},t_{2},t_{3}\in\mathcal{T}_{\mathit{Seg}(t)}:\mathit{prc}_{\mathit{loop}}(t_{1},t_{2})\land
t_{3}\leq t_{2}\land\mathit{prc}(t^{\prime},t_{3}))}$

For a transition $t^{\prime}\in\mathit{Fut}(B,\mathit{lkc}(t))$ that is not in
$\mathcal{T}_{\mathit{Seg}(t)}$, all places in its preset are causal
successors of $t$ (2.a) or there is a transition $t_{3}$ with
$\mathit{prc}(t^{\prime},t_{3})$ within a loop (2.b). So, the parts of a
winning strategy that get repeated due to partial repetition cuts are included
in the synchronisation segment. An example of a synchronisation segment is
shown in Fig. 6 and Fig. 7. _Synchronisation equivalent cuts_ are those cuts
where the synchronisation segments are isomorphic.

$P^{1}_{1}$$p^{1}_{1}$$C_{1}^{1}$$r_{1}^{1}$$S^{11}_{1}$$S^{12}_{1}$$W^{1}_{1}$$S^{13}_{2}$$o^{1}_{2}$$O^{1}_{2}$$S^{14}_{2}$$t_{1}$$S^{21}_{1}$$S^{22}_{1}$$r_{1}^{2}$$P_{1}^{2}$$p^{2}_{1}$$C_{1}^{2}$$W_{1}^{2}$$S^{23}_{2}$$d_{2}^{2}$$S^{21}_{4}$$C_{4}^{2}$$\mathit{Seg}(t_{1})$ptNo
more transitions are added due to 2.a.

Figure 6: A subprocess of $\sigma_{G}$ of Fig. 3 is shown. The nodes inside
the dashed, blue box are the nodes of the synchronisation segment
$\mathit{Seg}(t_{1})$. The initial marking is
$\mathit{In}_{\mathit{Seg}(t_{1})}=\\{W^{1}_{1},S^{13}_{2},S^{23}_{2},W^{2}_{1}\\}$.
This segment ends after the transitions $o^{1}_{2}$ and $d^{2}_{2}$ since
$t_{1}<O^{1}_{2},S^{14}_{2},S^{21}_{4},C^{2}_{4}$. So, if $\sigma_{G}$ repeats
to open the first door and keeping the second door closed after taking the
transition $t$ the winning strategy could repeat itself due to synchronisation
equivalent cuts.

$S^{21}_{1}$$S^{22}_{1}$$r_{1}^{2}$$P_{1}^{2}$$p^{2}_{1}$$C_{1}^{2}$$W_{1}^{2}$$n^{2}_{1}$$S^{23}_{1}$$d_{1}^{2}$$C^{2}_{2}$$S^{21}_{2}$$p^{2}_{2}$$P_{2}^{2}$$r_{2}^{2}$$W_{2}^{2}$$S^{22}_{2}$$S^{11}_{1}$$r^{1}_{1}$$P^{1}_{1}$$p^{1}_{1}$$C^{1}_{1}$$W_{1}^{1}$$S^{12}_{1}$ptNo
more transitions are added due to 2.b.$\mathit{Seg}(r^{1}_{1})$

Figure 7:  A branching process of the Petri game $G$ of Fig. 2 is shown. The
nodes inside the dashed, blue box are the nodes of the synchronisation segment
$\mathit{Seg}(r^{1}_{1})$.

######  Definition 3.4 (Synchronisation equivalent cuts).

Let $\sigma^{\mathit{pr}}$ be a maximally repeated winning strategy of a Petri
game $G$ and $t_{1},t_{2}\in\mathcal{T}_{\sigma^{\mathit{pr}}}$. The cuts
$\mathit{lkc}(t_{1})$ and $\mathit{lkc}(t_{2})$ are _synchronisation
equivalent cuts_ , denoted $\mathit{sqc}(t_{1},t_{2})$, if
$\mathit{Seg}(t_{1})\cong\mathit{Seg}(t_{2})$. $\mathit{sqc}(t_{1},t_{2})$ is
called an _s-loop_ , denoted $\mathit{sqc}_{\mathit{loop}}$, if $t_{1}<t_{2}$.

Now, we show that a winning strategy can be repeated after synchronisation
equivalent cuts.

######  Lemma 3.3 (Synchronisation equivalent cuts are imitable).

For transitions $t_{1},t_{2}\in\mathcal{T}_{\sigma^{\mathit{pr}}}$,
$\mathit{sqc}(t_{1},t_{2})$ implies that $\mathit{lkc}(t_{2})$ is imitable by
$\mathit{lkc}(t_{1})$ and vice versa.

###### Proof.

We show that
$\sigma^{\mathit{pr}}_{\mathit{lkc}(t_{1})\rightarrow\mathit{lkc}(t_{2})}=\sigma^{\mathit{pr}}-\mathit{Fut}(\sigma,\mathit{lkc}(t_{2}))+{\mathit{Fut}(\sigma,\mathit{lkc}(t_{1}))}^{\prime}$
is a winning strategy. Since $\mathit{Seg}(t_{1})\cong\mathit{Seg}(t_{2})$ the
construction is only a renaming for the nodes in the synchronisation segment
and for those that get repeated due to the partial repetition cuts. Thus, only
nodes that are causal successors of $t_{2}$ may be removed or added. Now, the
proof works in the same way as the proof of Lemma 3.2, that partial repetition
cuts are imitable. ∎

We show that 4-player Petri games can be solved in NEXP with the help of Lemma
3.2 and Lemma 3.3. A winning prefix of sufficient size is guessed from which a
winning strategy can be constructed. A branching process $B$ is a _winning
prefix_ if there exists a winning strategy $\sigma$ with $B\leq\sigma$.

######  Theorem 3.4.

The synthesis problem of 2-player Petri games is NP-complete and in NEXP for
3- and 4-player Petri games.

###### Proof.

Structure of this proof: from the 2-player case over the 3-player case to the
4-player case the size of a winning prefix is determined to guarantee that a
winning strategy can be constructed by repeating the futures of imitable cuts.
A prefix of appropriate size is guessed and it is checked if it is winning.
The prefix does not contain any causal successors of transitions $t_{2}$ if
$\exists
t_{1}:\mathit{prc}_{\mathit{loop}}(t_{1},t_{2})\lor\mathit{sqc}_{\mathit{loop}}(t_{1},t_{2})$.
Also, it does not contain causal successors of transitions $t_{4}$, if
$\exists t_{1},t_{2},t_{3}:t_{3}\leq
t_{2}\land((\mathit{prc}(t_{3},t_{4})\land\mathit{prc}_{\mathit{loop}}(t_{1},t_{2}))\lor(\mathit{sqc}(t_{2},t_{3})\land\mathit{sqc}_{\mathit{loop}}(t_{1},t_{2})))$.
Let $T$ be the number of transitions of the Petri game.

If a player does not take any joint transition she eventually repeats a place
she lays on, i.e. she reaches a partial repetition cut. This occurs after at
most $T$ transitions. Otherwise, the two players take a joint transition after
at most $T$ transitions. Since there are at most $T$ different joint
transitions, a winning prefix from which a winning strategy can be constructed
is at most of size $\mathcal{O}(T^{2})$. To check if the guessed prefix is
winning, we have to check all reachable markings for the winning properties.
In a safe Petri net with $T^{2}$ transitions and at most two tokens there are
at most $T^{4}$ reachable markings. Thus, guessing a winning prefix and
checking if it is winning takes time in $\mathcal{O}(|\mathcal{T}|^{4})$,
which shows together with Lemma 3.1 that the synthesis problem for two-player
Petri games is NP-complete.

In the 3-player case, it holds for the same reasons as in the 2-player case
that each pair of two players reaches partial repetition cuts after at most
$T^{2}$ transitions without taking a joint transition with the remaining third
player. The remaining third player can take up to $T$ transitions herself
before reaching a partial repetition cut or taking a joint transition.
Therefore, a synchronisation segment has at most $T^{2}+T$ transitions
resulting in at most $2^{(T^{2}+T)^{2}}$ non-isomorphic synchronisation
segments. Therefore, a synchronisation equivalent cut is always reached after
at most $2^{(T^{2}+T)^{2}}$ transitions such that the winning prefix can be
extended step by step by reaching synchronisation equivalent cuts again and
again. Thus, the size of a winning prefix is in $\mathcal{O}(2^{T^{4}})$. To
check if the prefix is winning takes polynomial time in its size and it
follows that the 3-player case is decidable in NEXP.

In a 4-player Petri game, it also holds that each pair of two players reaches
partial repetition cuts after at most $T^{2}$ transitions without taking a
joint transition with one of the two remaining players. So, there are two
pairs of players that can take $T^{2}$ transitions until they reach partial
repetition cuts or one player of each pair communicate with each other. This
leaves the other two players until they reach partial repetition cuts or take
a joint transition again after $T^{2}$ transitions. Thus, there are at most
$2^{3T^{2}}$ non-isomorphic synchronisation segments. Therefore, the size of a
winning prefix of a 4-player Petri game that needs to be checked if it is
winning is in $\mathcal{O}(2^{6T^{2}})$. So the bound is in NEXP. Note that if
more than 2 players take a joint transition the size of the synchronisation
segments decreases. ∎

This construction does not work for the 5-player case. The problem that occurs
is tricky to see. Assume there is a group of 3 players and a group of 2
players that take joint transitions repeatedly within their group, only two
players participating at a time. The group of 2 players get to partial
repetition cuts or one of them takes a joint transition with one player of the
other group, while the group of 3 players might not get to partial repetition
cuts. After two players, one from each group, have taken a joint transition
the problem occurs: the remaining 3 players that did not participate in that
joint transition might form a new group of 3 players that do not reach partial
repetition cuts. This cannot occur in the 4-player case since there is only a
pair of players left.

##  4 Undecidability Result

In this section, a tiling problem is reduced to the synthesis problem of a
6-player Petri game with a global safety condition. The tiling problem used
here is the $\omega$ bipartite colouring problem ($\omega$-BCP). The
undecidable $\omega$ Post correspondence problem ($\omega$-PCP) is reducible
to the $\omega$-BCP. Later, the undecidability result can be simplified to
local safety as a winning condition. The reduction is similar to the work in
[13], where the (normal) Post correspondence problem is reduced to a colouring
problem followed by a reduction to the synthesis problem of 6-process control
games with local termination as a winning condition.

Employing the translation of control games into Petri games in [2], the
6-process control games yield 6-player Petri games (with exponentially many
additional nodes) for local termination as a winning condition. In the
obtained Petri game, all players alternate in their roles as environment and
system players. Instead, we present a direct construction of 6-player Petri
games with at most 3 simultaneous system players. Later, we show that the
number of system players can be even further reduced to 2.

######  Definition 4.1 ($\omega$ bipartite colourings).

Let $\mathit{C}$ be a finite set of colours. An _$\omega$ bipartite colouring_
is a mapping $f:\mathbb{N}^{2}\mapsto\mathit{C}$. The initial colour is
$f(1,1)$. We define three subsets of $\mathit{C}^{2}$ called the patterns
induced by $f$:

  * •

the _diagonal patterns_ of f are all pairs
$\\{(f(x,y),f(x+1,y+1))\mid(x,y)\in\mathbb{N}^{2})\\}$

  * •

the _horizontal patterns_ of f are all pairs
$\\{(f(x,y),f(x+1,y))\mid(x,y)\in\mathbb{N}^{2})\\}$

  * •

the _vertical patterns_ of f are all pairs
$\\{(f(x,y),f(x,y+1))\mid(x,y)\in\mathbb{N}^{2})\\}$

We define a _colouring constraint_ as a 4-tuple
$(\mathit{C}_{i},\mathit{DP},\mathit{HP},\mathit{VP})$, where $\mathit{C}_{i}$
is the set of _initial_ colours, $\mathit{DP}$ a set of diagonal patterns,
$\mathit{VP}$ a set of vertical patterns and $\mathit{HP}$ a set of horizontal
patterns. $\mathit{DP}$, $\mathit{VP}$ and $\mathit{HP}$ are called _forbidden
patterns_. A colouring $f$ _satisfies_ a colouring constraint if its initial
colour is in $\mathit{C}_{i}$ and no diagonal pattern of $f$ is in
$\mathit{DP}$, no vertical pattern of $f$ is in $\mathit{VP}$ and no
horizontal pattern of $f$ is in $\mathit{HP}$.

$\omega$-BCP. Given a finite set of colours $\mathit{C}$ and colouring
constraints $(\mathit{C}_{i},\mathit{DP},$ $\mathit{VP},\mathit{HP})$, decide
whether there exists an $\omega$ bipartite colouring that satisfies the
colouring constraints. This problem is a variation of the standard tiling
problem and it is also undecidable. In the following we define a Petri game
for which a winning strategy exists if and only if a given $\omega$-BCP has a
solution. In this Petri game shown in Fig. 8, there are two identical parts, a
top part and a bottom part, each consisting of 3 players. The idea is that the
number of _rounds_ played in the lower and upper parts refer to the $x$ and
$y$ coordinates of a tile, respectively, so that the system players choose a
colour for each tile. Each colour choice requires one player from each part of
the Petri game, so there can be a maximum of 3 colour choices in one run of
the Petri game. If the colours chosen refer to a forbidden pattern a bad
marking is reached. As the bad markings have to be defined on the Petri net
and not on the unfolding, we define when two system players are in the same
round or when a player is one round ahead or one round behind to be able to
check for forbidden patterns.

$e^{T}_{00}$$e^{T}_{01}$$e^{T}_{02}$$e^{T}_{03}$$e^{T}_{04}$$e^{T}_{05}$$e^{T}_{02}$$e^{T}_{10}$$e^{T}_{11}$$e^{T}_{12}$$e^{T}_{13}$$e^{T}_{14}$$e^{T}_{15}$$e^{T}_{12}$$e^{T}_{20}$$e^{T}_{21}$$e^{T}_{22}$$e^{T}_{23}$$e^{T}_{24}$$e^{T}_{25}$$e^{T}_{22}$$e^{B}_{00}$$e^{B}_{01}$$e^{B}_{02}$$e^{B}_{03}$$e^{B}_{04}$$e^{B}_{05}$$e^{B}_{02}$$e^{B}_{10}$$e^{B}_{11}$$e^{B}_{12}$$e^{B}_{13}$$e^{B}_{14}$$e^{B}_{15}$$e^{B}_{12}$$e^{B}_{20}$$e^{B}_{21}$$e^{B}_{22}$$e^{B}_{23}$$e^{B}_{24}$$e^{B}_{25}$$e^{B}_{22}$$t_{aj-
ak}$$e_{aj-
ak}$$s_{a}$$t_{ac_{1}}$$t_{ac_{m}}$$(c_{1},a)$$(c_{m},a)$$\bullet$$\bullet$$e^{T}_{aj}$$\bullet$$\bullet$$\bullet$$e^{B}_{ak}$$\bullet$$\bullet$$\bullet$$\bullet$Round
1Round 2Round 3$N_{\mathit{CP}}$: Figure 8: Petri net $N_{\mathit{CP}}$ of the
Petri game $G_{\mathit{CP}}$ of an $\omega$-BCP. We have two structurally
identical parts consisting of 3 environment players, a top part and a bottom
part. Two of the players synchronise at each transition in these parts. After
firing 3 such transitions, each player has synchronised with the other two
players in its part. We define such a block of 3 transitions as a _round_.
Each part has 3 rounds. After the third round the players return to the places
they were in before the second round. This means that we have an initial round
and then the players alternate between the second and third rounds. As the
game progresses, the nodes have exact information in the unfolding about how
many rounds they have played. In the middle part, the environment players can
take a _check_ transition $t_{aj-ak}$, where $a\in\\{0,1,2\\}$ and
$j,k\in\\{0,\ldots,5\\}$ and $\mathit{pre}(t_{aj-
ak})=\\{e^{T}_{aj},e^{B}_{ak}\\}$. After that, the system player on place
$s_{a}$ has to choose a colour. Based on the number of rounds $x$ and $y$
played in the lower part and upper part, respectively, the system player has
to determine the colour $f(x,y)$ of the given $\omega$-BCP.

Compared rounds of two players. In the Petri net $N_{\mathit{CP}}$ of Fig. 8,
we compare the rounds of two players $a$ and $b$, both from the same part. We
say $a,b\in\\{0,1,2\\}$ are in the same round if and only if for their places
$e^{X}_{aj}$ and $e^{X}_{bk}$, $X\in\\{T,B\\}$, $j,k\in\\{0,1,2\\}$ or
$j,k\in\\{3,4\\}$ or $j,k\in\\{5,2\\}$ holds. We say that $a$ is one round
ahead of $b$ (or $b$ is one round behind of $a$) if and only if ($j\in\\{3\\}$
and $k\in\\{2\\}$) or ($j\in\\{5\\}$ and $k\in\\{4\\}$) . Other combinations
of indices are not possible.

######  Definition 4.2 (Petri game of an $\omega$ Bipartite colouring
Problem).

Let $\mathit{CP}$ be an $\omega$-BCP with colours $\mathit{C}$ and constraints
$\mathit{C}_{i}$, $\mathit{DP}$, $\mathit{VP}$ and $\mathit{HP}$. The
components of the Petri net of the Petri game $G_{\mathit{CP}}$ are the
components of $N_{\mathit{CP}}$ from Fig. 8. The bad markings of the Petri
game $G_{\mathit{CP}}$ are defined as follows:

$\mathcal{B}=\mathcal{B}_{\mathit{Same}}\cup\mathcal{B}_{\mathit{DP}}\cup\mathcal{B}_{\mathit{HP}}\cup\mathcal{B}_{\mathit{VP}}\cup\mathcal{B}_{\mathit{init}}$,
where
$\mathcal{B}_{\mathit{Same}}=\\{\\{e_{a^{T}j-a^{B}j^{\prime}},e_{b^{T}k-b^{B}k^{\prime}},(c_{u},a),(c_{v},b)\\}\mid\\\
a^{T}\text{ and }b^{T}\text{ are in the same round and }a^{B}\text{ and
}b^{B}\text{ are in same the round },c_{u}\neq c_{v}\\}$,
$\mathcal{B}_{\mathit{\mathit{DP}}}=\\{\\{e_{a^{T}j-a^{B}j^{\prime}},e_{b^{T}k-b^{B}k^{\prime}},(c_{u},a),(c_{v},b)\mid\\\
a^{T}\text{ and }a^{B}\text{ are one round ahead of }b^{T}\text{ and
}b^{B}\text{ respectively },(c_{v},c_{u})\in\mathit{DP}\\}$,
$\mathcal{B}_{\mathit{VP}}=\\{\\{\\{e_{a^{T}j-a^{B}j^{\prime}},e_{b^{T}k-b^{B}k^{\prime}},(c_{u},a),(c_{v},b)\\}\mid\\\
a^{T}\text{ is a round ahead of }b^{T}\text{ and }a^{B}\text{ and }b^{B}\text{
are in the same round },(c_{v},c_{u})\in\mathit{VP}\\}\\}$,
$\mathcal{B}_{\mathit{HP}}=\\{\\{\\{e_{a^{T}j-a^{B}j^{\prime}},e_{b^{T}k-b^{B}k^{\prime}},(c_{u},a),(c_{v},b)\\}\mid\\\
a^{B}\text{ is a round ahead of }b^{B}\text{ and }a^{T}\text{ and }b^{B}\text{
are in the same round },(c_{v},c_{u})\in\mathit{HP}\\}\\}$,
$\mathcal{B}_{\mathit{init}}=\\{\\{e_{a^{T}j-a^{B}j^{\prime}},(c_{u},a)\\}\mid
j,j^{\prime}\in\\{0,1\\},c_{u}\notin\mathit{C}_{i}\\}$.

In addition to the colouring constraints, the bad markings contain the set
$\mathcal{B}_{\mathit{Same}}$ to ensure that system players must choose the
same colour for two checks whenever the checks occur in the same round for
both players. To define a colouring from a strategy of the Petri game, we
define the number of rounds played in the unfolding.

Number of rounds. Let $\textit{unf}(G_{\mathit{CP}})$ be the unfolding of
$G_{\mathit{CP}}$ of Fig. 8. The _number of rounds_ played in part $X$,
$X\in\\{T,B\\}$ in a place $p\in\mathcal{P}_{\textit{unf}(G_{\mathit{CP}})}$
is defined as
$r^{X}(p)=\mathit{max}(\lceil|\\{t\in\mathcal{T}_{\textit{unf}_{\mathit{CP}}}\mid
t\leq p\text{ and }t\text{ is a transition in part }X\\}|/3\rceil,1)$

This means that the number of rounds is incremented after a player has taken
two transitions, starting from round 1. The divisor is 3 because the players
also get the knowledge of the synchronisation of the other two players in
their part. The number of rounds is not increased after a check transition.

######  Theorem 4.1 (Characterization of $\omega$-BCP as a Petri game).

The $\omega$-BCP is reducible to the synthesis Problem of 6-player Petri
games.

###### Proof.

Let $\mathit{CP}$ be a colouring problem and $G_{\mathit{CP}}$ be the Petri
game from Def. 4.2. We show that there exists a solution for $\mathit{CP}$ if
and only if there exists a winning strategy for $G_{\mathit{CP}}$.

We start by assuming that there is a solution
$f:\mathbb{N}\times\mathbb{N}\mapsto\mathit{C}$ for the colouring problem
$\mathit{CP}$. After the environment player has chosen a check transition the
system player must choose a colour in place $s_{a}$, $a\in\\{0,1,2\\}$. Since
the system player knows the entire causal history, she knows the number of
rounds played in the top and the bottom part of the Petri game. Let
$r^{T}(s_{a})=y$ denote the number of rounds in the top part and
$r^{B}(s_{a})=x$ the number of rounds in the bottom part. Then, the winning
strategy for the system players is to choose the colour $f(x,y)$. This way no
bad marking is reachable. The bad markings in $\mathcal{B}_{\mathit{Same}}$
are avoided because $f(x,y)$ is unique. The bad markings in
$\mathcal{B}_{\mathit{DP}},\mathcal{B}_{\mathit{VP}}$ and
$\mathcal{B}_{\mathit{HP}}$ are avoided because $f$ avoids all forbidden
patterns. Finally, the bad markings $\mathcal{B}_{\mathit{init}}$ are avoided
because $f(1,1)$ is an initial colour.

Now, we assume that there is a winning strategy for the Petri game
$G_{\mathit{CP}}$. We define the colouring
$f:\mathbb{N}\times\mathbb{N}\mapsto C$ derived from the winning strategy as
follows: $f(x,y)=c$ if there exists a system place
$s_{a}\in\mathcal{P}_{\textit{unf}(N_{\mathit{CP}})}$ with $r^{B}(s_{a})=x$
and $r^{T}(s_{a})=y$ and $t_{ac}\in\mathit{post}(s_{a})$.

We show that for every colour that a system player has to choose, there are
sequences of checks such that all colouring constraints are met. In these
sequences of checks, any two consecutive checks can be carried out
concurrently while the system players do not know whether the other check is
the previous check or the next check, so the winning strategy must play
correctly for both checks. Informally speaking, this leads to infinite
sequences of dependencies as a check depends on the choice of the colour of
the previous check and again that check depends on its previous check and so
on.

| $e^{X}_{00}$ | $e^{X}_{10}$ | $e^{X}_{20}$ | $e^{X}_{01}$ | $e^{X}_{11}$ | $e^{X}_{21}$ | $e^{X}_{02}$ | $e^{X}_{12}$ | $e^{X}_{22}$ | $e^{X}_{03}$ | $e^{X}_{13}$ | $e^{X}_{23}$ | $e^{X}_{04}$ | $e^{X}_{14}$ | $e^{X}_{24}$
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---
$e^{X}_{00}$ |  | $||$ | $||$ |  |  |  |  |  |  |  |  |  |  |  |
$e^{X}_{10}$ | $||$ |  | $||$ |  |  |  |  |  |  |  |  |  |  |  |
$e^{X}_{20}$ | $||$ | $||$ |  | $||$ | $||$ |  |  |  |  |  |  |  |  |  |
$e^{X}_{01}$ |  |  | $||$ |  | $||$ | $||$ |  | $||$ |  |  |  |  |  |  |
$e^{X}_{11}$ |  |  | $||$ | $||$ |  |  |  |  |  |  |  |  |  |  |
$e^{X}_{21}$ |  |  |  | $||$ |  |  |  | $||$ |  |  |  |  |  |  |
$e^{X}_{02}$ |  |  |  |  |  |  |  | $||$ | $||$ |  |  |  |  |  |
$e^{X}_{12}$ |  |  |  | $||$ |  | $||$ | $||$ |  | $||$ |  |  |  |  |  |
$e^{X}_{22}$ |  |  |  |  |  |  | $||$ | $||$ |  | $||$ | $||$ |  |  |  |
$e^{X}_{03}$ |  |  |  |  |  |  |  |  | $||$ |  | $||$ | $||$ |  | $||$ |
$e^{X}_{13}$ |  |  |  |  |  |  |  |  | $||$ | $||$ |  |  |  |  |
$e^{X}_{23}$ |  |  |  |  |  |  |  |  |  | $||$ |  |  |  | $||$ |
$e^{X}_{04}$ |  |  |  |  |  |  |  |  |  |  |  |  |  | $||$ | $||$
$e^{X}_{14}$ |  |  |  |  |  |  |  |  |  | $||$ |  | $||$ | $||$ |  |
$e^{X}_{24}$ |  |  |  |  |  |  |  |  |  |  |  |  | $||$ | $||$ |

Figure 9: Table of concurrent places of the first two rounds in the unfolding
of the Petri game $G_{\mathit{CP}}$. Empty cells denote that the places are
causally related. Filled cells denote that the places are concurrent. The
pattern continues identically. With the help of this table we can see the
sequences of checks to ensure that no bad markings are reached in the Petri
game. For example, to check that the initial colour chosen after the
transition $t_{00-00}$ and after $t_{22-00}$ is the same, we can perform the
following sequence of checks of the indices of the places in the upper part:
$00-20-01-12-22$. The indices of the place in the lower part remain $00$ here.
To carry out two consecutive checks in the same play they need to be
concurrent. We can check this in the table by going in a row from $00$ to
$20$, then in the column from $20$ to $01$, then again checking in the row and
so on. Note that the place of the bottom player can also change in these
sequences.

In Fig. 9, it is crucial to see that there are concurrent places between
different rounds such that we can always find at least one suitable check for
all diagonal, vertical and horizontal patterns. To check the horizontal
pattern of $(f(1,1),f(2,1))$ for example, the checks $t_{00-03}$ and
$t_{20-22}$ are fired. The places in the upper part are $e^{T}_{00}$ and
$e^{T}_{20}$ respectively, which are both in the first round. The places in
the lower part are $e^{B}_{03}$ and $e^{B}_{22}$ respectively, where
$e^{B}_{03}$ is in the second round and $e^{B}_{22}$ in the first round. These
two checks can be performed concurrently since $e^{T}_{00}$ and $e^{T}_{20}$
are concurrent, as are $e^{B}_{22}$ and $e^{B}_{03}$. For the initial colour
we have the extra initial round which does not get repeated.

The colouring $f$ is well-defined as the set of bad markings
$\mathcal{B}_{\mathit{Same}}$ ensures that every two colours chosen when both
top rounds and both bottom rounds are the same the colours chosen also must be
the same in a winning strategy. This can be seen with the help of Fig. 9, too.
There, we can find a sequence of checks throughout one round such that the
colour chosen at the beginning of that round (e.g. $e^{B}_{03}$) is still the
same colour as chosen at the end of that round (e.g $e^{B}_{04}$) (assuming
that the top round does not change too). ∎

It is easy to see that the Petri game presented here performs at most 3 checks
in every possible sequence of transitions. Therefore this Petri game has at
most 3 system players. For the undecidability result it is sufficient to have
2 concurrent checks. Therefore, the number of system players can be further
reduced to 2 by adapting the Petri game. This could be done by adding two
environment players that are consumed performing a check. Furthermore, by
adding a transition for each bad marking to a bad place, the set of bad
markings can be simplified to a set of bad places, the local safety condition.

##  5 Conclusions

Our contribution to the synthesis problem of distributed systems is that this
problem is undecidable for 6-player Petri games under a local safety condition
and that two system processes are sufficient to obtain undecidability. This
adds neatly to the result in [8], where Petri games with one system player are
solved in exponential time. Furthermore, the synthesis problem for 2-player
Petri games belongs to the class of NP-complete problems, and we provide a
non-deterministic exponential upper bound for this problem for Petri games
with a variable number of players up to 4 under a global safety condition.
This is a new class of Petri games for which the synthesis problem is
decidable. The case of 5 players remains open.

## References

  * [1]
  * [2] Raven Beutner, Bernd Finkbeiner & Jesko Hecking-Harbusch (2019): _Translating Asynchronous Games for Distributed Synthesis_.  In Wan J. Fokkink & Rob van Glabbeek, editors: 30th International Conference on Concurrency Theory, CONCUR 2019, LIPIcs 140, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 26:1–26:16, 10.4230/LIPIcs.CONCUR.2019.26.
  * [3] Roderick Bloem, Sven Schewe & Ayrat Khalimov (2017): _CTL* synthesis via LTL synthesis_.  In Dana Fisman & Swen Jacobs, editors: Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, EPTCS 260, pp. 4–22, 10.4204/EPTCS.260.4.
  * [4] Alonzo Church (1957): _Applications of recursive arithmetic to the problem of circuit synthesis_.  Summaries of the Summer Institute of Symbolic Logic 1, pp. 3–50.
  * [5] Joost Engelfriet (1991): _Branching Processes of Petri Nets_.  Acta Inf. 28(6), pp. 575–591, 10.1007/BF01463946.
  * [6] Javier Esparza, Stefan Römer & Walter Vogler (2002): _An Improvement of McMillan’s Unfolding Algorithm_.  Formal Methods Syst. Des. 20(3), pp. 285–310, 10.1023/A:1014746130920.
  * [7] Bernd Finkbeiner (2015): _Bounded Synthesis for Petri Games_.  In Roland Meyer, André Platzer & Heike Wehrheim, editors: Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Proceedings, Lecture Notes in Computer Science 9360, Springer, pp. 223–237, 10.1007/978-3-319-23506-6_15.
  * [8] Bernd Finkbeiner & Paul Gölz (2018): _Synthesis in Distributed Environments_.  In Satya Lokam & R. Ramanujam, editors: 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017), Leibniz International Proceedings in Informatics (LIPIcs) 93, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, pp. 28:1–28:14, 10.4230/LIPIcs.FSTTCS.2017.28.
  * [9] Bernd Finkbeiner & Ernst-Rüdiger Olderog (2017): _Petri games: Synthesis of distributed systems with causal memory_.  Information and Computation 253, pp. 181–203, 10.1016/j.ic.2016.07.006.  GandALF 2014.
  * [10] Bernd Finkbeiner & Sven Schewe (2005): _Uniform Distributed Synthesis_.  In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), Proceedings, pp. 321–330, 10.1109/LICS.2005.53.
  * [11] Blaise Genest, Hugo Gimbert, Anca Muscholl & Igor Walukiewicz (2013): _Asynchronous Games over Tree Architectures_.  In Fedor V. Fomin, Rusins Freivalds, Marta Z. Kwiatkowska & David Peleg, editors: Automata, Languages, and Programming - 40th International Colloquium, ICALP 2013, Proceedings, Part II, Lecture Notes in Computer Science 7966, Springer, pp. 275–286, 10.1007/978-3-642-39212-2_26.
  * [12] Hugo Gimbert (2017): _On the Control of Asynchronous Automata_.  In Satya V. Lokam & R. Ramanujam, editors: 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, India, LIPIcs 93, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 30:1–30:15, 10.4230/LIPIcs.FSTTCS.2017.30.
  * [13] Hugo Gimbert (2022): _Distributed Asynchronous Games With Causal Memory are Undecidable_.  Log. Methods Comput. Sci. 18(3), 10.46298/lmcs-18(3:30)2022.
  * [14] Paul Hannibal & Ernst-Rüdiger Olderog (2022): _The Synthesis Problem for Repeatedly Communicating Petri Games_.  In Luca Bernardinello & Laure Petrucci, editors: Application and Theory of Petri Nets and Concurrency - 43rd International Conference, PETRI NETS 2022, Proceedings, Lecture Notes in Computer Science 13288, Springer, pp. 236–257, 10.1007/978-3-031-06653-5_13.
  * [15] O. Kupferman & M.Y. Vardi (2001): _Synthesizing distributed systems_.  Proceedings - Symposium on Logic in Computer Science, pp. 389–398, 10.1109/LICS.2001.932514.
  * [16] P. Madhusudan & P. S. Thiagarajan (2002): _A Decidable Class of Asynchronous Distributed Controllers_.  In Lubos Brim, Petr Jancar, Mojmír Kretínský & Antonín Kucera, editors: CONCUR 2002 - Concurrency Theory, 13th International Conference, Proceedings, Lecture Notes in Computer Science 2421, Springer, pp. 145–160, 10.1007/3-540-45694-5_11.
  * [17] P. Madhusudan, P. S. Thiagarajan & Shaofa Yang (2005): _The MSO Theory of Connectedly Communicating Processes_.  In Ramaswamy Ramanujam & Sandeep Sen, editors: FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference, Proceedings, Lecture Notes in Computer Science 3821, Springer, pp. 201–212, 10.1007/11590156_16.
  * [18] Anca Muscholl (2015): _Automated Synthesis of Distributed Controllers_.  In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi & Bettina Speckmann, editors: Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Proceedings, Part II, Lecture Notes in Computer Science 9135, Springer, pp. 11–27, 10.1007/978-3-662-47666-6_2.
  * [19] Amir Pnueli & Roni Rosner (1989): _On the Synthesis of an Asynchronous Reactive Module_.  In Giorgio Ausiello, Mariangiola Dezani-Ciancaglini & Simona Ronchi Della Rocca, editors: Automata, Languages and Programming, 16th International Colloquium, ICALP89, Proceedings, Lecture Notes in Computer Science 372, Springer, pp. 652–671, 10.1007/BFb0035790.
  * [20] Amir Pnueli & Roni Rosner (1990): _Distributed Reactive Systems Are Hard to Synthesize_.  In: 31st Annual Symposium on Foundations of Computer Science, Volume II, pp. 746–757, 10.1109/FSCS.1990.89597.
  * [21] R. Rosner (1992): _Modular synthesis of reactive systems_.  Ph.D. thesis, Weizmann Institute of Science, Rehovot, Israel.