# Synthesising Full-Information Protocols

Dietmar Berwanger, Laurent Doyen, Thomas Soullard

► To cite this version:

Dietmar Berwanger, Laurent Doyen, Thomas Soullard. Synthesising Full-Information Protocols. FSTTCS 2025 – 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, BITS Pilani, K K Birla Goa Campus, India, Dec 2025, Goa, India. pp. 13:1–13:18, 10.4230/LIPIcs.FSTTCS.2025.13 . hal-05407606

HAL Id: hal-05407606

https://hal.science/hal-05407606v1

Submitted on 9 Dec 2025

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# Synthesising Full-Information Protocols

**Dietmar Berwanger**

<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /></figure>

Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Paris, France

**Laurent Doyen**

<figure><img src="image_4.png" /></figure>

<figure><img src="image_5.png" /></figure>

Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Paris, France

**Thomas Soullard**

<figure><img src="image_6.png" /></figure>

<figure><img src="image_7.png" /></figure>

Université Paris-Saclay, CNRS, ENS Paris-Saclay, Laboratoire Méthodes Formelles, Paris, France

## Abstract

We study a communication model where processes reveal their entire local information whenever they interact. However, the system involves an indeterminate environment that may control when a communication event occurs and which participants are involved. As a result, the amount of information a process may receive at once is unbounded.

Such full-information protocols are common in the distributed-computing literature. Here, we consider synchronous systems, modelled as infinite games with imperfect information played on finite graphs. We present a decision procedure for the synthesis of a process with an $\omega$-regular specification in a system where the other participating processes are fixed. The challenge lies in constructing a finite representation of information trees with unbounded branching. Our construction is non-elementary in the size of the problem instance, and we establish a matching non-elementary lower bound for the complexity of the synthesis problem.

**2012 ACM Subject Classification** Theory of computation → Automata over infinite objects; Theory of computation → Representations of games and their complexity; Computing methodologies → Planning under uncertainty

**Keywords and phrases** Infinite Games on Finite Graphs, Imperfect Information, Reactive Processes, Distributed Synthesis, Dynamic Networks

**Digital Object Identifier** 10.4230/LIPIcs.FSTTCS.2025.13

Related Version Full Version: https://arxiv.org/abs/2307.01063

## 1 Introduction

One core paradigm for the analysis of complex systems is that of reactive processes, introduced by Harel and Pnueli [17]. A reactive process interacts with its environment in a stepwise, ongoing manner: at each stage, it observes an input signal and chooses a control action with the purpose of ensuring that the system satisfies a specified objective.

Unlike terminating programs that compute a function on a given input, reactive processes are meant to operate indefinitely. Their interaction with the environment is naturally modelled as an infinite-duration game between a strategic player, representing the process, and a non-strategic opponent, Nature. The process aims to satisfy the objective regardless of Nature's choices. The synthesis problem – constructing such a process – thus translates to the construction of a winning strategy in an infinite game [7, 29].

Under perfect information, where input and output uniquely determine the system's run, the game is fully observable and, for $\omega$-regular objectives, it can be solved using established algorithms for parity games [10, 25, 29, 8]. In imperfect-information settings, where processes have only partial views of the system state, the problem becomes significantly harder. Classical approaches, going back to Reif [26, 9], reduce such games to perfect-information ones via a powerset construction, incurring exponential cost but preserving strategy equivalence.

<figure><img src="image_8.png" /></figure>

© Dietmar Berwanger, Laurent Doyen, and Thomas Soullard;
licensed under Creative Commons License CC-BY 4.0

45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
(FSTTCS 2025).

Editors: C. Aiswarya, Ruta Mehta, and Subhajit Roy; Article No. 13; pp. 13:1–13:18

<figure><img src="image_9.png" /></figure>

LIPICS
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
13:2 Synthesising Full-Information Protocols

In distributed systems, complexity increases further: multiple processes operate based
on their local observations and must coordinate to achieve a common objective. This yields
coordination games with imperfect information, which are undecidable in general [23, 19, 13].
Even two processes receiving distinct inputs face an undecidable synthesis problem [28].
Coordination may require reasoning about other players’ knowledge – a task that is algorithm-
mically intractable over infinite plays [6].

To study distributed synthesis beyond known undecidability barriers, we consider a model where communication is not restricted in content. We formalise a framework of full-information protocols (FIP), inspired by concepts from distributed computing [22, 11, 31], in which all information held by a sender is transmitted during a communication event. Communication availability is controlled externally, and processes cannot choose which information to reveal. This model captures systems with maximal information exchange constrained only by communication opportunities. Whenever synthesis is possible under arbitrary-bandwidth assumptions, it is also possible in the FIP model.

We formalise distributed systems with FIP semantics as repeated games between players and Nature. In each stage, players choose actions; the resulting action profile determines a set of enabled moves, from which Nature selects one. Each move yields an observation profile, including a local input and a set of views shared via communication. A player’s view accumulates their own observations and, recursively, those of others with whom they communicates, directly or indirectly. Strategies map such views to actions. A profile of strategies determines a set of plays – infinite sequences of moves – and is winning, if all resulting plays satisfy the objective, expressed by an automaton over infinite words.

As full synthesis remains undecidable in general, we focus on the case of a single active
player and an arbitrary number of passive observers. Observers do not act, but their views
may be communicated, conveying unbounded information in a single stage. This creates
information trees with unbounded branching, obstructing classical synthesis approaches
based on finite tree automata [25, 16, 1].

Nevertheless, we prove that synthesis is decidable in this setting. The key lies in a higher-
order quotient construction that vastly extends Reif’s powerset method to accommodate
full-information protocols. It yields a finite game bisimilar to the original one, with winning
strategies transferring via a homomorphism. The construction tracks information records
along nested coalitions of observers, leading to a state space of non-elementary size.

We show that this complexity is tight: the synthesis problem for FIP games with one active
player and *n* observers is as hard as the acceptance problem for Turing machines using *n*-fold
exponential space. Non-elementary bounds have appeared in similar contexts [2, 19, 13, 14, 5],
but are surprising here given the presence of only a single decision maker.

2 Basic Notions

For a function $f : X \to Y$ and a domain subset $Z \subseteq X$, we denote by $f(Z) = \{f(z) \mid z \in Z\}$ the set of images of elements in $Z$. The kernel of $f$ relates elements with the same image $\ker f = \{(x, x') \in X \times X \mid f(x) = f(x')\}$.

For a directed graph (V, E) with edge relation E ⊆ V × V, we designate the set of successors and predecessors of a node v ∈ V by vE = {v' | (v, v') ∈ E} and Ev = {v' | (v', v) ∈ E}.

For a set of players *I*, we refer to any nonempty subset *J* ⊆ *I* as a *coalition*. A *profile* is a tuple of objects *x* = (*x*<sup>*i*</sup>)<sub>*i*∈*I*</sub>, one for each player. Given a profile *x*, we write *x*<sup>*i*</sup> to designate the element corresponding to Player *i*. Likewise, for a coalition *J* ⊆ *I*, we write *x*<sup>*J*</sup> to designate the profile (*x*<sup>*j*</sup>)<sub>*j*∈*J*</sub> of objects associated to its members. In general, we use superscripts for (objects associated to) players or coalitions. To avoid confusion, we denote the powerset of a set *X* by *wp*(*X*) rather than 2<sup>*X*</sup>.
For an alphabet $\Gamma$, the set of finite words over $\Gamma$ is denoted by $\Gamma^*$, the set of finite nonempty words is $\Gamma^+ = \Gamma^* \setminus \{\varepsilon\}$, and the set of infinite words is $\Gamma^\omega$.

## 2.1 Games on Graphs

In the context of reactive systems, games are used to study worst-case scenarios where a system interacts with an adversarial environment. The goal is to synthesise a strategy for the system player that ensures the specification is satisfied regardless of the environment's behaviour. Accordingly, we focus on actions and strategies of one player – or a coalition of players – representing the system, and attribute the environment choices to a nonstrategic player, Nature. In particular, we deviate from traditional terminology by featuring two-player games as games between one player and Nature. To compare games played on different structures, we represent objectives in terms of colours assigned to game positions.

### Perfect Information

Let $A$ be a finite set of actions and $C$ a finite set of colours. A graph game with perfect information is described by a coloured graph $G = (V, v_\varepsilon, (E_a)_{a \in A}, \lambda)$, where $V$ is a set of positions, $v_\varepsilon \in V$ the initial position, each $E_a \subseteq V \times V$ is a transition relation for action $a$, and $\lambda: V \to C$ labels positions with colours. For all $v \in V$ and $a \in A$, we assume that the successor set $vE_a$ is nonempty.

The game is played in stages starting from the initial position $v_\varepsilon$. In a stage at position $v$, the player chooses an action $a \in A$, then Nature selects an edge $(v, w) \in E_a$, and the play moves to position $w$, which is announced to the player. The outcome is an infinite path in $G$ starting from $v_\varepsilon$, called a *play*; finite prefixes are called *histories*.

A reachability objective is given by a binary labelling $\lambda: V \to \{0, 1\}$, and a play is winning if it visits a position labelled 1. A parity objective is specified by a labelling $\lambda: V \to \mathbb{N}$ that assigns priorities to positions, and a play is winning if the least priority visited infinitely often is even.

