# First order synthesis for data words revisited

Julien Grange111Univ Paris Est Creteil, LACL, F-94010 Creteil, France Mathieu
Lehaut222University of Gothenburg, Sweden

###### Abstract

We carry on the study of the synthesis problem on data words for fragments of
first order logic, and delineate precisely the border between decidability and
undecidability.

##  1 Introduction

The reactive synthesis problem, which dates back to Church [4], is about
generating a _correct-by-construction_ program with respect to a given
specification. It is often formulated as a two-player game between an
uncontrollable Environment and the System, who alternate picking an input and
an output letter, respectively. This creates an infinite execution, and the
goal of the System is to make every execution satisfy the specification,
whatever Environment does. If the System has a strategy to ensure this result,
it then corresponds to a program that is sure to respect the specification.
The original problem is decidable and was solved by Büchi and Landweber [3],
and several improvements and extensions have since been studied. However, it
only encompasses finite alphabets, which is inadequate for representing
executions of distributed systems involving a number of processes which is not
fixed; this occurs in communication protocols, distributed algorithms, multi-
agent systems, swarm robotics, or with ad-hoc networks.

We thus consider an extension of this problem which deals with alphabets whose
size is not fixed. In those cases it is more adequate to use data words to
represent executions, where a data word consists of a sequence of pairs
(action, data), the action coming from a finite alphabet while the data, which
comes from an infinite alphabet (or at least, an alphabet whose size is not
fixed), specifies who performed said action.

We will assume that the sets of actions of both players are disjoint, but this
does not necessarily need to be the case for the processes. We will consider
two distinct cases, depending on process ownership. In the first case, all
processes are shared, meaning that both players can perform their respective
actions on any process. Consider for instance the modelling of a drone fleet,
where a process corresponds to a single drone, inputs correspond to
atmospheric conditions and outputs to possible movements of the drone. In that
case, it makes sense to have both System and Environment play their actions on
shared processes. In the second case, each player has their own processes, on
which only they can play an action. This is for instance useful for modelling
a single machine with several components, where each component is considered
to be its own process, some being sensors/receptors (belonging to Environment)
while other parts (System’s processes) perform the machine’s output.

Finally, it remains to chose a formalism to express the specification which
should be satisified by System. As always, there is a trade off between
expressiveness of the formalism and tractability of its synthesis problem.
Many specification languages for data words have been studied, and the
synthesis problem has been investigated for some of them, such as register
automata [6] and the Logic of Repeating Values [5]. Here we follow the steps
of [1] and consider first order logic FO and its fragment $\textsc{FO}^{2}$
where only two reusable variables are allowed. First order logic for words is
well understood, and its extension to data words is easy to define, which
makes it a good candidate for our purpose. On data words, FO has acess to a
binary predicate $\sim$ such that $x\sim y$ if positions $x$ and $y$ belong to
the same process. On top of that, a unary predicate for each action marks the
positions where this action has been played (as is usually the case for
words), and we will study variations where relative positions will either be
accessible via a binary predicate $<$, its successor relation $+1$, both or
none of them.

The satisfiability problem, which can be seen as a very restricted synthesis
problem in the case where Environment never acts, has been showed to be
decidable in the two-variable fragment with $<$ and $+1$
($\textsc{FO}^{2}[\sim,<,+1]$) [2]. The synthesis problem itself has
previously been studied in [1] for various of fragments of FO, with both
decidable and undecidable results, depending on the variety of the considered
fragment. The aim of this paper is to extend those results and get a better
understanding on where the border between decidability and undecidability lies
exactly.

##  2 Preliminaries

#### Data words.

Let $A$ be a finite alphabet of _actions_ , partitioned into System actions
$A_{\mathrm{S}}$ and Environment actions $A_{\mathrm{E}}$. Let
$\mathbb{P}_{\mathrm{S}}$ (resp. $\mathbb{P}_{\mathrm{E}}$) be a finite set of
_processes_ belonging to System (resp. Environment), and let
$\mathbb{P}_{\mathrm{S}\mathrm{E}}$ be a finite set of processes which can be
activated by both players. These sets are assumed to be pairwise disjoint, and
we define
$\mathbb{P}:=\mathbb{P}_{\mathrm{S}}\cup\mathbb{P}_{\mathrm{E}}\cup\mathbb{P}_{\mathrm{S}\mathrm{E}}$.
Let us refer to
$A_{\mathrm{S}}\times(\mathbb{P}_{\mathrm{S}}\cup\mathbb{P}_{\mathrm{S}\mathrm{E}})$
as $\Sigma_{S}$ and to
$A_{\mathrm{E}}\times(\mathbb{P}_{\mathrm{E}}\cup\mathbb{P}_{\mathrm{S}\mathrm{E}})$
as $\Sigma_{E}$. A _data word_ is a finite or infinite sequence
$w=(a_{0},p_{0})(a_{1},p_{1})\dots$ over $\Sigma:=\Sigma_{S}\cup\Sigma_{E}$.

Intuitively, a data word represents the trace of an execution of a distributed
system. Each pair $(a,p)$ (called a _position_) indicates that action $a$ has
been performed by process $p$. Note that the above definition prevents a
player from playing on processes owned by their opponent.

#### First order logic.

Let $A$ be a finite alphabet of actions and $V$ be a set of variable names. We
define formulas of first order logic with $<$ and $+1$ on data words
($\textsc{FO}[\sim,<,+1]$) as follows:

$\displaystyle t:=~{}$ $\displaystyle a(x)\mid x=y\mid x<y\mid x=y+1\mid x\sim
y\mid\mathbb{P}_{\mathrm{S}}(x)\mid\mathbb{P}_{\mathrm{E}}(x)\mid\mathbb{P}_{\mathrm{S}\mathrm{E}}(x)$
$\displaystyle\varphi:=~{}$ $\displaystyle
t\mid\neg\varphi\mid\varphi\land\varphi\mid\varphi\lor\varphi\mid\exists
x.\varphi\mid\forall x.\varphi$

where $a\in A$ and $x,y\in V$.

A data word $w=(a_{0},p_{0})(a_{1},p_{1})\dots$ is represented as a structure
whose domain has an element for each position $(a_{i},p_{i})$, and an element
for each process in $\mathbb{P}_{\mathrm{S}}$ (resp.
$\mathbb{P}_{\mathrm{E}}$, resp. $\mathbb{P}_{\mathrm{S}\mathrm{E}}$), which
is in the interpretation of the unary predicate $\mathbb{P}_{\mathrm{S}}$
(resp. $\mathbb{P}_{\mathrm{E}}$, resp. $\mathbb{P}_{\mathrm{S}\mathrm{E}}$).
Note that this allows to quantify on processes on which no action has been
played. For every action $a\in A$, the unary predicate $a$ is interpreted as
the set of positions with action $a$. The binary predicate $<$ is interpreted
as the linear order on positions and $+1$ as its successor relation. Finally,
$(a_{i},p_{i})\sim(a_{j},p_{j})$ holds if and only if $p_{i}=p_{j}$; on top of
that, $\sim$ also relates each process $p$ to all positions $(a,p)$. Beyond
that, we consider the usual semantics for first order logic, e.g. see [7].

We then define various fragments of $\textsc{FO}[\sim,<,+1]$ depending on
which binary predicates are allowed, and how many variables are available.
$\textsc{FO}[\sim,<,+1]$ is the whole fragment with $\sim$, $<$, and $+1$,
while $\textsc{FO}[\sim]$ only allows $\sim$ out of the three predicates.
Furthermore, we also study the two-variable restriction of FO, in which one
can only use two (reusable) variables in the whole formula, i.e.
$V=\\{x,y\\}$. We denote this variation by $\textsc{FO}^{2}$, and combine it
with the previous notations; for instance $\textsc{FO}^{2}[\sim,<]$ is the
two-variable fragment with predicates $\sim$ and $<$, but without $+1$. Note
that unless restricted to two variables, first order logic can define $+1$
using $<$, but not the other way around.