Strategies in games with perfect information are maps $s: V^* \to A$ from histories to actions. The *outcome* of a strategy $s$ is the set $\text{Out}(s)$ of plays $v_0v_1v_2\dots$ such that $v_{t+1} \in v_tE_a$ for $a = s(v_0v_1\dots v_t)$ at every stage $t \ge 0$. A strategy is winning, if all the plays in $\text{Out}(s)$ are winning. The synthesis problem asks whether such a strategy exists and aims to construct one effectively.

For parity and reachability objectives, it is known that whenever a winning strategy exists, there exists one that depends only on the last position in the history. Such positional strategies can be represented by a labelling of positions with actions. As the winning status of a positional strategy can be verified efficiently, the synthesis problem for parity games is decidable in NP $\cap$ CoNP; reachability games are solvable in polynomial time.

### Partial Observation

One way to model uncertainty is by associating to each position an observation from a finite alphabet $B$, via a function $\beta: V \to B$. In a stage where the game moves to position $w$, only $\beta(w)$ is revealed to the player.

Formally, a graph game with partial observation is given by a coloured graph $(V, v_\varepsilon, (E_a)_{a \in A}, \beta, \lambda)$. Every history $\tau = v_0v_1\dots v_t$ yields an observation history $\hat{\beta}(\tau) := \beta(v_0)\beta(v_1)\dots\beta(v_t)$. Strategies are functions $s: V^* \to A$ from histories to actions that do not distinguish between histories with the same observation. Under the assumption that objectives are *visible*, in the sense that indistinguishable histories end in positions with the
13:4 Synthesising Full-Information Protocols

same colour given by $\lambda$, the synthesis problem for partial-observation games on graphs with
parity or reachability objectives can be reduced to a perfect-information game via a powerset
construction, yielding an EXPTIME-complete problem [26, 9].

To model distributed systems, graph games with partial observation are extended to
multiple players $i \in I$, each with an action set $A^i$, an observation set $B^i$, and a local
observation function $\beta^i: V \to B^i$. The edges are then indexed by action profiles $a = (a^i)_{i \in I}$.
At the stage game from position $v$, each player $i$ selects an action $a^i \in A^i$, Nature chooses
an edge $(v, w) \in E_a$, and each player observes $\beta^i(w)$. Strategies $s^i$ of Player $i$ are functions
that do not distinguish between her observation histories. The outcome of a strategy profile
is formed by the plays that are in the outcome of all component strategies.

The synthesis problem for a given, common objective asks whether there exists a strategy
profile $s = (s^i)_{i \in I}$, such that all outcoming plays satisfy the objective. This problem is
undecidable in general for distributed games with partial observation, even with only two
players against Nature (see, e.g., [28]).

2.2 Automata

We use deterministic finite automata as language acceptors for infinite words and as transducers on finite words.

A Mealy automaton is given by a tuple $(Q, \Gamma, \Sigma, q_{\varepsilon}, \delta, \lambda)$ consisting of a finite set $Q$ of states, a finite input alphabet $\Gamma$, a finite output alphabet $\Sigma$, a designated initial state $q_{\varepsilon} \in Q$, a transition function $\delta : Q \times \Gamma \to Q$, and an output function $\lambda : Q \times \Gamma \to \Sigma$. To describe the internal behaviour, we extend the transition function from input letters to words and define $\delta : Q \times \Gamma^* \to Q$, for every state $q \in Q$, by setting $\delta(q, \varepsilon) := q$, for the empty word $\varepsilon$, and $\delta(q, \tau c) := \delta(\delta(q, \tau), c)$, for words $\tau \in \Gamma^*$ and letters $c \in \Gamma$. Likewise, to describe the external behaviour, we extend the output function to $\lambda : \Gamma^+ \to \Sigma$ by setting $\lambda(\tau c) = \lambda(\delta(q_{\varepsilon}, \tau), c)$ for all $\tau \in \Gamma^*$ and $c \in \Gamma$. A function on $\Gamma^*$ is *regular* if there exists a Mealy automaton that defines it. Further, we define the *cumulative output*, for an input word $\tau = c_1c_2\dots c_n \in \Gamma^*$, as the sequence $\hat{\lambda}(\tau) = \lambda(c_1)\lambda(c_1c_2)\dots\lambda(c_1c_2\dots c_n)$ consisting of the outputs of all prefixes of $\tau$. Finally, we extend $\hat{\lambda}$ to infinite words $\pi = c_1c_2\dots \in \Gamma^{\omega}$, by setting $\hat{\lambda}(\pi) = \lambda(c_1)\lambda(c_1c_2)\dots$

3 The Model

3.1 Repeated Games with Imperfect Information

Our purpose is to model dynamical systems driven by occurrences of discrete state changes
that we call *moves*. System runs correspond to infinite sequences of moves drawn from a
finite set $\Gamma$ as outcome of a multistage game played between a fixed set $I = \{0, 1, \dots, n\}$ of
players and Nature (or Environment, in control-theoretic terminology). Each player $i \in I$
has a set $A^i$ of actions, and any action profile $(a^i)_{i \in I}$ enables a set of moves, according to a
move-action map act: $\Gamma \to A$, which is *surjective*. In every stage, a one-shot *base game* is
played as follows: each player $i \in I$ chooses an *action* $a^i$ from her given action set $A^i$; the
chosen profile $a = (a^i)_{i \in I}$ constrains the set of possible outcomes to the subset of moves
$\{c \in \Gamma \mid \text{act}(c) = a\}$ supported by $a$, from which Nature chooses one. The outcome move
is recorded in the play history, and the game proceeds to the next stage. The outcome of
the multistage game, called a *play*, is thus an infinite sequence $\pi = c_1c_2\dots \in \Gamma^\omega$ of moves.
A *history* (of length $\ell$) is a finite prefix $\tau = c_1c_2\dots c_\ell \in \Gamma^*$ of a play; the empty history $\varepsilon$
has length zero. The objective of a player is described by a subset of plays declared as winning.
To pursue their objectives, players choose actions based on the information available to them. The information of a player $i \in I$ is modelled by a partition $\mathcal{U}^i$ of the set $\Gamma^*$ of histories; the parts of $\mathcal{U}^i$ are called *information sets* (of the player). The intended meaning is that if the actual history belongs to an information set $U \in \mathcal{U}^i$, then Player $i$ considers every history in $U$ possible. The particular case where all information sets in the partition are singletons characterises the setting of *perfect information*.

Our model is synchronous, which means, intuitively, that players always know how many stages have been played. Formally, this amounts to asserting that all histories in an information set have the same length; in particular the empty history forms a singleton information set. Further, we assume that every player has perfect recall – he never forgets what he knew previously, and which actions he took. Formally, if an information set of Player $i$ contains nontrivial histories $\tau c$ and $\tau' c'$, then the predecessor history $\tau$ is in the same information set as $\tau'$ and the moves $c$ and $c'$ are supported by the same action of Player $i$.

A *decision function* for a player $i \in I$ is a map $f^i: \Gamma^* \to A^i$ from histories to actions. We say that a play, or a history, $c_1c_2\dots$ follows $f^i$ if $\text{act}^i(c_t) = f^i(c_1\dots c_{t-1})$, for every stage $t > 0$. Further, we say that an information set $U \in \mathcal{U}^i$ is *reachable* if there exists a history in $U$ that follows $f^i$. A *decision function* $f^i$ is *information consistent* if it is constant on all reachable information sets. A *strategy* for Player $i$ is a decision function that is information consistent (with respect to her information partition). The outcome of a strategy $f^i$ is the set $\text{Out}(f^i) \subseteq \Gamma^\omega$ of plays that follow it. To capture coordination problems in distributed systems, we refer to an objective $W \subseteq \Gamma^\omega$ that is common to all players. A strategy profile $f = (f^i)_{i \in I}$ is *winning* if $\text{Out}(f) \subseteq W$.

Finite-state representation

As we are interested in algorithmic questions for repeated games, we will consider instances
described by finite objects. We assume that the move set $\Gamma$ and the set $A$ of action profiles
are finite. Hence, the action map act: $\Gamma \to A$ provides a finite description of the move
structure, that is, $\Gamma^*$ equipped with the labelling of action profiles.

To represent objectives – sets of infinite words from $\Gamma^\omega$ – we use colouring functions
defined by Mealy automata over $\Gamma$. We mainly work with *parity automata*, which provide a
canonical form for $\omega$-regular specifications relevant as system-design objectives [30]. These
are automata that input moves – drawn during the play – and output natural numbers called
*priorities*: a play is winning if the least priority output infinitely often is even. We sometimes
refer to reachability objectives, given by an automaton that outputs flags 0 or 1: a play is
winning if some prefix history yields output 1.