#### Synthesis.

Let us now define the synthesis problem. A data word is seen as an execution,
or history, in a game opposing System and Environment. A _strategy_
$\mathcal{S}$ for System is a function
$\Sigma^{\ast}\to\Sigma_{S}\cup\\{\varepsilon\\}$ which, given some finite
data word representing the history of the game, either outputs some move in
$\Sigma_{S}$ (i.e. plays an action on some process which can be activated by
System) or passes its turn. An execution $w=\sigma_{0}\sigma_{1}\dots$ is said
to be $\mathcal{S}$-compatible if

  * •

for all $0\leq i<|w|$, $\sigma_{i}\in\Sigma_{S}$ implies
$\sigma_{i}=\mathcal{S}(\sigma_{0}\dots\sigma_{i-1})$, and

  * •

if $w$ is finite, then $\mathcal{S}(w)=\varepsilon$.

With this definition we intuitively allow Environment to block System from
playing anytime Environments wants to play, which could potentially be
forever. To prevent pathological cases, we will consider only _fair_
executions for $\mathcal{S}$, i.e. executions $w=\sigma_{0}\sigma_{1}\dots$
such that if there are infinitely many $i$ such that
$\mathcal{S}(\sigma_{0}\dots\sigma_{i-1})\neq\varepsilon$, then there are
infinitely many positions in $\Sigma_{S}$. In other words, Environment can
delay actions from System, but cannot silence them forever. Finally, for a
given formula $\varphi$, we say that $\mathcal{S}$ is _winning_ for $\varphi$
if all executions which are $\mathcal{S}$-compatible and fair for
$\mathcal{S}$ satisfy $\varphi$.

In this paper we focus on two specific configurations for processes: when they
are shared, and when they are partitioned between players.

#### Shared.

We say that the processes are _shared_ when
$\mathbb{P}_{\mathrm{S}}=\mathbb{P}_{\mathrm{E}}=\emptyset$, i.e. when all
processes can be affected both by System and Environment. The synthesis
problem for logic $\mathcal{L}$ with shared processes is denoted
$\textsc{SharedSynth}(\mathcal{L})$: it amounts, given an alphabet $A$ of
actions and a formula $\varphi\in\mathcal{L}$, to decide whether there exists
a winning strategy $\mathcal{S}$ for $\varphi$ with
$\mathbb{P}_{\mathrm{S}}=\mathbb{P}_{\mathrm{E}}=\emptyset$ and some (finite)
$\mathbb{P}_{\mathrm{S}\mathrm{E}}$. Since the identity of the shared
processes does not matter and only the cardinality of
$\mathbb{P}_{\mathrm{S}\mathrm{E}}$ is relevant, we say in that case that
$\mathcal{S}$ is a $|\mathbb{P}_{\mathrm{S}\mathrm{E}}|$-winning strategy for
$\varphi$.

#### Partitioned.

We say that the processes are _partitioned_ if
$\mathbb{P}_{\mathrm{S}\mathrm{E}}=\emptyset$. In that case, each player has
their own pool of processes on which they can play, but that their opponent
cannot use. The synthesis problem for logic $\mathcal{L}$ with partitioned
processes is denoted $\textsc{PartSynth}(\mathcal{L})$. As above, it is the
problem of deciding, given $A$ and $\varphi\in\mathcal{L}$, whether System has
a winning strategy for $\varphi$ with
$\mathbb{P}_{\mathrm{S}\mathrm{E}}=\emptyset$ and some arbitrary finite sets
$\mathbb{P}_{\mathrm{S}}$ and $\mathbb{P}_{\mathrm{E}}$. Similarly, we say in
that case that $\mathcal{S}$ is a
$(|\mathbb{P}_{\mathrm{S}}|,|\mathbb{P}_{\mathrm{E}}|)$-winning strategy for
$\varphi$.

#### Known results.

Data words were introduced in [2]. Bojańczyk et al. proved that the
satisfiability problem for $\textsc{FO}^{2}[\sim,<,+1]$ on data words is
decidable. Note that this corresponds to the synthesis problem for
$\textsc{FO}^{2}[\sim,<,+1]$ when both $\mathbb{P}_{\mathrm{E}}$ and
$\mathbb{P}_{\mathrm{S}\mathrm{E}}$ are empty. They also showed that as soon
as a third variable is available, this problem becomes undecidable, even
without the order (i.e. for $\textsc{FO}^{3}[\sim,+1]$).

Decidability of the satisfiability problem for the two-variable logic in this
setting is what prompted Bérard et al. to consider the synthesis problem on
data words, for serveral fragments of first order logic [1]. They proved that
the synthesis problem for $\textsc{FO}[\sim]$ is decidable when processes are
partitioned and when the number of Environment processes is fixed. In
constrast, they established undecidability results for $\textsc{FO}[\sim]$ and
$\textsc{FO}^{2}[\sim,<,+1]$ when processes are shared.

#### Contributions.

We summarize the contributions of this paper in Table 1, in bold font. Results
from [1] are also mentioned. As can be seen, we bridge all the gaps left open
by [1].

Logic $\backslash$ Processes | Partitioned | Shared
---|---|---
$\textsc{FO}^{2}[\sim]$ |  decidable (Th 2) |  undecidable (Th 5)
$\textsc{FO}[\sim]$ |  decidable (Th 2) | undecidable [1]
$\textsc{FO}^{2}[\sim,<]$ |  undecidable (Th 3) |  undecidable (Th 5)
$\textsc{FO}^{2}[\sim,+1]$ |  undecidable (Th 4) |  undecidable (Th 5)
$\textsc{FO}^{2}[\sim,<,+1]$ |  undecidable (Th 3 or 4) | undecidable [1]
Table 1: Decidability and undecidability of the synthesis problem for
fragments of first order logic, in the pure and mixed cases. New results from
this paper appear in bold.

##  3 $\textsc{FO}[\sim]$ with processes partitioned between players

First, we turn to the case where processes are partitioned between System and
Environment. It has been shown in [1] that in that case, the synthesis problem
for $\textsc{FO}[\sim]$ is decidable when System has an arbitrary number of
processes, but Environment only has access to a fixed number of processes. We
extend this result by lifting this restriction: we show in Theorem 2 that
$\textsc{PartSynth}(\textsc{FO}[\sim])$ is decidable.

As a first step towards proving this result, let us show that beyond a certain
threshold (which depends only on the formula), having access to more processes
in $\mathbb{P}_{\mathrm{E}}$ is always a boon for the Environment. Note that
this is note true for small cardinalities of $\mathbb{P}_{\mathrm{E}}$: it is
not hard to design a game where Environment wins if
$\mathbb{P}_{\mathrm{E}}=\emptyset$ but loses as soon as
$|\mathbb{P}_{\mathrm{E}}|\geq 1$.

######  Lemma 1.

For every alphabet $A$ and every $\varphi\in\textsc{FO}[\sim]$, there exists
$n^{\text{min}}_{\text{E}}\in\mathbb{N}$ such that for every
$n_{S}\in\mathbb{N}$ and every $n_{E}\geq n^{\text{min}}_{\text{E}}$, if
System has a $(n_{S},n_{E}+1)$-winning strategy for $\varphi$, then System has
an $(n_{S},n_{E})$-winning strategy for $\varphi$.

###### Proof.

For this proof, we rely on a characterisation of the synthesis problem for
$\textsc{FO}[\sim]$ via parametrised vector games, defined in [1]. The
_parametrised vector game_ on alphabet $A=A_{\mathrm{S}}\uplus A_{\mathrm{E}}$
with bound $B\in\mathbb{N}$, victory condition $\mathcal{F}$ and
($n_{S}$,$n_{E}$) pebbles is a game between two players, System and
Environment, defined as follows. An _S-location_ (resp. E-location) is a
vector $\ll\\!a_{1}^{\nu_{1}}\cdots a_{d}^{\nu_{d}}\\!\gg$, where
$a_{1},\cdots,a_{d}$ are the letters from $A_{\mathrm{S}}$ (resp.
$A_{\mathrm{E}}$), and $0\leq\nu_{i}\leq B$. An S-location (resp. E-location)
$\ll\\!a_{1}^{\mu_{1}}\cdots a_{d}^{\mu_{d}}\\!\gg$ is reachable from the
S-location (resp. E-location) $\ll\\!a_{1}^{\nu_{1}}\cdots
a_{d}^{\nu_{d}}\\!\gg$ if $\mu_{i}\geq\nu_{i}$ for every $i$. The initial
S-location (resp. E-location) is the one for which all $\nu_{i}$ are zero.
System (resp. Environment) has a number $n_{S}$ (resp. $n_{E}$) of pebbles,
which are private to each player. The identity of the pebbles is irrelevant;
only their number in each location matters. An S-configuration $C_{\text{S}}$
(resp. an E-configuration $C_{\text{E}}$) is just a way for System (resp.
Environment) to distribute their pebbles on their locations; namely, it is a
function which maps every S-location (resp. E-location) $l$ to
$C_{\text{S}}(l)\in\\{0,\cdots,n_{S}\\}$ (resp.
($C_{\text{E}}(l)\in\\{0,\cdots,n_{E}\\}$) whose sum over the locations is
$n_{S}$ (resp. $n_{E}$). An S-configuration (and similarly for
E-configurations) $\widehat{}C_{\text{S}}$ is reachable from $C_{\text{S}}$ if
it is possible to obtain $\widehat{}C_{\text{S}}$ from $C_{\text{S}}$ by
moving a number of pebbles from locations $l$ to locations that are reachable
from $l$.

A _location_ is a couple composed of an S- and an E-locations, and the initial
location $l_{0}$ is the couple of initial S- and E-locations. A
_configuration_ $C=(C_{\text{S}},C_{\text{E}})$ is a couple composed of an S-
and an E-configuration. In the initial configuration, the pebbles of both
players are placed on their respective initial locations. An _acceptance
condition_ $c$ is a mapping from the set of S- and E-locations to the set of
conditions $\\{``=n",``\geq n":n\in\mathbb{N}\\}$, and a configuration
$(C_{\text{S}},C_{\text{E}})$ satisfies this acceptance condition if for every
S- or E-location $l$, $C_{\text{S}}(l)$ or $C_{\text{E}}(l)$ satisfies $c(l)$.
The winning condition $\mathcal{F}$ is a finite set of acceptance conditions,
and a configuration is said to be _winning for System_ if it satisfies at
least one acceptance condition in $\mathcal{F}$; otherwise, it _winning for
Environment_.

A strategy for System (resp. Environment) is a function mapping a
configuration $(C_{\text{S}},C_{\text{E}})$ to a configuration
$(\widehat{}C_{\text{S}},C_{\text{E}})$ where $\widehat{}C_{\text{S}}$ is
reachable from $C_{\text{S}}$ (resp. to a configuration
$(C_{\text{S}},\widehat{}C_{\text{E}})$ where $\widehat{}C_{\text{E}}$ is
reachable from $C_{\text{E}}$). A strategy for System (resp. Environment) is
said to be _winning_ if for every strategy for Environment (resp. System), the
result of letting both strategies alternate moves against each other, starting
with Environment (which can easily be seen to lead to a well-defined final
configuration) is winning for System (resp. for Environment). Parametrised
vector games are determined.

Parametrised vector games are shown in [1] (Lemma 11) to be equivalent to the
synthesis problem for $\textsc{FO}[\sim]$: for every formula
$\varphi\in\textsc{FO}[\sim]$, there exists a parametrised vector game
$\mathfrak{G}_{\varphi}$ such that for every $n_{S},n_{E}\in\mathbb{N}$,
System has an $(n_{S},n_{E})$-winning strategy for $\varphi$ if and only if
System wins $\mathfrak{G}_{\varphi}$ with $(n_{S},n_{E})$ pebbles.

Thus, to prove the lemma, we show that if Environment has a winning strategy
in the parametrised vector game $\mathfrak{G}_{\varphi}$ with $(n_{S},n_{E})$
pebbles, Environment has a winning strategy in $\mathfrak{G}_{\varphi}$ with
$(n_{S},n_{E}+1)$ pebbles, for every $n_{E}\geq n^{\text{min}}_{\text{E}}$.
Let $A_{\mathrm{E}}=\\{a_{1},\cdots,a_{d}\\}$, $B$ be the bound of
$\mathfrak{G}_{\varphi}$, and let $K$ be the largest constant that occurs in
$\mathcal{F}$. We claim that $n^{\text{min}}_{\text{E}}:=K\cdot(d+1)^{d\cdot
B}$ fits the bill.

Given an E-location $l:=\ll\\!a_{1}^{\nu_{1}}\cdots a_{d}^{\nu_{d}}\\!\gg$,
let us denote by $E^{*}(l)$ the set of E-locations that can be reached from
$l$, i.e. locations $\ll\\!a_{1}^{\mu_{1}}\cdots a_{d}^{\mu_{d}}\\!\gg$ for
$\mu_{i}\geq\nu_{i}$, and by $C_{\text{E}}^{*}(l)$ the number of Environment
pebbles in locations of $E^{*}(l)$, i.e.

$C_{\text{E}}^{*}(l):=\sum_{l^{\prime}\in
E^{*}(l)}C_{\text{E}}(l^{\prime})\,.$

Let $E^{+1}(l)$ be the subset of successors of $l$ in $E^{*}(l)$, i.e.
locations $\ll\\!a_{1}^{\mu_{1}}\cdots a_{d}^{\mu_{d}}\\!\gg$ where
$\mu_{i}=\nu_{i}$ except for one $i$, for which $\mu_{i}=\nu_{i}+1$.

We define the potential $\rho(l)$ of some E-location $l=\ll
a_{1}^{\nu_{1}}\cdots a_{d}^{\nu_{d}}\gg$ as follows:
$\rho(l):=\sum_{i=1}^{d}(B-\nu_{i})$. In other words, $\rho(l)$ is the number
of times an Environment pebble in $l$ can be moved. Note that the potention of
the initial E-location is $d\cdot B$.

Consider some E-configuration $C_{\text{E}}$, and let $P(l)$ denote the
property

$C_{\text{E}}^{*}(l)\geq K\cdot(d+1)^{\rho(l)}\,.$ ($P(l)$)

If $P(l)$, then either $C_{\text{E}}(l)\geq K$ or there exists $l^{\prime}\in
E^{+1}(l)$ such that $P(l^{\prime})$. Indeed, note that

$E^{*}(l)=\\{l\\}\cup\bigcup_{l^{\prime}\in E^{+1}(l)}E^{*}(l^{\prime})\,.$

If $\rho(l)=0$, there is nothing to prove. Otherwise, suppose that
$C_{\text{E}}(l)<K$ and $P(l^{\prime})$ fails for every $l^{\prime}\in
E^{+1}(l)$. Then we would have

$C_{\text{E}}^{*}(l)\leq C_{\text{E}}(l)+\sum_{l^{\prime}\in
E^{+1}(l)}C_{\text{E}}^{*}(l^{\prime})<K+d\cdot K(d+1)^{\rho(l)-1}\leq
K(d+1)^{\rho(l)}\,,$

contradicting $P(l)$.

With this in mind, a simple induction on $\rho(l)$ establishes the following:
if $P(l)$ holds for some $l$, there there exists some $l^{\prime}\in E^{*}(l)$
such that $P(l^{\prime})$ and $C_{\text{E}}(l)\geq K$.

We are now ready to describe the winning strategy for Environment in
$\mathfrak{G}_{\varphi}$ with $(n_{S},n_{E}+1)$ pebbles, based on their
winning strategy with $(n_{S},n_{E})$ pebbles: at all time, Environment keeps
a marked E-location $\hat{}l$ where they place their additional pebble.

We argue that it is at all time possible to choose an $\hat{}l$ which is such
that $P(\hat{}l)$ and $C_{\text{E}}(\hat{}l)\geq K$ in the configuration of
the game with $(n_{S},n_{E})$ pebbles, such that Environment can move the
additional pebble from one $\hat{}l$ to the next. Indeed, this holds in the
initial configuration by choice of $n^{\text{min}}_{\text{E}}$ (in that case,
$\hat{}l$ is the initial E-location), and the previous observation ensures
that it is always possible to find, after each move of Environment in the
original game, a new position $l$ of $E^{*}(\hat{}l)$, which satisfies $P(l)$
and $C_{\text{E}}(l)\geq K$. Then we take such an $l$ as our new $\hat{}l$.

Given that $C_{\text{E}}(\hat{}l)\geq K$ and that, by definition, $K$ is the
largest bound appearing in the victory condition $\mathcal{F}$, the additional
pebble lying in $\hat{}l$ is irrelevant to whether a congiguration is winning
for Environment or not. ∎

We now have the tools to prove our main decidability result:

######  Theorem 2.

$\textsc{PartSynth}(\textsc{FO}[\sim])$ is decidable.

###### Proof.

Let $(A,\varphi)$ be an input for $\textsc{PartSynth}(\textsc{FO}[\sim])$, and
let $n^{\text{min}}_{\text{E}}$ be the corresponding integer whose existence
is guaranteed by Lemma 1.

Theorem 15 from [1] states that there exists some integer
$n^{\text{min}}_{\text{S}}$ such that System has a
$(n^{\text{min}}_{\text{S}},n^{\text{min}}_{\text{E}})$-winning strategy for
$\varphi$ iff System has a $(n_{S},n^{\text{min}}_{\text{E}})$-winning
strategy for $\varphi$ for any (every) $n_{S}\geq n^{\text{min}}_{\text{S}}$.

We argue in the following that System has an $(n_{S},n_{E})$-winning strategy
for $\varphi$ for some $n_{S},n_{E}\in\mathbb{N}$ if and only if System has an
$(n_{S},n_{E})$-winning strategy for $\varphi$ for some $n_{S}\leq
n^{\text{min}}_{\text{S}}$ and $n_{E}\leq n^{\text{min}}_{\text{E}}$. Thus
there are only a finite number of process configurations to explore in order
to decide whether System has a $(n_{S},n_{E})$-winning strategy for $\varphi$
for some $n_{S},n_{E}\in\mathbb{N}$. When the numbers $n_{S}$ and $n_{E}$ of
processes are fixed, one can duplicate the letter from the alphabet (for
instance, multiplying $A_{\mathrm{S}}$ by the number of System processes), and
reduce the synthesis problem on data words to the decidable synthesis problem
on plain words [3], and thus decide the problem in each of this finitely many
fixed configurations. It is important to note that the bounds
$n^{\text{min}}_{\text{S}}$ and $n^{\text{min}}_{\text{E}}$ are computable.

Let us now show that one need not look further than
$(n^{\text{min}}_{\text{S}},n^{\text{min}}_{\text{E}})$: suppose that System
has an $(n_{S},n_{E})$-winning strategy for $\varphi$. Let us consider four
cases, which cover all the possible values of $n_{S}$ and $n_{E}$.

  * •

If $n_{S}\leq n^{\text{min}}_{\text{S}}$ and $n_{E}\leq
n^{\text{min}}_{\text{E}}$, there is nothing to prove.

  * •

If $n_{S}>n^{\text{min}}_{\text{S}}$ and $n_{E}>n^{\text{min}}_{\text{E}}$,
then in virtue of Lemma 1, System has an
$(n_{S},n^{\text{min}}_{\text{E}})$-winning strategy for $\varphi$. In turn,
Theorem 15 from [1] ensures System has an
$(n^{\text{min}}_{\text{S}},n^{\text{min}}_{\text{E}})$-winning strategy for
$\varphi$.

  * •

If $n_{S}\leq n^{\text{min}}_{\text{S}}$ and
$n_{E}>n^{\text{min}}_{\text{E}}$, then Lemma 1 ensures System has an
$(n_{S},n^{\text{min}}_{\text{E}})$-winning strategy for $\varphi$.

  * •

Finally, suppose $n_{S}>n^{\text{min}}_{\text{S}}$ and $n_{E}\leq
n^{\text{min}}_{\text{E}}$. Remark that in the proof of Theorem 15 from [1],
$\hat{N}$ increases as $k_{e}$ increases. This means that, since System has a
winning strategy with more than $n^{\text{min}}_{\text{S}}$ processes for
$\varphi$ when Environment has $n^{\text{min}}_{\text{E}}$ processes if and if
System has an $(n^{\text{min}}_{\text{S}},n^{\text{min}}_{\text{E}})$-winning
strategy for $\varphi$, then _a fortiori_ System has a winning strategy with
more than $n^{\text{min}}_{\text{S}}$ processes for $\varphi$ when Environment
has $n_{E}$ processes if and if System has an
$(n^{\text{min}}_{\text{S}},n_{E})$-winning strategy for $\varphi$.

In all of these cases, the search for a winning strategy for $\varphi$ can be
limited to $[0,n^{\text{min}}_{\text{S}}]\times[0,n^{\text{min}}_{\text{E}}]$,
which concludes the proof. ∎

##  4 Undecidability results

When System and Environment processes are partitioned, we have seen that when
one is only allowed to check whether two positions belong to the same process,
the synthesis problem is decidable for FO. In this section, we show that as
soon as we are able to compare the relative positions of two processes, this
is no longer the case, even when restricting ourselves to the two-variable
setting, and when having access only to one positional relations ($<$ or
$+1$): both $\textsc{PartSynth}(\textsc{FO}^{2}[\sim,<])$ (Theorem 3) and
$\textsc{PartSynth}(\textsc{FO}^{2}[\sim,+1])$ (Theorem 4) are undecidable.

When processes are shared, the prospect is even darker: it was shown in [1]
that the synthesis problem in undecidable for $\textsc{FO}[\sim]$. We argue
that this is already the case in the two-variable fragment:
$\textsc{SharedSynth}(\textsc{FO}^{2}[\sim])$ is already undecidable (Theorem
5).

###  4.1 Undecidability of $\textsc{PartSynth}(\textsc{FO}^{2}[\sim,<])$ and
$\textsc{PartSynth}(\textsc{FO}^{2}[\sim,+1])$

Let us start by considering the case where the only positional relation is the
order. We show in the following that when System and Environment processes are
separated, the synthesis problem is undecidable in this setting.

######  Theorem 3.

$\textsc{PartSynth}(\textsc{FO}^{2}[\sim,<])$ is undecidable.

###### Proof.

We prove this theorem by reduction from the halting problem for two-counter
Minsky machines. A _two-counter Minsky machine_ $M$ has a finite set of states
$\mathcal{Q}$ (containing an initial state $q_{0}$ and an halting state
$q_{h}$), two counters $c_{0}$ and $c_{1}$ and a set of transitions
$\mathcal{T}$, which is partitioned into

$\mathcal{T}=\biguplus_{i=0,1}\mathcal{T}^{++}_{i}\uplus\mathcal{T}^{--}_{i}\uplus\mathcal{T}^{==0}_{i}\,,$

where $\mathcal{T}^{++}_{i}\subseteq\mathcal{Q}\times\mathcal{Q}$ is the set
of transitions incrementing counter $c_{i}$,
$\mathcal{T}^{--}_{i}\subseteq\mathcal{Q}\times\mathcal{Q}$ is the set of
transitions decrementing counter $c_{i}$, and $\mathcal{T}^{==0}_{i}$ is the
set of zero-test transitions on counter $c_{i}$. A _configuration_ of $M$ is a
triple $(q,v_{0},v_{1})$, where $q\in\mathcal{Q}$ indicates the current state
of the machine and $v_{i}\in\mathbb{N}$ the value of counter $c_{i}$. A _run_
of $M$ is a sequence starting in the initial configuration $(q_{0},0,0)$, and
such that two successive configurations $(q,v_{0},v_{1})$ and
$(q^{\prime},v^{\prime}_{0},v^{\prime}_{1})$ satisfy the following condition:
either $v^{\prime}_{i}=v^{\prime}_{i}+1$, $v^{\prime}_{1-i}=v_{1-i}$ and
$(q,q^{\prime})\in\mathcal{T}^{++}_{i}$, or $v^{\prime}_{i}=v^{\prime}_{i}-1$,
$v^{\prime}_{1-i}=v_{1-i}$ and $(q,q^{\prime})\in\mathcal{T}^{--}_{i}$, or
$v^{\prime}_{i}=v_{i}=0$, $v^{\prime}_{1-i}=v_{1-i}$ and
$(q,q^{\prime})\in\mathcal{T}^{==0}_{i}$. A run is _halting_ if it is finite
and ends in some configuration $(q_{h},v_{0},v_{1})$ for any
$v_{i}\in\mathbb{N}$. It is undecidable, on input $M$, to tell whether such a
halting run exists [8].

Given such a machine $M$, we exhibit a formula $\varphi_{M}$, computable from
$M$, with the following property: there exists a halting run for $M$ iff
System has an $(n_{S},1)$-winning strategy for $\varphi_{M}$ for some
$n_{S}\in\mathbb{N}$. This proves the Theorem.

We consider the signature $A:=A_{E}\uplus A_{S}$ where
$A_{E}:=\\{\text{ok}_{E},\text{ko}_{E}\\}$ and

$A_{S}:=\\{\text{inc}_{0},\text{dec}_{0},\text{inc}_{1},\text{dec}_{1},\text{noop},\text{ok}_{S},\text{ko}_{S}\\}\uplus\mathcal{Q}\uplus\mathcal{T}\,.$

Let us start by giving an example of a data word encoding a halting run.
Suppose that $\mathcal{Q}:=\\{q_{0},q_{1},q_{2},q_{h}\\}$ and
$\mathcal{T}:=\\{t_{0},t_{1},t_{2}\\}$ where

$\begin{cases}t_{0}:q_{0}\xrightarrow{c_{0}++}q_{0}\\\
t_{1}:q_{0}\xrightarrow{c_{0}--}q_{1}\\\
t_{2}:q_{1}\xrightarrow{c_{0}--}q_{2}\\\
t_{3}:q_{2}\xrightarrow{c_{0}==0}q_{h}\end{cases}$

The halting run ($t_{0}\cdot t_{0}\cdot t_{1}\cdot t_{2}\cdot t_{3}$) of $M$
could be represented as the following data word, where we denote System’s
processes by integers, and Environment’s process as $\bullet$. Here, System
plays mainly on process $0$; they could have mixed their play, as the only
time process identity matters is when playing $\text{inc}_{i}$ or
$\text{dec}_{i}$.

$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(0,\text{ok}_{S})}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(\bullet,\text{ok}_{E})}$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(0,q_{0})(0,t_{0})(0,\text{inc}_{0})(0,\text{ok}_{S})}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(\bullet,\text{ok}_{E})}$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(0,q_{0})(0,t_{0})(1,\text{inc}_{0})(0,\text{ok}_{S})}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(\bullet,\text{ok}_{E})}$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(0,q_{0})(0,t_{1})(0,\text{dec}_{0})(0,\text{ok}_{S})}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(\bullet,\text{ok}_{E})}$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(0,q_{1})(0,t_{2})(1,\text{dec}_{0})(0,\text{ok}_{S})}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(\bullet,\text{ok}_{E})}$
$\displaystyle{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(0,q_{2})(0,t_{3})(0,\text{noop})(0,\text{ok}_{S})}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(\bullet,\text{ok}_{E})}{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(0,q_{h})}$