To describe information partitions in a finite way, it will be convenient to refer to
their representation as *indistinguishability relations*, which equate histories that the player
cannot distinguish. An information partition $\mathcal{U}$ thus corresponds to the equivalence relation
$\sim \in \Gamma^* \times \Gamma^*$ with $\tau \sim \tau'$ whenever $\tau, \tau' \in U$ for some $U \in \mathcal{U}$. Generally, an indistinguishability
relation for Player $i$ is a synchronous equivalence $\sim$ on $(\Gamma \times \Gamma)^*$ that is prefix-closed and
respects the player’s actions: if $\tau c \sim \tau' c'$ then $\tau \sim \tau'$ and $\text{act}^i(c) = \text{act}^i(c')$, for all $\tau, \tau' \in \Gamma^*$
and $c, c' \in \Gamma$. Indeed, $\sim$ defines an information partition with information sets given by
equivalence classes $[\tau] \sim = \{\tau' \in \Gamma^* | \tau' \sim \tau\}$, for each history $\tau \in \Gamma^*$. The information
structures arising from the full-information protocols introduced in this paper are a particular
case of indistinguishability relations recognisable by two-tape deterministic finite automata,
as studied in [4].

We shall distinguish between the finite-state representation of a repeated game, for
instance as a tuple $(\text{act}, (\mathcal{R}^i)_{i \in I}, \mathcal{A})$, on the one hand, that includes automata $\mathcal{R}^i$ and $\mathcal{A}$
describing the indistinguishability relations and the objective, and its presentation as a logical
structure $\mathcal{G} = (\Gamma^*, \text{act}, (\sim^i)_{i \in I}, \lambda)$, on the other hand, with $\sim^i = L(\mathcal{R}^i)$ and $\lambda = \lambda^A$.
## 3.2 Full-Information Protocols

We formalise a communication model that gives rise to a particular class of finitely-representable information structures for repeated games. Our formalisation and the application scenario are inspired from [21].

In full-information protocols, players receive local observations from a finite set $B^i$ via an observation function $\beta^i$, as they do in partial-observation games, but additionally they communicate with other players. The information transfer in that event is idealistically efficient: the entire information available to the sending party is revealed to the receiving player. However, the opportunity of communication may not be under the control of the players: whether a communication event occurs in a particular stage, and which player it includes, is determined by the current move.

Communication opportunities for a player $i \in I$ are specified by a function $com^i: B^i \to \wp(I)$ that associates with each of her local observation $b \in B^i$, a set of players $com^i(b^i) \subseteq I$ to which communication links are enabled. Intuitively, when Player $i$ receives the local observation $b^i \in B^i$, she also receives the information of every player $j \in com^i(b^i)$, which includes his observation history $b_1^j, b_2^j, \dots, b_\ell^j$, but also (recursively) the observation history of all players in $com^j(b_t^j)$ at previous stages $t = 1, 2, \dots, \ell$. Thus, a link $j \in com^i(b^i)$ specifies a one-way communication event from sender $j$ to receiver $i$: upon observing $b^i$, Player $i$ can peek at Player $j$. We refer to such links as direct links. Our semantics of communication links is transitive. If at some history, there is a direct link from Player $i$ to Player $j$, and also a direct link from Player $j$ to Player $k$, then an indirect communication link is established from Player $i$ to Player $k$. Even if the protocol specifies no direct link from $i$ to $k$, the information of $k$ is revealed to $i$.

Formally, we represent the information available to the players at a history $\tau = c_1c_2\dots c_\ell$ by a view graph View($\tau$) = $(V, E)$, defined as follows:

- $V = I \times \{0, 1, \dots, \ell\}$ is the set of nodes, and a node $(i, t) \in V$ represents the viewpoint of Player $i$ in stage $t$;

- $E \subseteq V \times V$ is the set of edges, where an edge $((i,t), (j,u))$ intuitively means that in stage $t$, Player $i$ has access to the view of Player $j$ in stage $u$; the set $E$ contains the edges $((i,t), (i, t-1))$ for all stages $1 < t \le \ell$ and every player $i$ - which correspond to looking into the past, and the edges $((i,t), (j,t))$ are included, for all stages $1 \le t \le \ell$ and all players $i \in I$ and $j \in com^i(b^i)$ where $b = \beta^i(c_1c_2\dots c_t)$ - which correspond to revealing the current view of Player $j$ to Player $i$ (via a direct link).

Two histories $\tau, \tau' \in \Gamma^*$ are indistinguishable for Player $i$, denoted $\tau \sim^i \tau'$, if they have the same length $\ell$ and the local observations $\beta^j(\tau(t)) = \beta^j(\tau'(t))$ agree, for all nodes $(j,t)$ reachable from $(i, \ell)$ in the view graph View($\tau$). In particular, this means that from $(i, \ell)$ the same set of nodes is reachable in View($\tau$) and in View($\tau'$). We say that the histories $\tau, \tau'$ are indistinguishable for a coalition $J \subseteq I$, denoted $\tau \sim^J \tau'$, if they are indistinguishable for all players of the coalition, that is, $\tau \sim^i \tau'$ for all $i \in J$.

A full-information protocol (FIP) for a set of players $I$, a move alphabet $\Gamma$, and an alphabet $B$ of observation profiles, is described by a profile $F = (\mathcal{M}^i, com^i)_{i \in I}$ specifying for each player $i \in I$, a Mealy automaton $\mathcal{M}^i$ that defines the local observation function $\beta^i: \Gamma^* \to B^i$ and the communication map $com^i: B^i \to \wp(I)$ that specifies, for every local observation, the set of players to which a communication link from $i$ is enabled. The protocol $F$ defines an indistinguishability relation, for each player $i \in I$, which we denote by $\sim_F^i$.

To turn a FIP instance $F = (\mathcal{M}^i, com^i)_{i \in I}$ into a game, consider now a profile $A$ of action sets $A^i$ for the players $i \in I$ together with a suitable action map act: $\Gamma \to A$. The actions of any player $i$ should be observable to himself: if $act^i(c) \neq act^i(c')$, then $\beta^i(\tau c) \neq \beta^i(\tau' c')$,
for all histories $\tau, \tau' \in \Gamma^*$ and moves $c, c' \in \Gamma$. If the condition is satisfied, then $F$ induces a profile of indistinguishability relations for the repeated game form described by act. Together with the action map $act$ and a parity automaton $\mathcal{A}$ for defining the objective, we thus obtain the repeated game $\mathcal{G}(F) := (\Gamma^*, act, (\sim_F^i)_{i \in I}, \lambda^A)$, which we call the *FIP game* associated with $F$.

## 3.3 Example: Leader election with failures and recoveries

To illustrate the model, consider a classical leader election scenario. A set $V = \{0, \dots, n\}$ of processes is connected in a network graph $(V, E)$, where each edge $(i, j) \in E$ represents a unidirectional channel through which process $i$ can send messages to process $j$. The system runs indefinitely in synchronous rounds.

In each round $t \in \mathbb{N}$, every process $i$ declares a leader candidate $a_t^i \in V$ and proposes a message $m_t^i$ for broadcasting to its neighbours $j \in iE$. The environment may crash a subset $F_t \subseteq E$ of channels, so that process $i$ receives messages only from $j \in (E \setminus F_t)i$. In the next round, some channels may recover while others may fail. A process $i$ is said to fail at time $t$ if any of its outgoing channels crash. Failures are bounded by parameters $(N, L)$: at most $N$ channels may crash in any window of $L$ rounds. A process is valid at time $t$ if it does not fail.

The objective of leader election is to ensure that, unless all processes fail repeatedly, there is a time $t_0$ after which all valid processes $i$ agree on a leader $a_t^i = k$ who is also valid.

Note that we did not specify the message space. This is intentional: in practice, it is often difficult to settle on the structure of internal messages for distributed algorithms that are yet to be designed. To maintain focus on external behaviour, we instead assume that processes broadcast all available information whenever communication is possible – in other words, they follow a full-information protocol. Once a solution is found for this idealised setting, it may later be implemented more efficiently. It might turn out that the problem is unsolvable even under full information, hence no effective protocol exists either.

Process implementation must answer two questions: (1) How to choose a leader based on the observed failure history; (2) What to transmit. The full-information assumption focuses on the first question, assuming the second is solved or deferred.

We model this as a FIP game with players in $I = V \cup E$. Each process player $i \in V$ has actions $A^i = I$, representing candidates, whereas channel players are passive, with $|A^e| = 1$, for all $e \in E$. Moves are tuples $(a, F)$ of declarations and crash sets, with $\Gamma = \prod_{i \in V} V \times \wp(E)$ and $act(a, F) = a$.

Local observations, for each process player $i$, specify the subset of channels from which it can read, i.e., $B^i \subseteq \{(j, i) \in E\}$, and the communication function $com^i$ is the identity. Including the channels as observers is an artifice to prevent players from seeing the entire network, since we choose a semantics where communication is transitive. Accordingly, each channel $(i, j)$ has two observations: $\{\text{read}, \text{lock}\}$ with $com^{(i,j)}(\text{read}) = \{i\}$ – when the source process is revealed – and $com^{(i,j)}(\text{lock}) = \emptyset$ – when it may reveal to the target. The observation automata for channels alternate between read at odd times and lock at even times. For processes, the observation automaton of $i$ sends the $\emptyset$ observation at odd times, whereas it reveals the enabled incoming channels from $E \setminus F$ at even times. The Mealy automaton is further adjusted to keep track of the number of crashes within the time window. To ensure that the bounds $(N, L)$ are respected, the automata send $\emptyset$ when the budget does not allow to crash the subset $F$ recorded in the current move.

The objective is described by a parity automaton with three priorities: 2 when all valid processes agree on a valid leader; 1 when there is disagreement or the leader is invalid; 0 after a phase in which all processes failed. It rejects plays that visit priority 1 infinitely often.
13:8 Synthesising Full-Information Protocols

Now we can verify that the model faithfully captures our scenario: any distributed
protocol – regardless of which messages the processes pass – corresponds to a strategy profile.
It solves the leader election problem under the given bounds if, and only if, the strategy is
winning in the FIP game.

4 The Synthesis Problem

We study the following synthesis problem: Given a finite FIP game instance $\mathcal{F} =$
(ac t, $(\mathcal{M}^i, \text{com}^i)_{i \in I}, \mathcal{A}$), decide whether there exists a winning strategy in the repeated
game $\mathcal{G}(\mathcal{F})$ and, if so, effectively construct one.

Graph games are special cases of FIP games. For instance, a perfect-information game on a graph $(V, v_\epsilon, (E_a)_{a \in A}, \lambda)$ corresponds to the repeated game (act, id, $\mathcal{M}$) with $\Gamma = A \times V$, where $\text{act}(a, v) = a$ and $\mathcal{M}$ maps a history $\tau = (a_1, v_1) \dots (a_t, v_t)$ to $\lambda(v_t)$ if $\tau$ follows a path from $v_\epsilon$, and to a fresh colour $\perp$ otherwise. Given an objective $L \subseteq C^\omega$, a play is winning in the repeated game, if $\mathcal{M}$ maps it to a sequence in $L$ or to one reaching $\perp$.

Partial-observation games translate similarly by expressing observation functions as Mealy automata that output observation labels on transitions. Standard partial-observation games [26] correspond precisely to FIP games with one player. In such repeated games, the indistinguishability relation $\sim$ is defined by a regular observation function $\beta : \Gamma^* \to B$, such that $\tau \sim \tau'$ if $\hat{\beta}(\tau) = \hat{\beta}(\tau')$. Assuming perfect recall, $\tau c \sim \tau' c'$ iff $\tau \sim \tau'$ and $\beta(\tau c) = \beta(\tau' c')$. Accordingly, every information set $U$ has at most $|B|$ successors, so the information tree has bounded branching.