Let us inspect this data word step-by-step. The first two letters of the data
word representing a valid run are always an $\text{ok}_{S}$ by System followed
by an $\text{ok}_{E}$ by Environment.

Following these two letters, we get a succession of the pattern

${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\\_,q)(\\_,t)(\\_,l)(\\_,\text{ok}_{S})}{\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}(\\_,\text{ok}_{E})}$

where $q\in\mathcal{Q},t\in\mathcal{T}$ and $l$ is either noop, an
$\text{inc}_{i}$ or a $\text{dec}_{i}$. Eventually, the data words stops in
the halting state $q_{h}$.

Notice how the value of $c_{0}$ is encoded during this run: at any point
during the run, the value of $c_{0}$ is equal to the number of System
processes on which an $\text{inc}_{0}$ has been played, but no
$\text{dec}_{0}$. Thus, following a transition in $\mathcal{T}^{++}_{i}$,
$\varphi_{M}$ will force System to play an $\text{inc}_{i}$ on a new process.
Similarly, after each transition in $\mathcal{T}^{--}_{i}$, in order not to
lose immediately, System will be forced to play a $\text{dec}_{i}$ on a
process on which an $\text{inc}_{i}$ has been played, but no $\text{dec}_{i}$
yet. When the transition is in $\mathcal{T}^{==0}_{i}$, System must play a
noop on any process; and $\varphi_{M}$ grants Environment a immediate win if
$c_{i}$ is not zero - that is, if there exists a process on which an
$\text{inc}_{i}$ and no $\text{dec}_{i}$ have been played.

Let us now explain how players are prevented from cheating to their advantage.
The mechanism of fraud prevention is always the same: if System cheats, then
Environment immediately responds by playing $\text{ko}_{E}$, and on the other
way around, System plays $\text{ok}_{S}$ when detecting a fraud from
Environment. Note that there is by definition an asymmetry between the
players, and that the $\text{ko}_{S}$ can be differed by the Environment; but
the fairness assumption guarantees that System will be able to output their
$\text{ko}_{S}$ after some time. Once a $\text{ko}_{E}$ or $\text{ko}_{S}$ has
been played, both players are encouraged to stop (a player who plays after a
ko loses the game), and $\varphi_{M}$ checks whether the ko is justified. If
the other player indeed was cheating, then the player who ko’ed wins,
otherwise they lose.

Environment can cheat in only three ways:

  1. [E1]

by not respecting the prefix $(\\_,\text{ok}_{S})(\\_,\text{ok}_{E})$

  2. [E2]

by playing multiple $\text{ok}_{E}$ in a row

  3. [E3]

by playing an $\text{ok}_{E}$ before their turn, i.e. before System has played
their $\text{ok}_{S}$

Let us now described the ways System can cheat:

  1. [S1]

by not respecting the prefix $(\\_,\text{ok}_{S})(\\_,\text{ok}_{E})$

  2. [S2]