For two or more players, FIP games yield strictly richer information structures. Consider a FIP game with players $I = \{0, 1\}$, binary observations, and a communication map where Player 0 can communicate with Player 1 only on observation 1. Suppose Player 0 observes 0 for 7 stages, while Player 1 observes an arbitrary bit sequence. In stage 8, Player 0 observes 1, revealing all 8 bits seen by Player 1. Thus, her current information set, with $2^7$ histories, has $2^8$ successors (that are singletons). If the play continues in the same way, until the next communication event occurs, say in stage 88, there will be a branching of degree $2^{80}$, and so on. Hence, FIP information trees may have unbounded branching.

Restriction to one active player, visible objectives

Since synthesis is undecidable already for two players in partial-observation games, we restrict
our analysis to one active player. Accordingly, we consider games with a set of players
$I = \{0, \dots, n\}$, where Player 0 is active and the others are passive observers ($|A^i| = 1$ for
$i \neq 0$). References to actions or indistinguishability relations refer to Player 0 unless specified.

We further restrict to *visible objectives*, where the colouring function $\lambda^A$ defined by the
objective automaton $\mathcal{A}$ is information consistent: $\lambda^A(\tau) = \lambda^A(\tau')$ whenever $\tau \sim^0 \tau'$.

Despite these restrictions, the model captures significant system-design problems. One
motivation is monitoring and diagnosis: constructing a decentralised supervisor that runs
alongside a fixed distributed system – using the given communication architecture – to
log data and detect faults. The active player outputs new data according to the specified
objective, leaving the system unchanged.

An active player added to a fixed distributed protocol can influence the system meaning-
fully. For example, in leader election, we may let one process repair channels in addition to
its original role, with the objective to ensure stability, that is, that leaders are revoked only
if they fail. Formally this is done by extending Player 0’s action set to $A^0 \times E$, and adapting
the action map to exclude the repaired channel from the crash set of the stage outcome. The
synthesis objective is stability in conjunction with the condition that passive players follow the actions prescribed by the original protocol. Under standard connectivity assumptions (already necessary to solve basic leader election), this can be specified by a visible automaton.

## 4.1 Method

In the rest of the paper, we show that the synthesis problem for FIP games with one active player is computationally solvable, albeit with daunting theoretical complexity.

The key tool for synthesis in infinite games is the automata-theoretic approach, founded by Büchi and Landweber [7] and Rabin [24, 25]. Strategies are viewed as trees with bounded branching. However, FIP games may yield unbounded information trees. Indeed, [4] shows that a regular indistinguishability relation defines a tree of finite branching degree if, and only if, it corresponds to an observation function. The counterexample there is a FIP protocol with one active player and one passive observer. Thus, we cannot rely on tree automata to recognise the set of winning strategies of a FIP game.

To overcome this obstacle, we reduce a finite FIP game (with parity objectives) to a perfect-information graph game, preserving winning strategies: (1) if a winning strategy exists in the original game, one exists in the reduct; (2) from a regular strategy in the reduct, we can construct one for the original.

The reduction builds effectively a homomorphism from histories $\Gamma^*$ to a finite set of abstract states, preserving information sets. By collapsing the abstract states of an information set, we obtain a finite perfect-information game equivalent (bisimilar) to the original. This allows pulling back winning strategies.

### Information quotient

A repeated game with imperfect information and one active player can be represented as a game with perfect information played on the information tree – the infinite graph with information sets as positions.

Let us fix a move alphabet $\Gamma$ and a set $A$ of actions. The information quotient of a game $\mathcal{G} = (\Gamma^*, \text{act}, \sim, \lambda)$ is the graph $\mathcal{U}(\mathcal{G})$ on $U = \{[\tau]_{\sim} | \tau \in \Gamma^*\}$, with initial node $u_{\varepsilon} = [\varepsilon]_{\sim}$, edges:

$$E_a^{\mathcal{U}} := \{([\tau]_{\sim}, [\tau c]_{\sim}) | \text{act}(c) = a\}, \quad \text{for each } a \in A,$$

and colouring $\lambda^{\mathcal{U}}([\tau]_{\sim}) = \lambda(\tau)$. As $\sim$ has perfect recall, $\mathcal{U}(\mathcal{G})$ is a tree. Therefore, each node $u \in U$ identifies a unique path from $u_{\varepsilon}$, and we view strategies as functions $s: U \to A$.

Although structurally different, a game with imperfect information and the perfect-information game played on its information tree are the same (from the perspective of the active player), in the following sense.

**Lemma 1.** For every game $\mathcal{G}$ with indistinguishability relation $\sim$, there is a one-to-one correspondence mapping each strategy $s$ in $\mathcal{U}(\mathcal{G})$ to a strategy $\tilde{s}$ in $\mathcal{G}$, such that $\tilde{s}(\tau) = s([\tau]_{\sim})$, and their outcomes agree on colours: $\tilde{\lambda}(\text{Out}(\tilde{s})) = \tilde{\lambda}^{\mathcal{U}}(\text{Out}(s))$.

### Bisimulation

Further, we use bisimulation to relate strategies across games.

Let $\mathcal{G}, \mathcal{H}$ be perfect-information game graphs with the same vocabulary $(v_{\varepsilon}, (E_a)_{a \in A}, \lambda)$. A bisimulation between $\mathcal{G}$ and $\mathcal{H}$ is a relation $Z \subseteq V^{\mathcal{G}} \times V^{\mathcal{H}}$ such that every related pair of nodes $(u, v) \in Z$ agree on the colour $\lambda^{\mathcal{G}}(u) = \lambda^{\mathcal{H}}(v)$ and
13:10 Synthesising Full-Information Protocols

(Zig) for each $a \in A$ and $(u, u') \in E_a^G$, there is $(v, v') \in E_a^H$ with $(u', v') \in Z$;

(Zag) for each $a \in A$ and $(v, v') \in E_a^H$, there is $(u, u') \in E_a^G$ with $(u', v') \in Z$.

The graphs $G, \mathcal{H}$ are *bisimilar* if their initial states are related: $(v_{\varepsilon}^{G}, v_{\varepsilon}^{\mathcal{H}}) \in Z$.

A graph homomorphism from $G$ to $\mathcal{H}$ is a function $h: V^G \to V^{\mathcal{H}}$ that preserves the initial state: $h(v_{\varepsilon}^G) = v_{\varepsilon}^{\mathcal{H}}$, the edges: $h(E_a^G) \subseteq E_a^{\mathcal{H}}$ for all $a \in A$, and the colouring: $\lambda^G = \lambda^{\mathcal{H}} \circ h$. A $p$-morphism is a homomorphism $h: G \to \mathcal{H}$ such that the relation $\{(x, h(x)) \mid x \in V^G\}$ forms a bisimulation. Equivalently, $h$ is a homomorphism and, for every edge $(v, w) \in E_a^{\mathcal{H}}$ and node $x \in V^G$ with $h(x) = v$, there exists an edge $(x, y) \in E_a^G$ such that $h(y) = w$ [15, 27].

**► Lemma 2 ([12]).** Let $G$ and $\mathcal{H}$ be bisimilar game graphs. Then, $G$ has a winning strategy iff $\mathcal{H}$ has one. Moreover, if there exists a $p$-morphism $h: G \to \mathcal{H}$, then it takes every strategy $s$ in $\mathcal{H}$, to a strategy $s \circ h$ in $G$ such that the outcomes agree on colours: $\hat{\lambda}^G(\mathrm{Out}(s \circ h)) = \hat{\lambda}^{\mathcal{H}}(\mathrm{Out}(s))$.

5 The Reduction

For this section, let us fix a set $I = \{0, \dots, n\}$ of players with 0 being the active player, with an action set $A$, and the others being passive observers.

5.1 Simplifications

To simplify the presentation, we assume that all players in $I$ share a common observation
alphabet $B$. Moreover, we identify moves with observation profiles: $\Gamma = \coprod_{i \in I} B$. Each
player's observation function is defined trivially by $\beta^i(\tau c) = c^i$ for all $\tau \in \Gamma^*$ and $c \in \Gamma$.

These assumptions can be made without loss of generality. Any FIP instance can be
brought to this form by adding a dummy observer and modifying the objective to check
that the observations in the view of the active players match the original Mealy-automaton
outputs, or else go to a sink state labelled with an even priority. This modification incurs an
exponential blowup in size, but preserves visibility of the objective.

In the simplified model, we can characterise indistinguishability relations without reference to view graphs. Given a move $c \in \Gamma$, let $\mathrm{Link}(c) := \bigcup_{i \in I} \{i\} \times \mathrm{com}^i(c^i)$ denote the set of all communication links enabled under $c$. For any player $i \in I$, let now $\mathrm{sync}^i(c)$ be the set of players reachable from $i$ via the reflexive-transitive closure of $\mathrm{Link}(c)$. Hence, $\mathrm{sync}^i(c)$ describes the set of players that communicate (directly or indirectly) with Player $i$ under move $c$. For a coalition $J \subseteq I$, let $\mathrm{sync}^J(c) := \bigcup_{i \in J} \mathrm{sync}^i(c)$.

We note the following properties for later use: sync<sup>J</sup>(c) always includes J, every coalition L = sync<sup>J</sup>(c) that occurs as a synchronisation target is autonomous, meaning L = sync<sup>L</sup>(c), intermediary coalitions J ⊆ K ⊆ sync<sup>J</sup>(c) share the same target: sync<sup>K</sup>(c) = sync<sup>J</sup>(c), and sync<sup>J∪K</sup>(c) = sync<sup>J</sup>(c) ∪ sync<sup>K</sup>(c).

The following lemma describes how the information sets of a coalition evolve with a move.

**► Lemma 3.** Let $J \subseteq I$ be a coalition. Then, for all histories $\tau \in \Gamma^*$ and all moves $c \in \Gamma$:

(i) For the target coalition $L = \text{sync}^J(c)$, we have $[\tau c]_{\sim L} = \{\tau' d \mid \tau' \sim L \tau \text{ and } d^L = c^L\}$.

(ii) For every intermediary coalition $K$ with $J \subseteq K \subseteq \text{sync}^J(c)$, we have $[\tau c]_{\sim K} = [\tau c]_{\sim J}$.

Lemma 3 provides an inductive definition of indistinguishability in simplified FIP games: $[\tau c]_{\sim J} = [\tau c]_{\sim L} = \{\tau' d \mid \tau' \in [\tau]_{\sim L} \text{ and } d^L = c^L\}$, for $L = \text{sync}^J(c)$. Recall that, for the grand coalition, $\sim^I$ is the identity.
## 5.2 Abstraction morphism

As a first step towards our reduction, we map each history $\tau \in \Gamma^*$ to an abstract state from a finite domain. This state encodes the knowledge of every coalition containing the active player 0. For a coalition $J \subseteq I$, its own knowledge is information-consistent, hence visible; whereas knowledge of strictly larger coalitions $K \supsetneq J$ might not be information-consistent for coalition $J$ – these values form a hidden part of the abstract state, called the configuration.

Knowledge is represented by a set of configurations, and configurations are profiles of knowledge sets indexed by coalitions. For the grand coalition, the configuration is just the state of the objective automaton.

For any $J \subseteq I$, let $J^\uparrow := \{K \subseteq I \mid J \subseteq K\}$ be the set of coalitions containing $J$, and $J^\downarrow := J^\uparrow \setminus \{J\}$. We call any $J \in \{0\}^\uparrow$ an active coalition.

Let $\mathcal{F} = (\text{act}, (\text{sync}^J)_{J \in \{0\}^\uparrow}, \mathcal{A})$ be a FIP game in simplified form, with local observation alphabet $\mathcal{B}$, moves $\Gamma$, action map act: $\Gamma \to \mathcal{A}$, a profile of synchronisation maps sync$^J$: $\Gamma \to \wp(I)$, one for every active coalition $J$, and a Mealy automaton $\mathcal{A}$ defining the objective. We refer to the corresponding one-player game as $\mathcal{G} := (\Gamma^*, \text{act}, \sim, \lambda^A)$.

For each $J \in \{0\}^\uparrow$ and history $\tau \in \Gamma^*$, we define the configuration $\varphi_J(\tau)$ and the knowledge set $\Phi^J(\tau)$ by mutual induction:

- $\varphi_I(\tau) := \delta^A(q_\epsilon, \tau)$,

- $\varphi_J(\tau) := (\Phi^K(\tau))_{K \in J^\uparrow}$ for $J \neq I$,

- $\Phi^J(\tau) := \{\varphi_J(\tau') \mid \tau' \sim^J \tau\}$.

Finally, the abstract state for coalition $J$ is $h_J(\tau) := (\Phi^J(\tau), \varphi_J(\tau))$. We write $\text{Conf}_J$ and $\text{KSet}^J$ for the ranges of $\varphi_J$ and $\Phi^J$, respectively. These sets are finite, as $\text{Conf}_I = \mathcal{Q}$ and $\text{Conf}_J \subseteq \prod_{K \in J^\uparrow} \text{KSet}^K$, whereas $\text{KSet}^J \subseteq \wp(\text{Conf}_J)$. The set of abstract states is $\mathcal{Q}^H_J \subseteq \text{KSet}^J \times \text{Conf}_J$. We omit indices for $J = \{0\}$ and write $h = h_{\{0\}}$.

Note that in any $(\Psi, \psi) \in \mathcal{Q}^H_J$, we have $\psi \in \Psi$. Also, the knowledge-set component of $h_J$ is information-consistent by construction.

**Lemma 4 (Preservation of indistinguishability).** If $\tau \sim^J \tau'$, then $\Phi^J(\tau) = \Phi^J(\tau')$, for all histories $\tau, \tau' \in \Gamma^*$ and all active coalitions $J \in \{0\}^\uparrow$.

In particular, this holds for the active player singleton $J = \{0\}$, hence $\sim \subseteq \ker \Phi^{\{0\}}$. The abstraction map also respects the colour assigned by the objective automaton.

**Lemma 5 (Preservation of objective colouring).** If $h_J(\tau) = h_J(\tau')$, then $\lambda(\tau) = \lambda(\tau')$, for all histories $\tau, \tau'$ and active coalitions $J$.

**Proof.** The statement is immediate for $J = I$, since $\varphi_I(\tau) = \varphi_I(\tau')$ is a state $q$, so $h_I(\tau) = h_I(\tau') = (\{q\}, q)$ and $\lambda(\tau) = \lambda(\tau') = \lambda(q)$. Otherwise, if $J^\uparrow$ is nonempty and $h_J(\tau) = h_J(\tau')$, then $\Phi^K(\tau) = \Phi^K(\tau')$ for all $K \in J^\uparrow$, in particular $\Phi^I(\tau) = \Phi^I(\tau') = \{q\}$, and again $\lambda(\tau) = \lambda(\tau') = \lambda(q)$. $\blacksquare$

Accordingly, we can map abstract states to colours via $\lambda^H(\Phi, \varphi) := \lambda(\tau)$ for any history $\tau \in \Gamma^*$ such that $h(\tau) = (\Phi, \varphi)$.

An elementary, but important insight is that the abstract state of a history determines the set of abstract states of its information set.

**Lemma 6 (Information commuting).** If $h_J(\tau) = h_J(\tau')$ then $h_J([\tau]_{\sim^J}) = h_J([\tau']_{\sim^J})$, for all histories $\tau, \tau'$ and active coalitions $J$.
13:12 Synthesising Full-Information Protocols

**Proof.** Any histories $\tau, \tau'$ with the same image under $h_J$ share $\Phi^J(\tau) = \Phi^J(\tau') =: \Psi$, so their information sets map to:

$$ \begin{aligned} h[\tau]_{\sim J} &= \{(\Phi^J(\pi), \varphi) \mid \varphi \in \Phi^J(\tau)\} = \{(\Psi, \varphi) \mid \varphi \in \Psi\} \\ &= \{(\Phi^J(\tau'), \varphi) \mid \varphi \in \Phi^J(\tau')\} = h[\tau]_{\sim J}. \end{aligned} \quad \blacksquare $$

Regularity

To show that the abstraction map $h$ can be constructed effectively, we prove that it is a homomorphism on the repeated game $\mathcal{G}$, as it preserves the move operations: for every pair of histories $\tau, \tau' \in \Gamma^*$, and every $c \in \Gamma$, if $h(\tau) = h(\tau')$, then $h(\tau c) = h(\tau'c)$. Towards this, we define operations on abstract states that mimic the information updates triggered either by local observations or by communication.

Intuitively, when a coalition $J$ communicates with coalition $L$, it is as if $J$ communicates with $J \cup L$. Therefore, we focus on communication between coalitions that are comparable with respect to inclusion. We define, for every increasing pair of active coalitions $J \subseteq L$, a lifting operator $\lceil \cdot \rceil_L^J: KSet^L \to KSet^J$ that maps every knowledge set $\Phi$ for $L$ to a knowledge set $\lceil \Phi \rceil_L^J$ for $J$, by setting $\lceil \Phi \rceil_J^J := \Phi$ and

$$ \lceil \Phi \rceil_L^J := \{ \lceil \Phi, \varphi \rceil_L^J \mid \varphi \in \Phi \}, \quad \text{for all } L \in J^\dagger. $$

The construction uses an auxiliary operator that maps every abstract state $(\Phi^L, \varphi_L) \in KSet^L \times \text{Conf}_L$ for the larger coalition $L$ to a configuration $\lceil \Phi, \varphi \rceil_L^J \in \text{Conf}^J$ for the smaller $J$:

$$ \lceil \Phi, \varphi \rceil_L^J := (\Psi^K)_{K \in J^\dagger} \quad \text{with} \quad \Psi^K := \begin{cases} \lceil \Phi \rceil_L^K & \text{if } K \subseteq L; \\ \lceil \varphi^{K \cup L} \rceil_{K \cup L}^K & \text{otherwise.} \end{cases} $$

By unfolding the definition, we can see that the operators compose naturally.

**Lemma 7 (Composition of lifting).** For all increasing coalitions $J \subseteq K \subseteq L$,

$$ \lceil \lceil \Phi \rceil_L^K \rceil_K = \lceil \Phi \rceil_L^J, \quad \text{for every knowledge set } \Psi \in KSet^J. $$

The following lemma states that the operator indeed captures that the information of a coalition $L$ is revealed to smaller (hence, possibly less informed) coalition $J$.

**Lemma 8 (Communication).** For coalition $J$ and a move $c \in \Gamma$, consider the target coalition $L = \text{sync}^J(c)$. Then, $\lceil \Phi^L(\tau c) \rceil_L^J = \Phi^J(\tau c)$, for every history $\tau \in \Gamma^*$.

**Proof.** We proceed by induction starting with the grand coalition. As $\text{sync}^I(d) = I$, the base case is trivial. For the induction step, suppose that the statement holds for all coalitions strictly larger than $J$. By unfolding the definitions, we obtain:

$$ \begin{aligned} \lceil \Phi^L(\tau c) \rceil_L^J &= \{(\lceil \Phi^L(\tau c), \varphi \rceil_L^K)_{K \in J^\dagger} \mid \varphi \in \Phi^L(\tau c)\} && (\text{Set lifting, configuration}) \\ &= \{(\lceil \Phi^L(\tau'd), \varphi_L(\tau'd) \rceil_L^K)_{K \in J^\dagger} \mid \tau'd \sim^L \tau c\} && (\text{Lemma 3(i), Lemma 4}) \\ &= \{(\lceil \Phi^{L \cup K}(\tau'd) \rceil_{L \cup K}^K)_{K \in J^\dagger} \mid \tau'd \sim^L \tau c\}. && (\text{Abstract-state lifting}) \end{aligned} $$