by not respecting the order or number of their letters in a pattern ($q\to
t\to\text{inc}_{i}/\text{dec}_{i}/\text{noop}\to\text{ok}_{S}$)

  3. [S3]

by playing some $q\in\mathcal{Q}$ which is not the end-state of the last
transition (or $q_{0}$ if it is the first state)

  4. [S4]

by playing some $t\in\mathcal{T}$ which does not start in the previous state

  5. [S5]

by playing an $\text{inc}_{i}$, $\text{dec}_{i}$ or noop which does not match
the previous transition

  6. [S6]

by playing $\text{inc}_{i}$ on a process on which an $\text{inc}_{i}$ has
already been played

  7. [S7]

by playing $\text{dec}_{i}$ on a process on which an $\text{dec}_{i}$ has
already been played

  8. [S8]

by playing $\text{dec}_{i}$ on a process on which no $\text{inc}_{i}$ has been
played

  9. [S9]

by playing some $t\in\mathcal{T}^{==0}_{i}$ while $c_{i}$ is non-zero

On top of that, $\varphi_{M}$ ensures a player loses the game if they refuse
to play when their turn comes.

The following notations will be useful:

$\begin{cases}\mathcal{Q}(x)&:=\quad\bigvee_{q\in\mathcal{Q}}\ q(x)\\\
\mathcal{T}(x)&:=\quad\bigvee_{t\in\mathcal{T}}\ t(x)\\\
\mathcal{T}^{++}_{i}(x)&:=\quad\bigvee_{t\in\mathcal{T}^{++}_{i}}\ t(x)\\\
\mathcal{T}^{--}_{i}(x)&:=\quad\bigvee_{t\in\mathcal{T}^{--}_{i}}\ t(x)\\\
\mathcal{T}^{==0}_{i}(x)&:=\quad\bigvee_{t\in\mathcal{T}^{==0}_{i}}\ t(x)\\\
\mathcal{U}(x)&:=\quad\text{noop}(x)\ \lor\ \bigvee_{i=0,1}\
\text{inc}_{i}(x)\lor\text{dec}_{i}(x)\\\ A_{S}(x)&:=\quad\bigvee_{a\in
A_{S}}a(x)\\\ A_{E}(x)&:=\quad\bigvee_{a\in A_{E}}a(x)\end{cases}$

The following formula $\Phi_{\text{ko}_{S}}$ is satisfied when there is an
irregularity on Environment’s part since System last played an $\text{ok}_{S}$
(either [E2] or [E3]). Thus, System wins if they play $\text{ko}_{S}$ while
$\Phi_{\text{ko}_{S}}$ is satified.

$\displaystyle\Phi_{\text{ko}_{S}}:=\exists x,$ $\displaystyle\
\text{ok}_{S}(x)\land\big{(}\forall y,x<y\to\neg\text{ok}_{S}(y)\big{)}$
$\displaystyle\land\exists
y,x<y\land\text{ok}_{E}(y)\land\Big{[}\big{(}\exists
x,y<x\land\text{ok}_{E}(y)\big{)}\lor\neg\big{(}\exists
y,x<y\land\text{ok}_{S}(y)\big{)}\Big{]}$

Conversely, $\Phi_{\text{ko}_{E}}$ holds when System has cheated since
Environment last played an $\text{ok}_{E}$. Thus, $\varphi_{M}$ will ensure
that Environment wins if they output a $\text{ko}_{E}$ while
$\Phi_{\text{ko}_{E}}$ holds. Due to the number of ways for System to cheat,
we introduce subformulas to cover each case.

$\displaystyle\Phi_{\text{ko}_{E}}:=\exists x,$ $\displaystyle\
\text{ok}_{E}(x)\land\big{(}\forall y,x<y\to\neg\text{ok}_{E}(y)\big{)}$
$\displaystyle\land\Big{[}\Psi_{\text{bad sequence}}(x)\lor\Psi_{\text{bad
target}}(x)\lor\Psi_{\text{bad source}}(x)\lor\Psi_{\text{bad
upkeep}}(x)\lor\Psi_{\text{bad zero test}}(x)\Big{]}$

where

  * •

$\Psi_{\text{bad sequence}}(x)$ covers [S2]

  * •

$\Psi_{\text{bad target}}(x)$ covers [S3]

  * •

$\Psi_{\text{bad source}}(x)$ covers [S4]

  * •

$\Psi_{\text{bad upkeep}}(x)$ covers [S5], [S6], [S7] and [S8]

  * •

$\Psi_{\text{bad zero test}}(x)$ covers [S9].