Observe that for every $K \in J^\dagger$, we have $\text{sync}^K(d) = \text{sync}^{J \cup K}(d) = \text{sync}^J(d) \cup \text{sync}^K(d) = L \cup \text{sync}^K(d)$. On the other hand $\text{sync}^{L \cup K}(d) = \text{sync}^L(d) \cup \text{sync}^K(d) = L \cup \text{sync}^K(d)$. Hence, the coalitions $L \cup K$ and $K$ share the same target $T := \text{sync}^{L \cup K}(d) = \text{sync}^K(d)$, strictly larger than $J$. Therefore, we can develop the knowledge sets in the last expression as follows:
$$ \begin{align*} \lceil \Phi^{L \cup K}(\tau'd) \rceil_{L \cup K}^K &= \lceil \lceil \Phi^T(\tau'd) \rceil_{T}^{L \cup K} \rceil_{L \cup K}^K && \text{(Induction hypothesis for sync}^{K \cup L}(d) = T) \\ &= \lceil \Phi^T(\tau'd) \rceil_{T}^{K} && \text{(Lemma 7)} \\ &= \Phi^K(\tau'd) && \text{(Induction hypothesis for sync}^K(d) = T). \end{align*} $$

In conclusion, $\lceil \Phi^L(\tau c) \rceil_L^J = \{\varphi_J(\tau'd) \mid \tau'd \sim^L \tau c\} = \{\varphi_J(\tau'd) \mid \tau'd \sim^J \tau c\} = \Phi^J(\tau c)$, according to Lemma 3(ii). ◀

With the lifting operators in place, we define update operations on configurations, knowledge sets, and ultimately on abstract states, for each active coalition.

For configurations, define $succ_J: \text{Conf}_J \times \Gamma \to \text{Conf}_J$ as follows. For the grand coalition, this coincides with the automaton update: $succ_I(\varphi, c) := \delta^A(\varphi, c)$. For other coalitions $J$, the update is componentwise, based on synchronisation targets:

$$ \text{succ}_J(\varphi, c) := (\text{Succ}^K(\varphi^{\text{sync}^K(c)}))_{K \in J^\dagger}. $$

Knowledge sets are updated by a partial function $\text{Succ}^J: \text{KSet} \times \Gamma \to \text{KSet}^J$, defined on pairs $(\Phi, c)$ with $\Phi \in \text{KSet}^L$ and $L = \text{sync}^J(c)$:

■ If $J$ is autonomous ($J = L$), set

$$ \text{succ}^J(\Phi, c) := \{\text{succ}_J(\psi, d) \mid \psi \in \Phi, d^L = c^L\}, $$

■ Otherwise, for $L \neq J$, define

$$ \text{succ}^J(\Phi, c) := \lceil \text{succ}^L(\Phi, c) \rceil_L^J. $$

The state update $\delta_J^H: Q_J^H \to Q_J^H$ is defined as:

■ If $J$ is autonomous, then

$$ \delta_J^H((\Phi, \varphi), c) = (\text{succ}^J(\Phi, c), \text{succ}_J(\varphi, c)), $$

■ Otherwise, letting $L = \text{sync}^J(c)$, set

$$ \delta_J^H((\Phi, \varphi), c) := (\text{succ}^J(\varphi^L, c), \text{succ}_J(\varphi, c)). $$

► **Lemma 9 (Preservation of moves).** Let $J$ be an active coalition. Then,

$$ h_J(\tau c) = \delta_J^H(h(\tau), c), \quad \text{for all } \tau \in \Gamma^*, c \in \Gamma. $$

**Proof.** We detail the inductive argument for knowledge sets to show that for $L = \text{sync}^J(c)$,

$$ \text{succ}^J(\Phi^L(\tau), c) = \Phi^J(\tau c). $$

The base case, with $I = \text{sync}^I(c)$, concerns moves in the objective automata:

$$ \begin{align*} \text{succ}^I(\Phi^I(\tau), c) &= \{\text{succ}_I(\varphi, d) \mid \varphi \in \Phi^I(\tau), c^I = d^I\} \\ &= \{\delta(\delta(q_\varepsilon, \tau), c)\} = \{\delta(q_\varepsilon, \tau c)\} = \text{succ}^I(\tau c). \end{align*} $$

Inductive step: if $J$ is autonomous,

$$ \begin{align*} \text{succ}^J(\Phi^J(\tau), c) &= \{\text{succ}_J(\varphi, d) \mid \varphi \in \Phi^J(\tau), d^J = c^J\} && \text{(Definition of $\text{succ}^J$)} \\ &= \{\text{succ}_J(\varphi_J(\tau'), d) \mid \tau' \sim^J \tau, d^J = c^J\} && \text{(Knowledge set $\Phi^J$)} \\ &= \{(\text{succ}^K(\Phi^{\text{sync}^K(d)}(\tau'), d))_{K \in J^\dagger} \mid \tau'd \sim^J \tau c\} && \text{(Lemma 3(i))} \\ &= \{(\Phi^K(\tau'd))_{K \in J^\dagger} \mid \tau'd \sim^J \tau c\} = \Phi^J(\tau c) && \text{(Induction hypothesis).} \end{align*} $$
13:14 Synthesising Full-Information Protocols

Otherwise, if $J \neq L := \text{sync}^J(c)$:

$$
\begin{align*}
\text{Succ}^J(\Phi^L(\tau), c) &= \lceil \text{Succ}^L(\Phi^L(\tau), c) \rceil_L^J && \text{(Definition of Succ}^J) \\
&= \lceil \Phi^L(\tau c) \rceil_L^J = \Phi^J(\tau c). && \text{(Induction hypothesis, Lemma 8)}
\end{align*}
$$

The statement extends to configurations and abstract states by structural induction. ◀

With these ingredients in hand, let us define the automaton $\mathcal{H} = (Q^{\mathcal{H}}, \Gamma, Q^{\mathcal{H}}, \delta^{\mathcal{H}}, q_{\varepsilon}^{\mathcal{H}}, \delta^{\mathcal{H}})$ on the set $Q^{\mathcal{H}}$ of abstract states – also used as output alphabet –, with input alphabet $\Gamma$, transition function $\delta_0^{\mathcal{H}}$, initial state $q_{\varepsilon}^{\mathcal{H}} := h(\varepsilon)$ and an output function that returns the current state $\lambda^{\mathcal{H}} = \delta^{\mathcal{H}}$. This Mealy automaton $\mathcal{H}$ defines $h$. By projecting the output on its first component, we obtain, for every input history $\tau$, the knowledge set $\Phi^{\{0\}}(\tau)$. In conclusion, the functions $h$ and $\Phi^{\{0\}}$ are regular.

5.3 Knowledge Quotient

Now, we construct a new game from the automaton $\mathcal{H}$ by collapsing abstract states that
share the same knowledge set. Concretely, we define the perfect-information game graph
$\mathcal{K} = (Q^{\mathcal{K}}, (E_a^{\mathcal{K}})_{a \in A}, q_{\varepsilon}^{\mathcal{K}}, \lambda^{\mathcal{K}})$ with the following ingredients. The set of positions consists of
knowledge sets: $Q^{\mathcal{K}} := \text{KSet}^0 = \Phi^{\{0\}}(\Gamma^*)$. For every action $a \in A$, the set $E_a$ contains the
edge from $\Phi$ to $\Phi'$ if there exist abstract states $(\Phi, \varphi)$ and $(\Phi', \varphi')$ in $Q^{\mathcal{H}}$ and a move $c \in \Gamma$
such that $\delta^{\mathcal{H}}((\Phi, \varphi), c) = (\Phi', \varphi')$. The initial position is obtained from the initial abstract
state $q_{\varepsilon}^{\mathcal{H}} = (\Phi_{\varepsilon}, \varphi_{\varepsilon})$ by taking the first component $q_{\varepsilon}^{\mathcal{K}} := \Phi_{\varepsilon}$. As the objective colouring $\lambda^{\mathcal{A}}$
and the knowledge-set map $\Phi^{\{0\}}$ are both information consistent, we can lift the colouring
from the configuration component of the states in $Q^{\mathcal{H}}$ defined in Lemma 5 to the knowledge
set in their knowledge-set component: for any $\Phi \in Q^{\mathcal{K}}$, we assign $\lambda^{\mathcal{K}}(\Phi) := \lambda^{\mathcal{H}}(\Phi, \varphi)$ for
some/any abstract state $(\Phi, \varphi) \in Q^{\mathcal{H}}$ with $\Phi$ in the first component.

The same game graph can be obtained directly from the original repeated game by taking
the quotient $\Gamma_{/ker \Phi}$. Indeed, $Q^{\mathcal{K}} = \Phi^0(\Gamma^*)$, $E_a = \{(\Phi^0(\tau), \Phi^0(\tau c)) \mid \tau \in \Gamma^*, c \in \Gamma\}$ for all
$a \in A$, $q^{\varepsilon} = \Phi^0(\varepsilon)$, and $\lambda^{\mathcal{K}}(\Phi^0(\tau)) = \lambda(\tau)$, for all histories $\tau \in \Gamma^*$.

Let $k: \Gamma^* \to \text{KSet}^0$ be the quotienting map that associates to every history its knowledge set: $k(\tau) := \Phi^{\{0\}}(\tau)$. Since $k$ is information consistent with respect to $\sim$, it induces a map $\bar{k}: \Gamma^*/\sim \to \text{KSet}^0$ with $\bar{k}([\tau]) = k(\tau) = \Phi^0(\tau)$. The map $\bar{k}$ is actually a graph homomorphism from the information quotient $\mathcal{U}(\mathcal{G}) = \mathcal{G}^*/\sim$ of the original game to $\mathcal{K} = k(\mathcal{G})$, as it preserves edges, actions and the colouring $\lambda$.

As an immediate consequence of Lemma 6, the factor map describes a functional bisimu-
lation.

► **Lemma 10 (p-morphism).** For every history $\tau c \in \Gamma^*$, and every $\tau' \in \Gamma^*$ with $k(\tau') = k(\tau)$, there exists a history $\tau'' \sim \tau'$ such that $k(\tau''c) = k(\tau c)$.

Accordingly, $\{([\tau], \Phi^0(\tau)) \in (\Gamma^*/\sim) \times \text{KSet}^0 | \tau \in \Gamma^*\}$ is a bisimulation between $\mathcal{U}(\mathcal{G})/\sim$ and $k(\mathcal{G})$ and, by Lemma 2, we can conclude that the games are equivalent.

**Corollary 11 (Bisimulation).** The finite parity game $\mathcal{K}$ on $k(\Gamma^*)$ is bisimilar to the information quotient $\mathcal{U}(\mathcal{G})$ of the original FIP game on $\Gamma^*/\sim$. Moreover, for every winning strategy $s$ in the parity game $\mathcal{K}$, the strategy $s \circ k = s \circ \Phi^{\{0\}}$ is winning in the FIP game $\mathcal{G}$.

By positional determinacy of parity games, if there exists a winning strategy in $\mathcal{K}$, then
there exists one represented by a labelling $s: Q^{\mathcal{K}} \to A$ of positions with actions. Recall that
the positions of $\mathcal{K}$ correspond to knowledge sets $\Phi^0(\tau)$ output by the automaton $\mathcal{H}$ (with
projection on the first component). By composing the output function of the automaton
with the action labelling $s$, we thus obtain a winning strategy for the game $\mathcal{G}$ at the outset.
**► Theorem 12.** The synthesis problem for FIP games with parity objectives is decidable. Whenever a winning strategy exists, we can effectively construct a Mealy automaton that defines one.

Given a FIP game with $n$ observers, the pre-processing step from Subsection 5.1 adds one observer, and thus the size $|K|$ of the perfect-information game constructed in the reduction is $(n+1)$-fold exponential in the size of the FIP game. Note that the number of priorities for the parity objective does not change. Since perfect-information parity games can be solved in time at most exponential in the number of priorities (actually, in quasi-polynomial time in the number of nodes, see, e.g., [18, 20]), we derive an $(n+1)$-EXPTIME upper bound for the synthesis problem.

Theorem 12 extends to all visible objectives for which perfect-information games are decidable, such as mean-payoff or discounted-sum conditions.

# 6 Complexity Lower Bound

We show a matching lower bound for reachability objectives, by a reduction of the membership problem for alternating $n$-EXPSPACE Turing machines, which is $(n+1)$-EXPTIME-complete, to the synthesis problem for FIP games with $n$ observers.

Intuitively, the FIP game simulates an execution of an alternating Turing machine $M$ on an input word $w$ of length $\ell$, where the player chooses transitions in existential states, and Nature chooses transitions in universal states. The winning condition requires the player to announce successive configurations of $M$ – consisting of the tape content (of $n$-fold exponential size), the head position, and the control state – until an accepting configuration is reached.

The main difficulty is to verify the consistency of these configurations using only polynomial-size Mealy automata. To address this, we use the structure of FIP games with imperfect information and $n$ observers. Instead of checking transitions directly, the game allows Nature to challenge the equality of successive configurations. Nature may mark differing positions in the two configurations by sending observations to designated observers. These marks are hidden to the player until a communication occurs.

If the marked bits differ, the player may claim the marks refer to different positions, which reduces to checking inequality between two $(n-1)$-fold exponential-size numbers. The player does so by pointing out a differing bit in their binary encodings and announcing its address (a $(n-2)$-fold exponential-size number) – again recursively allowing Nature to challenge this claim. Each level of this recursive protocol uses one of the $n$ observers. Eventually, the values are small enough to be verified by the objective automaton.

The encoding uses nested counters: a level-$n$ counter is a sequence of bits, each followed by its address as a level-$(n-1)$ counter. This encoding is directly inspired by a similar definition in previous work [14, Section 4.2]. We define actions for the player to emit bits, counters, Turing machine transitions, and specific claims like $r^{01}$ or $r^{10}$ asserting bit differences. Nature's moves include sending observations (marks), initiating communication, and branching to verification components in the Mealy automaton.

Correct encoding is enforced by separate Mealy components that check syntactic properties: correct counter format, input encoding, control state updates, and that configurations follow transitions. Nature can branch to any component. The marking mechanism allows checking bit-equality claims, and address comparison proceeds recursively with up to $n$ observers.

We argue that a small (polynomial-size) Mealy automaton can store the values of the marked bits in order to verify the player's claims ($r^{01}$ or $r^{10}$). Storing two bits at each level (hence $2n$ bits) would suffice if Nature never challenges the format of the counters announced
13:16 Synthesising Full-Information Protocols

by the player. However, if a challenge occurs, the game restarts at a lower level to check the
counter format, which requires storing only 2*(n − 1) bits at that level – assuming no further
challenges. Repeating this argument recursively, the total number of bits needed for storage
is O(n²). Since *n* is fixed independently of the input word *w* and the Turing machine *M*, the
resulting Mealy automata remain polynomial in size. This ensures that the overall reduction
is polynomial-time.

We conclude that the player has a winning strategy in the FIP game if and only if the
machine *M* accepts the input *w*.

**▶ Theorem 13.** *The synthesis problem for FIP games with *n* observers is (n+1)-EXPTIME-complete, both for parity and reachability objectives.*

7 Conclusion

We studied the problem of synthesising a finite-state process that must aggregate information
from multiple sources, where the accessibility of a source is determined through interaction
with the environment. This models dynamic networks with time-varying links and failures,
and captures *convergecast* (single-sink data aggregation) tasks in which a designated process
must fuse inputs from dispersed sensors while the environment controls when and with whom
communication occurs. In game-theoretic terms, the question requires handling information
trees with unbounded branching, beyond the reach of classical tree-automata approaches.

Our main contribution is a decision procedure for the case of one active player with
visible objectives and *n* passive observers. Technically, we introduce a higher-order knowledge
quotient that tracks nested coalitions and induces a p-morphism from the information quotient
to a finite perfect-information parity game on knowledge sets; by positional determinacy, a
winning strategy there yields a finite-state strategy for the original game.

The reduction is non-elementary in the number of observers, and we show tight complexity:
with *n* observers, the synthesis problem is (*n*+1)-EXPTIME-complete. The upper bound holds
for parity objectives and extends to other visible objectives (e.g., mean-payoff, discounted-
sum), and the lower bound already for reachability.

Outlook

(i) **Efficient implementability.** Given a FIP strategy, can it be implemented by processes that exchange only bounded-length messages ? The answer is not always yes. For instance, consider one active player and two observers that all receive bit sequences; the player can communicate with the observers only upon input 1, and the specification requires the player to indicate whether the two observation histories are equal. Clearly, any protocol with a finite message space fails; each observer must reveal her full private history. If instead of equality, the specification asks whether the observation histories belong to a given regular relation, the task is solvable under FIP (the specification is indeed a winning strategy), but deciding implementability with finite messages corresponds to the *monadic decomposability of regular relations* [3]. Lifting such decomposition techniques to scenarios with intermediary communication events appears challenging, but possible.

(ii) **Regular indistinguishability via two-tape automata.** For indistinguishability relations recognisable by two-tape automata, information trees form a more general subclass of automatic trees than those arising from FIP. Do such information trees always admit a finite bisimulation quotient? A positive answer would yield decidability for one-player synthesis in games with imperfect information beyond full-information protocols.
References

1 André Arnold, Aymeric Vincent, and Igor Walukiewicz. Games for synthesis of controllers with partial observation. *Theoretical computer science*, 303(1):7-34, 2003. doi:10.1016/S0304-3975(02)00442-5.

2 Salman Azhar, Gary Peterson, and John Reif. Lower bounds for multiplayer non-cooperative games of incomplete information. *Journal of Computers and Mathematics with Applications*, 41:957-992, 2001. doi:10.1016/S0898-1221(00)00333-3.

3 Pablo Barceló, Chih-Duo Hong, Xuan-Bach Le, Anthony W. Lin, and Reino Niskanen. Monadic Decomposability of Regular Relations. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, *46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)*, volume 132 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 103:1–103:14, Dagstuhl, Germany, 2019. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.ICALP.2019.103.

4 D. Berwanger and L. Doyen. Observation and distinction. representing information in infinite games. *Theory of Computing Systems*, 67(1):4–27, 2023. doi:10.1007/s00224-021-10044-x.

5 D. Berwanger, A. B. Mathew, and M. van den Bogaard. Hierarchical information and the synthesis of distributed strategies. *Acta Informatica*, 55(8):669–701, 2018. doi:10.1007/s00236-017-0306-5.

6 Dietmar Berwanger, Lukasz Kaiser, and Bernd Puchala. A perfect-information construction for coordination in games. In *IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2011, December 12-14, 2011, Mumbai, India*, volume 13 of *LIPIcs*, pages 387–398. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2011. doi:10.4230/LIPIcs.FSTTCS.2011.387.

7 J. R. Büchi and L. H. Landweber. Solving sequential conditions by finite-state strategies. *Transactions of the American Mathematical Society*, 138:295–311, 1969. doi:10.1090/S0002-9947-1969-0280205-0.

8 Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasi-polynomial time. *SIAM J. Comput.*, 51(2):17–152, 2022. doi:10.1137/17M1145288.

9 K. Chatterjee, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Algorithms for omega-regular games of incomplete information. *Logical Methods in Computer Science*, 3(3:4), 2007. doi:10.2168/LMCS-3(3:4)2007.

10 A. Church. Logic, arithmetics, and automata. *Proc. Int. Congr. Math.*, pages 23–35, 1962.

11 Cynthia Dwork and Yoram Moses. Knowledge and common knowledge in a byzantine environment: Crash failures. *Inf. Comput.*, 88(2):156–186, 1990. doi:10.1016/0890-5401(90)90014-9.

12 Kousha Etessami, Thomas Wilke, and Rebecca A. Schuller. Fair simulation relations, parity games, and state space reduction for Büchi automata. *SIAM J. Comput.*, 34(5):1159–1175, 2005. doi:10.1137/S0097539703420675.

13 Bernd Finkbeiner and Sven Schewe. Uniform distributed synthesis. In *20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings*, pages 321–330. IEEE Computer Society, 2005. doi:10.1109/LICS.2005.53.

14 B. Genest, H. Gimbert, A. Muscholl, and I. Walukiewicz. Asynchronous games over tree architectures. In *Proc. of ICALP: Automata, Languages, and Programming, LNCS 7966*, pages 275–286. Springer, 2013. doi:10.1007/978-3-642-39212-2_26.

15 Valentin Goranko and Martin Otto. Model theory of modal logic. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, *Handbook of Modal Logic*, volume 3 of *Studies in logic and practical reasoning*, pages 249–329. North-Holland, 2007. doi:10.1016/S1570-2464(07)80008-5.

16 Yuri Gurevich and Leo Harrington. Trees, automata, and games. In *Proceedings of the fourteenth annual ACM symposium on theory of computing*, pages 60–65, 1982. doi:10.1145/800070.802177.
13:18 Synthesising Full-Information Protocols

17 D. Harel and A. Pnueli. On the development of reactive systems. In Krzysztof R. Apt, editor, *Logics and Models of Concurrent Systems*, pages 477–498, Berlin, Heidelberg, 1985. Springer Berlin Heidelberg.

18 M. Jurdzinski, R. Morvan, and K. S. Thejaswini. Universal algorithms for parity games and nested fixpoints. In *Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday*, LNCS 13660, pages 252–271. Springer, 2022. doi:10.1007/978-3-031-22337-2_12.

19 Orna Kupferman and Moshe Y. Vardi. Synthesizing distributed systems. In Proc. of LICS '01, pages 389–398. IEEE Computer Society Press, June 2001. doi:10.1109/LICS.2001.932514.

20 Karoliina Lehtinen, Pawel Parys, Sven Schewe, and Dominik Wojtczak. A recursive approach to solving parity games in quasip polynomial time. Log. Methods Comput. Sci., 18(1), 2022. doi:10.46298/LMCS-18(1:8)2022.

21 Tal Mizrahi and Yoram Moses. Continuous consensus with ambiguous failures. Theor. Comput. Sci., 411(34-36):3031-3041, 2010. doi:10.1016/J.TCS.2010.04.025.

22 M. Pease, R. Shostak, and L. Lamport. Reaching agreements in the presence of faults. Journal of the ACM, 27(2):228-234, April 1980. doi:10.1145/322186.322188.

23 A. Pnueli and R. Rosner. Distributed reactive systems are hard to synthesize. In Proc. of FOCS: Foundations of Computer Science, pages 746–757. IEEE, 1990.

24 M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the AMS, 141:1–35, 1969.

25 M. O. Rabin. Automata on Infinite Objects and Church's Problem. American Mathematical Society, Boston, MA, USA, 1972.

26 John H. Reif. The complexity of two-player games of incomplete information. Journal of Computer and System Sciences, 29(2):274–301, 1984. doi:10.1016/0022-0000(84)90034-5.

27 D. Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011.

28 Sven Schewe. Distributed synthesis is simply undecidable. Inf. Process. Lett., 114(4):203-207, April 2014. doi:10.1016/j.ipl.2013.11.012.

29 W. Thomas. On the synthesis of strategies in infinite games. In Proc. of STACS: Symposium on Theoretical Aspects of Computer Science, LNCS 900. Springer, 1995. doi:10.1007/3-540-59042-0_57.

30 W. Thomas. Languages, automata, and logic. In Handbook of Formal Languages, volume 3, Beyond Words, chapter 7, pages 389–455. Springer, 1997. doi:10.1007/978-3-642-59126-6_7.

31 Thomas YC Woo and Simon S Lam. A lesson on authentication protocol design. ACM SIGOPS Operating Systems Review, 28(3):24–37, 1994. doi:10.1145/182110.182113.