$\displaystyle\Psi_{\text{bad sequence}}(x):=$ $\displaystyle\quad\exists
y>x,\ \begin{aligned} \Big{[}\quad&\mathcal{Q}(y)\ \land\ \exists
x>y,\mathcal{Q}(x)\\\ \lor\ &\mathcal{T}(y)\ \land\ \exists
x>y,\big{(}\mathcal{Q}(x)\lor\mathcal{T}(x)\big{)}\\\ \lor\ &\mathcal{U}(y)\
\land\ \exists
x>y,\big{(}\mathcal{Q}(x)\lor\mathcal{T}(x)\lor\mathcal{U}(x)\big{)}\\\ \lor\
&\text{ok}_{S}(y)\ \land\ \exists x>y,A_{S}(x)\quad\Big{]}\end{aligned}$
$\displaystyle\lor\ \big{(}\exists y>x,\ A_{S}(y)\big{)}\ \land\
\neg\big{(}\exists y>x,\ \mathcal{Q}(y)\big{)}$ $\displaystyle\lor\
\big{(}\exists y>x,\ \mathcal{U}(y)\ \lor\ \text{ok}_{S}(y)\big{)}\ \land\
\neg\big{(}\exists y>x,\ \mathcal{T}(y)\big{)}$ $\displaystyle\lor\
\big{(}\exists y>x,\ \text{ok}_{S}(y)\big{)}\ \land\ \neg\big{(}\exists y>x,\
\mathcal{U}(y)\big{)}$ $\displaystyle\Psi_{\text{bad target}}(x):=$
$\displaystyle\ \neg\big{(}\exists y>x,\ \mathcal{T}(y)\big{)}\ \land\
\bigvee_{q\in\mathcal{Q}}\Big{[}\big{(}\exists y>x,\ q(y)\big{)}\ \land\
\exists x,\big{(}[\forall y>x,\ \neg\mathcal{T}(y)]\ \land\
\bigvee_{\begin{subarray}{c}t\in\mathcal{T}\text{ doesn't}\\\ \text{end in
}q\end{subarray}}t(x)\big{)}\Big{]}$ $\displaystyle\lor\ \neg\big{(}\exists
y,\ \mathcal{T}(y)\big{)}\ \land\
\bigvee_{q\in\mathcal{Q}\setminus\\{q_{0}\\}}\exists y,\ q(y)$
$\displaystyle\Psi_{\text{bad source}}(x):=$
$\displaystyle\bigvee_{q\in\mathcal{Q}}\quad\bigvee_{\begin{subarray}{c}t\in\mathcal{T}\text{
doesn't}\\\ \text{start in }q\end{subarray}}\Big{[}\big{(}\exists y>x,\
q(y)\big{)}\ \land\ \big{(}\exists y>x,\ t(y)\big{)}\Big{]}$
$\displaystyle\Psi_{\text{bad upkeep}}(x):=$
$\displaystyle\bigvee_{i=0,1}\begin{aligned} \Big{[}\quad&\big{(}\exists y>x,\
\mathcal{T}^{++}_{i}(y)\big{)}\ \land\ \big{(}\exists y>x,\
\mathcal{U}(y)\land\neg\text{inc}_{i}(y)\big{)}\\\ \lor\ &\big{(}\exists y>x,\
\mathcal{T}^{--}_{i}(y)\big{)}\ \land\ \big{(}\exists y>x,\
\mathcal{U}(y)\land\neg\text{dec}_{i}(y)\big{)}\\\ \lor\ &\big{(}\exists y>x,\
\mathcal{T}^{==0}_{i}(y)\big{)}\ \land\ \big{(}\exists y>x,\
\mathcal{U}(y)\land\neg\text{noop}(y)\big{)}\\\ \lor\ &\exists y>x,\
\big{(}\text{inc}_{i}(y)\ \land\ \exists x<y,\ [x\sim y\ \land\
\text{inc}_{i}(x)]\big{)}\\\ \lor\ &\exists y>x,\ \big{(}\text{dec}_{i}(y)\
\land\ \exists x<y,\ [x\sim y\ \land\ \text{dec}_{i}(x)]\big{)}\\\ \lor\
&\exists y>x,\ \big{(}\text{dec}_{i}(y)\ \land\ \neg(\exists x<y,\ [x\sim y\
\land\ \text{inc}_{i}(x)])\big{)}\quad\Big{]}\end{aligned}$
$\displaystyle\Psi_{\text{bad zero test}}(x):=$
$\displaystyle\bigvee_{i=0,1}\Big{[}\big{(}\exists y>x,\
\mathcal{T}^{==0}_{i}(y)\big{)}\ \land\ \exists x,\big{[}\text{inc}_{i}(x)\
\land\ \neg(\exists y,\ y\sim x\ \land\ \text{dec}_{i}(x))\big{]}\Big{]}$

It only remains to cover cases [E1] and [S1], with $\Phi_{\text{bad prefix
E}}$ and $\Phi_{\text{bad prefix S}}$, as well as the case where a players
refuses to play when their turn comes, covered by $\Phi_{\text{E blocks}}$ and
$\Phi_{\text{S blocks}}$, and the immediate loss when a players keeps playing
after a ko, with $\Phi_{\text{E plays after ko}}$ and $\Phi_{\text{S plays
after ko}}$. We use first, second and last to respectively denote the first,
second and last element wrt. $<$, which are obviously definable in
$\textsc{FO}^{2}[\sim,<]$.

$\displaystyle\Phi_{\text{bad prefix E}}:=$ $\displaystyle\quad
A_{E}(\texttt{first})\ \lor\
\big{[}A_{E}(\texttt{second})\land\neg\text{ok}_{E}(\texttt{second})\big{]}$
$\displaystyle\Phi_{\text{bad prefix S}}:=$
$\displaystyle\quad\big{[}A_{S}(\texttt{first})\land\neg\text{ok}_{S}(\texttt{first})\big{]}\
\lor\ A_{S}(\texttt{second})$ $\displaystyle\Phi_{\text{E blocks}}:=$
$\displaystyle\quad\text{ok}_{S}(\texttt{last})$ $\displaystyle\Phi_{\text{S
blocks}}:=$ $\displaystyle\quad(\neg\exists x,\top)\ \lor\
\text{ko}_{E}(\texttt{last})\ \lor\ \big{[}\mathcal{Q}(\texttt{last})\land\neg
q_{h}(\texttt{last})\big{]}\ \lor\ \mathcal{T}(\texttt{last})\ \lor\
\mathcal{U}(\texttt{last})$ $\displaystyle\Phi_{\text{E plays after ko}}:=$
$\displaystyle\quad A_{E}(\texttt{last})\ \land\ \exists
x,x\neq\texttt{last}\land\big{[}\text{ko}_{E}(x)\lor\text{ko}_{S}(x)\big{]}$
$\displaystyle\Phi_{\text{S plays after ko}}:=$ $\displaystyle\quad
A_{S}(\texttt{last})\ \land\ \exists
x,x\neq\texttt{last}\land\big{[}\text{ko}_{E}(x)\lor\text{ko}_{S}(x)\big{]}$

We are now ready to make $\varphi_{M}$ explicit. We want to $\varphi_{M}$ hold
either when Environment has made a misplay (either by satisfying
$\Phi_{\text{bad prefix E}}$, $\Phi_{\text{E blocks}}$ or $\Phi_{\text{E plays
after ko}}$, or by making a move after which System can play $\text{ko}_{S}$
and satisfy $\Phi_{\text{ko}_{S}}$), or if System has made no misplay (in
which case the data word represents a valid run) and this run ends in $q_{h}$:

$\displaystyle\varphi_{M}:=$ $\displaystyle\quad\Phi_{\text{bad prefix E}}\
\lor\ \Phi_{\text{E blocks}}\ \lor\ \Phi_{\text{E plays after ko}}\ \lor\
\big{[}\exists x,\text{ko}_{S}(x)\land\Phi_{\text{ko}_{S}}\big{]}$
$\displaystyle\lor\Big{(}\neg\Phi_{\text{bad prefix S}}\ \land\
\neg\Phi_{\text{S blocks}}\ \land\ \neg\Phi_{\text{S plays after ko}}\ \land\
\neg\big{[}\exists x,\text{ko}_{E}(x)\land\Phi_{\text{ko}_{E}}\big{]}\ \land\
q_{h}(\texttt{last})\Big{)}$

It remains to explain why System having a winning strategy for $\varphi_{M}$
amounts exactly to the existence of a halting run in $M$. First, consider a
halting run of $M$. It is straighforward to see that System has an
$(n_{S},1)$-winning strategy for $\varphi_{M}$, where $n_{S}$ is the total
number of transition of $\bigcup_{i=0,1}\mathcal{T}^{++}_{i}$ used in the run
(or $n_{S}=1$ if no such transitions are used): start by playing
$\text{ok}_{S}$ on any process, and wait for Environment to play
$\text{ok}_{E}$ on their process. Once this is done, play according to the
run, in the sequence $q\to
t\to\text{inc}_{i}/\text{dec}_{i}/\text{noop}\to\text{ok}_{S}$ (taking care to
play $\text{inc}_{i}$ on a new process each time, and $\text{dec}_{i}$ on a
process which has an $\text{inc}_{i}$ but no $\text{dec}_{i}$), and after each
such sequence wait for the acknowledgement from Environment, in the form of an
$\text{ok}_{E}$. Then stop when reaching $q_{h}$. If Environment blocks, block
as well; if Environment deviates by playing $\text{ok}_{E}$ too soon, play
$\text{ko}_{S}$ as soon as possible and then block; if Environment plays
$\text{ko}_{E}$, block. It is easily shown by induction on the length of the
run that such a strategy is winning for $\varphi_{M}$, and indeed require only
$n_{S}$ processes.

Conversely, suppose that System has an $(n_{S},1)$-winning strategy for
$\varphi_{M}$, for some $n_{S}\in\mathbb{N}$. We argue this entails the
existence of a halting run in $M$. Let us inspect the data word $w$ produced
by this winning strategy against an Environment which respects the
aforementioned rules (namely, which waits their turn to play $\text{ok}_{E}$,
unless System cheats, i.e. if the current data word satisfies
$\Phi_{\text{ko}_{E}}$, in which case Environment plays a $\text{ko}_{E}$ and
stops). Since Environment respects the format and makes no false allegation,
$\varphi_{M}$ cannot be satisfied because of the subformulas $\Phi_{\text{bad
prefix E}}$, $\Phi_{\text{E blocks}}$, $\Phi_{\text{E plays after ko}}$ or
$\exists x,\text{ko}_{S}(x)\land\Phi_{\text{ko}_{S}}$. Hence, the second part
of $\varphi_{M}$ must hold: $\Phi_{\text{bad prefix S}}$, $\Phi_{\text{S
blocks}}$ and $\Phi_{\text{S plays after ko}}$ are false, no $\text{ko}_{E}$
was played, and $q_{h}(\texttt{last})$ holds: System’s part of $w$ must start
with an $\text{ok}_{S}$, followed by a sequence of patterns $q\to
t\to\text{inc}_{i}/\text{dec}_{i}/\text{noop}\to\text{ok}_{S}$ interspered
with $\text{ok}_{E}$ from Environment, until it reaches a position marked with
$q_{h}$. Since Environment played no $\text{ko}_{E}$, at no point was
$\Phi_{\text{ko}_{E}}$ satisfied, which means that one can reproduce in a run
of $M$ the sequence of states and transitions played by System in $w$: by
induction on the number of patterns $q\to
t\to\text{inc}_{i}/\text{dec}_{i}/\text{noop}\to\text{ok}_{S}$ played by
System, one shows that there is a corresponding run in $M$ whose last
configuration is $(q,v_{0},v_{1})$, where $q$ is the last letter from
$\mathcal{Q}$ played by System and $v_{i}$ is the number of processes from
$\mathbb{P}_{\mathrm{S}}$ marked with one $\text{inc}_{i}$ and no
$\text{dec}_{i}$. The validity of the transitions from $\mathcal{T}^{--}_{i}$
and $\mathcal{T}^{==0}_{i}$ comes from the fact $\Psi_{\text{bad upkeep}}(x)$
and $\Psi_{\text{bad zero test}}(x)$ were never satisfied, for otherwise
Environment would have immediately played a $\text{ko}_{E}$. Considering the
whole of $w$, we get a run of $M$ ending in $q_{h}$, thus concluding the
proof. ∎∎

Let us now argue that this problem remains undecidable if one has access to
the successor relation on positions, rather that to the order itself:

######  Theorem 4.

$\textsc{PartSynth}(\textsc{FO}^{2}[\sim,+1])$ is undecidable.

First of all, note that Theorems 3 and 4 are not derivable from one another,
as $\textsc{FO}^{2}[\sim,<]$ and $\textsc{FO}^{2}[\sim,+1]$ have orthogonal
expressive power: with only two variables, the successor relation is not
definable from the order.

###### Sketch of proof.

The main idea is to note that in the proof of Theorem 3, the encoding of a run
follows a sequence of patterns of size 5 ($q\to
t\to\text{inc}_{i}/\text{dec}_{i}/\text{noop}\to\text{ok}_{S}\to\text{ok}_{E}$).
Furthermore, as soon as an $\text{ok}_{E}$ or $\text{ok}_{S}$ is issued, the
suspected violation can be found in the positions immediately preceding it (in
the case of $\text{ok}_{E}$) or is easily seen globally (in the case of an
$\text{ok}_{S}$ issued to report an instance of [E2] or [E3], which can be
delayed for arbitraily long by Environment). As a consequence of this
locality, all the formulas in the proof can be reformulated with $+1$ instead
of $<$. ∎∎

###  4.2 Undecidability of $\textsc{SharedSynth}(\textsc{FO}^{2}[\sim])$

Let us now turn to the case where processes are shared between both players.
In this context, not much can be done:
$\textsc{SharedSynth}(\textsc{FO}[\sim])$ was shown to be undecidable in [1].
As we now show, this problem is already undecidable when we restrict ourselves
to two variables.

######  Theorem 5.

$\textsc{SharedSynth}(\textsc{FO}^{2}[\sim])$ is undecidable.

###### Sketch of proof.

We give a guideline to adapt the proof of undecidability of
$\textsc{SharedSynth}(\textsc{FO}[\sim])$ ([1], Theorem 17) to the case where
only two variables are available. That proof was a reduction from the halting
problem for two-counter Minsky machines, but in a way that is quite different
from the reduction from the proof of Theorem 3: the idea was to encode the
value of each counter as the number of processes having a particular number of
actions played by both System and Environment. Namely, to increment a counter,
System and Environment would cooperate to pick a fresh process and perform two
$a$’s (from System) and two $b$’s (from Environment) on it. To decrement the
same counter, one such process would further receive two additional $a$’s and
$b$’s, and from this point on this particular process would never be involved
again. A limited kind of alternation enforced by the formula made sure System
and Environment followed this construction; otherwise they immediately lost
the game.

The winning condition in the previous proof was given as a condition on the
locations of the corresponding parameterized vector game, but it is
straightforward to go back to $\textsc{FO}[\sim]$ formulas from those. The
number of variables needed depends on the largest value appearing in the count
of the number of letters for a given process or in the count of the number of
processes for a given location. For instance, we need two different variables
to express that a process has at least two $a$’s, or that it has exactly one
$a$ (by stating it has at least one and not at least two):

$\varphi_{|a|\geq 2}(x):=\exists y,\ y\sim x\ \land\ a(y)\ \land\ \exists x,\
x\sim y\ \land x\neq y\ \land\ a(x)\,.$

Similarly if we want to specify that there are at least two such processes
then we need at least two different variables.

The counting of processes for a given location is not a problem for the proof
in the case of $\textsc{FO}^{2}[\sim]$, as we only check for the existence of
exactly zero (one variable needed), exactly one (two variables needed), at
least zero (no variable needed), and at least one (one variable needed)
processes in a particular location. The only hurdle lies in the counting of
actions, as we need to count up to four occurrences for each letter (as seen
above, four $a$’s and four $b$’s). The trick to overcome this difficulty is to
use multiple letters to play the same role, instead of just one: $a$ is split
into $a_{1}$ and $a_{2}$, and $b$ into $b_{1}$ and $b_{2}$. And indeed,
although it was not possible in $\textsc{FO}^{2}$ to express the existence of
a process with four $a$’s or more, we can now use a formula stating the
existence of a process with at least two $a_{1}$’s and two $a_{2}$’s with only
two variables: $\varphi_{|a_{1}|\geq 2}(x)\land\varphi_{|a_{2}|\geq 2}(x)$.
The incrementation of a counter is now encoded by playing exactly one $a_{1}$,
one $a_{2}$, one $b_{1}$, and one $b_{2}$ (instead of exactly two $a$’s and
two $b$’s) on a new process, and to decrement a counter, we double the count
of each letter as was done previously. We now only need to count the number of
occurrences of each letter up to two, which can be done with two variables
instead of four. The rest of the proof is unchanged. ∎

##  5 Conclusion

In this paper, we have answered the questions left open in [1]. It appears
that when positions between two processes can be compared, the synthesis
problem quickly becomes undecidable. As a next step, it thus seems natural to
consider the case of partitioned processes for an intermediate logic between
$\textsc{FO}^{2}[\sim]$ and $\textsc{FO}^{2}[\sim,<]$:
$\textsc{FO}^{2}[\lesssim]$, where one can compare only positions pertaining
to the same process.

## References

  * [1] Bérard, B., Bollig, B., Lehaut, M., Sznajder, N.: Parameterized synthesis for fragments of first-order logic over data words. In: Foundations of Software Science and Computation Structures FOSSACS. Springer (2020)
  * [2] Bojanczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: 21th IEEE Symposium on Logic in Computer Science LICS (2006)
  * [3] Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society (1969)
  * [4] Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic – Volume 1 (1957)
  * [5] Figueira, D., Praveen, M.: Playing with repetitions in data words using energy games. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS (2018)
  * [6] Khalimov, A., Maderbacher, B., Bloem, R.: Bounded synthesis of register transducers. In: Automated Technology for Verification and Analysis - 16th International Symposium, ATVA (2018)
  * [7] Libkin, L.: Elements of Finite Model Theory. Springer (2004)
  * [8] Minsky, M.L.: Computation. Prentice-Hall Englewood Cliffs (1967)