Béatrice Bérard

Benedikt Bollig

Patricia Bouyer

Matthias Függer

Nathalie Sznajder

C B Bérard

Synthesis in Presence of Dynamic Links

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Starting from Church's work [START_REF] Church | Applications of recursive arithmetic to the problem of circuit synthesis -Summaries of talks[END_REF] on synthesizing circuits from arithmetic specifications in the 1960s, automatic synthesis of programs or circuits has been widely studied.

In the case of a reactive system, given a specification, the goal is to find an implementation for a system that repeatedly receives inputs from the environment and generates outputs such that the system's behavior adheres to the specification. Early work [START_REF] Pnueli | A framework for the synthesis of reactive modules[END_REF][START_REF] Pnueli | On the synthesis of a reactive module[END_REF][START_REF] Michael | Automata on infinite objects and Church's problem. 13[END_REF] was synthesizing algorithms that require knowledge of the complete system state, inherently yielding single-process solutions.

Single-process synthesis is related to finding a strategy for a player representing the process that has to win against the adversarial environment, and has been studied in the context of games [START_REF] Abadi | Realizable and unrealizable specifications of reactive systems[END_REF][START_REF] Büchi | Solving sequential conditions by finite-state strategies[END_REF][START_REF] Thomas | On the synthesis of strategies in infinite games[END_REF] as well as with automata techniques [START_REF] Kupferman | Church's problem revisited[END_REF][START_REF] Pnueli | On the synthesis of a reactive module[END_REF].

For systems with more than one process, different models for how communication and computation is organized have been studied. Their two extremes are message-triggered asynchronous computation [START_REF] Gastin | Distributed games with causal memory are decidable for series-parallel systems[END_REF][START_REF] Madhusudan | The MSO theory of connectedly communicating processes[END_REF] and round-wise synchronous computation.

An example for the latter is the work by Pnueli and Rosner [START_REF] Pnueli | Distributed reactive systems are hard to synthesize[END_REF], who considered synchronous distributed systems with an a priori fixed communication network. In their model, the network is given by a directed communication graph, whose nodes are the processes and with a link from process p to q if p can send messages to q (or write to and read from a shared variable). Messages are from a fixed, finite alphabet per link. A solution to the synthesis problem is a distributed algorithm that operates in rounds, repeatedly reading inputs, exchanging messages, and setting outputs. Already the case of two processes with separate inputs and outputs, and without a communication link to each other, was shown to be undecidable for linear temporal logic (LTL) specifications [START_REF] Pnueli | The temporal semantics of concurrent programs[END_REF] on the inputs and outputs. As a positive result, the paper presents a solution for unidirectional process chains.

Still in the case of static architectures and bounded messages, Kupferman and Vardi [START_REF] Kupferman | Synthesis with incomplete information[END_REF][START_REF] Kupferman | Synthesizing distributed systems[END_REF] extended decidability results to branching time specifications and proved sufficient conditions on communication networks for decidability, while Finkbeiner and Schewe [START_REF] Finkbeiner | Uniform distributed synthesis[END_REF] presented a characterization of networks where synthesis is decidable. Since specifications are allowed to talk about messages, however, they are powerful enough to break existing communication links between processes, leading to undecidability like in the two-process system without communication [START_REF] Pnueli | Distributed reactive systems are hard to synthesize[END_REF]. Gastin et al. [START_REF] Gastin | Distributed synthesis for well-connected architectures[END_REF] proved a necessary and sufficient condition for decidability on a class of communication networks if specifications are only on inputs and outputs. Like [START_REF] Gastin | Distributed synthesis for well-connected architectures[END_REF], our work only allows "input-output" specifications, so that we obtain decidability in several cases where the framework of [START_REF] Finkbeiner | Uniform distributed synthesis[END_REF] does not allow it.

Like in the single-process scenario, synthesis in distributed systems can be modeled as a game, which, in this context, are partial information games played between a cooperating set of processes against the environment [START_REF] Berwanger | Hierarchical information and the synthesis of distributed strategies[END_REF][START_REF] Van Der Meyden | Synthesis of distributed systems from knowledge-based specifications[END_REF][START_REF] Mohalik | Distributed games[END_REF][START_REF] Gary | Multiple-person alternation[END_REF]. With the exception of [START_REF] Berwanger | Hierarchical information and the synthesis of distributed strategies[END_REF], all the above approaches assume static, reliable networks. In [START_REF] Berwanger | Hierarchical information and the synthesis of distributed strategies[END_REF], Berwanger et al. study games in which information that players have about histories is hierarchically ordered, and this order may change dynamically during a play. The main difference to our work is that we consider a memory model where messages carry the complete causal history allowing for unbounded communication messages, while [START_REF] Berwanger | Hierarchical information and the synthesis of distributed strategies[END_REF] is based on local observations so that, at every round, a bounded amount of information is transmitted between players. Further, while asynchronous solutions to the synthesis problem considered potentially unbounded messages [START_REF] Gastin | Distributed games with causal memory are decidable for series-parallel systems[END_REF][START_REF] Madhusudan | The MSO theory of connectedly communicating processes[END_REF], previous synchronous solutions assume an a priori fixed message size. Also [START_REF] Madhusudan | The MSO theory of connectedly communicating processes[END_REF] assume that processes that communicate infinitely often encounter each other within a bounded number of steps.

The above assumptions have two shortcomings:

Modeling unreliability. Distributed computing has a long history of studying algorithms that provide services in presence of unstable or unreliable components [START_REF] Lynch | Distributed algorithms[END_REF]. Indeed, classical process and link failures can be treated as particular dynamic network behavior [START_REF] Charron-Bost | The heard-of model: computing in distributed systems with benign faults[END_REF]. Early work by Akkoyunlu et al. [START_REF] Eralp | Some constraints and tradeoffs in the design of network communications[END_REF] considered the problem of two groups of gangsters coordinating a coup despite an unreliable channel between both parties; later on generalized to the Byzantine generals problem [START_REF] Lamport | The Byzantine Generals Problem[END_REF]. Protocols like the Alternating Bit Protocol [START_REF] Bartlett | A note on reliable full-duplex transmission over half-duplex links[END_REF] aim at tolerating message loss between a sender and receiver node, and [START_REF] Aho | Bounds on the size and transmission rate of communications protocols[END_REF] studies optimal transmission rates over unreliable links. Afek et al. [START_REF] Afek | Reliable communication over unreliable channels[END_REF] discuss protocols that implement reliable links on top of unreliable links. Further, for algorithms that have to operate in dynamic networks, see, e.g., [START_REF] Charron-Bost | Approximate Consensus in Highly Dynamic Networks: The Role of Averaging Algorithms[END_REF][START_REF] Coulouma | A Characterization of Dynamic Networks Where Consensus is Solvable[END_REF][START_REF] Kuhn | Distributed computation in dynamic networks[END_REF], network changes are the normal case rather than the exception. Synthesis with unstable or faulty components has been studied by Velner and Rabinovich [START_REF] Velner | Church synthesis problem for noisy input[END_REF] for two player games in presence of information loss between the environment and the inputs of a process. The approach is restricted to a single process, however. Dimitrova and Finkbeiner [START_REF] Dimitrova | Synthesis of fault-tolerant distributed systems[END_REF] study synthesis of fault-tolerant distributed algorithms in synchronous, fully connected networks. Processes are partitioned into correct and faulty. It is assumed that at every round at least one process is correct and the output of a correct process must not depend on the local inputs of faulty processes. While unreliable links can be mapped to process failures, the above assumptions are a priori too restrictive to cover dynamic networks.

Modeling full-information protocols. An important class of distributed algorithms are full-information protocols, where nodes piggy-pack previously received messages onto current messages [START_REF] Fagin | Reasoning about knowledge[END_REF][START_REF] Lynch | Distributed algorithms[END_REF]. By construction, such algorithms do not have bounded message size. This kind of causal memory has been considered in [START_REF] Gastin | Distributed games with causal memory are decidable for series-parallel systems[END_REF][START_REF] Genest | Asynchronous Games over Tree Architectures[END_REF][START_REF] Gimbert | On the Control of Asynchronous Automata[END_REF][START_REF] Madhusudan | The MSO theory of connectedly communicating processes[END_REF] for synthesis and control of Zielonka automata over Mazurkiewicz traces with various objectives, ranging from local-state reachability to ω-branching behaviors. Zielonka automata usually model asynchronous processes (there is no global clock so that processes evolve at their own speed until they synchronize) and symmetric communication (whenever processes synchronize, they mutually exchange their complete history).

In this work we consider the synthesis problem for a system of two nodes communicating in synchronous rounds, where specifications are given as LTL formulas or, more generally, ω-regular languages. The nodes are connected via a dynamic link. As in [START_REF] Charron-Bost | Approximate Consensus in Highly Dynamic Networks: The Role of Averaging Algorithms[END_REF][START_REF] Coulouma | A Characterization of Dynamic Networks Where Consensus is Solvable[END_REF], a network is a set of communication graphs, called network model. A distributed algorithm operates in rounds as in [START_REF] Pnueli | Distributed reactive systems are hard to synthesize[END_REF], with the difference that the communication graph is chosen by an adversary per round. Motivated by communication buses, like the industry standard I 2 C bus [START_REF]I2C-Bus Specification and User Manual[END_REF] and CAN bus [2], with direct acknowledge mechanisms after message transfers, we assume that nodes are aware if messages have been delivered successfully. In contrast to the Pnueli-Rosner setting, we suppose full-information protocols where processes have access to their causal history. That is, the dynamic links have unbounded message size. Unlike in Zielonka automata over traces, however, we consider synchronous processes and potentially asymmetric communication. In particular, the latter implies that a process may learn all about the other's history without revealing its own. Observe that, when restricting to Zielonka automata, synthesis of asynchronous distributed systems is not a generalization of the synchronous case.

We show that the synthesis problem is decidable for a network model if and only if it does not contain the empty link that dismisses both nodes' messages. As we assume that LTL specifications can not only reason about inputs and outputs, but also about the communication graph, our result covers synthesis for dynamic systems where links change in more restricted ways. In particular, this includes processes that do not send further messages after their message has been lost, bounded interval omission faults, etc.

Outline. We define the synthesis problem for the dynamic two-process model in Section 2. In Section 3, we discuss the asymmetric model where communication to process 1 never fails. Central to the analysis is to show that, despite the availability of unbounded communication links, finite-memory distributed algorithms actually suffice. We then prove that the synthesis problem is decidable (Theorem 2). In Section 5 we reduce the general case of dynamic communication to the asymmetric case, obtaining our main result of decidability in network models that do not contain the empty link (Theorem 1). We conclude in Section 6. Missing proofs can be found in the appendix.

The Synthesis Problem

We start with a few preliminaries. Let N = {0, 1, 2, . . .}. For a (possibly infinite) alphabet A, the set of finite words over A is denoted by A * , the set of nonempty finite words by A + , and the set of countably infinite words by A ω . We let ε be the empty word and denote the concatenation of w 1 ∈ A * and w 2 ∈ A * ∪ A ω by w 1 • w 2 or simply w 1 w 2 .

Fix the set of processes P = {1, 2}. Every process p ∈ P comes with fixed finite sets X p and Y p of possible inputs and outputs, respectively. We assume there are at least two possible inputs and outputs per process, i.e., |X p | ≥ 2 and |Y p | ≥ 2.

We consider systems where computation and communication proceed in rounds. In round r = 0, 1, 2, . . ., process p ∈ P receives an input x r p ∈ X p and it produces an output y r p ∈ Y p . The decision on y r p depends on the knowledge that process p has about the execution up to round r. In addition to all local inputs x 0 p , . . . , x r p , this knowledge can also include inputs of the other process, which may be communicated through communication links.

Following Charron-Bost et al. [START_REF] Charron-Bost | Approximate Consensus in Highly Dynamic Networks: The Role of Averaging Algorithms[END_REF], we consider a dynamic communication topology in terms of a network model, i.e., a fixed nonempty set N ⊆ {-×, , , } of potentially occurring communica-

x 0 1 - × x 0 2 x 1 1 - × x 1 2 x 2 1 - × x 2 2 x 3 1 - × x 3 2 x 0 1 x 0 2 x 1 1 x 1 2 x 2 1 x 2 2 x 3 1 x 3 2 x 0 1 x 0 2 x 1 1 x 1 2 x 2 1 x 2 2 x 3 1 x 3 2
Figure 1: w 1 for some histories w; the white part is unknown in the view, and replaced by ⊥.

tion graphs. In round r, a graph r ∈ N is chosen non-deterministically with the following intuitive meaning:

-× No communication takes place. The knowledge of process p that determines y r p only includes the knowledge at round r -1 as well as the new input x r p .

Process 1 becomes aware of the whole input sequence x 0 2 . . . x r 2 that process 2 has received so far. This includes x r 2 , which is transmitted without delay. The case is analogous. Both processes become aware of the whole input sequence of the other process.

As discussed in the introduction, the knowledge of process p at round r also includes the communication link r at r, which is therefore common knowledge.

Histories and Views

Let us be more formal. Recall that we fixed the sets P, X p , Y p , and N . We let Σ = X 1 × N × X 2 be the set of input signals. For ease of notation, we write x 1

x 2 instead of (x 1 , , x 2 ) ∈ Σ. Moreover, for ∈ N , we let Σ = X 1 × { } × X 2 . A word w ∈ Σ * represents a possible history, a sequence of signals to which the system has been exposed so far. For a process p, we inductively define the view w p of p on w by replacing inputs that are invisible to p by the symbol ⊥ (we suppose ⊥ ∈ X 1 ∪ X 2 ). First of all, let ε 1 = ε 2 = ε. Moreover, for u ∈ Σ * :

u x 1 x 2 1 = u x 1 x 2 u x 1 x 2 2 = u x 1 x 2 u x 1 x 2 1 = u x 1 x 2 u x 1 x 2 2 = u x 1 x 2 u x 1 x 2 1 = u 1 x 1 ⊥ u x 1 x 2 2 = u 2 ⊥ x 2 u x 1 - × x 2 1 = u 1 x 1 - × ⊥ u x 1 - × x 2 2 = u 2 ⊥ -× x 2
With this, we let Views 1 = { w 1 | w ∈ Σ + } and Views 2 = { w 2 | w ∈ Σ + } be the sets of possible views of processes 1 and 2. The view w 1 is illustrated in Figure 1 for three different words w. For the history in the middle, we have x 0 1

x 0 2 x 1 1 x 1 2 x 2 1 x 2 2 x 3 1 x 3 2 1 = x 0 1 x 0 2 x 1 1 x 1 2 x 2 1 ⊥ x 3 1 ⊥ .

Linear-Time Temporal Logic

Let Ω = Y 1 ×Y 2 be the set of output signals. An execution is a word from (Σ × Ω) ω , which records, apart from the input signals, the outputs at every round. A convenient specification language to define the valid system executions is linear-time temporal logic (LTL) interpreted over words from (Σ × Ω) ω . The logic can, therefore, talk about inputs, outputs, and communication links at a given position. Moreover, it has the usual temporal modalities. Formally, the set LTL(N ) of LTL formulas is given by the grammar

ϕ ::= (in p = x) | (out p = y) | (link = ) | atomic formulas Xϕ | Fϕ | Gϕ | ϕUϕ | temporal modalities ¬ϕ | ϕ ∨ ϕ | ϕ ∧ ϕ | ϕ =⇒ ϕ | ϕ ⇐⇒ ϕ Boolean connectives
where p ∈ P, x ∈ X p , y ∈ Y p , and ∈ N . Let e = α 0 α 1 α 2 . . . be an execution with α i ∈ Σ × Ω for all i ∈ N and α 0 = x 0 1 0 x 0 2 , (y 0 1 , y 0 2 ) . For r ∈ N, let e ≥r denote its suffix α r α r+1 α r+2 . . ., i.e., e = e ≥0 . Boolean connectives are interpreted as usual. Moreover: Finally, we let L(ϕ) = {e ∈ (Σ × Ω) ω | e |= ϕ} be the set of executions that satisfy ϕ. Remark 1. In general, the sequence of communication graphs in an execution is arbitrary from N ω , modeling a highly dynamic network without any restrictions on stability, eventual convergence, etc. Note that the specification is allowed to speak about the communication links along a history, however, with the possibility to restrict the behavior of the dynamic network and impose process behavior to depend on the network dynamics.

e |= (in p = x) if x 0 p = x e |= Xϕ if
Example 1. Suppose X 1 = X 2 = Y 1 = Y 2 = {0, 1} and N = { , }. Consider ϕ 1 = G (out 1 = 1) ⇐⇒ (out 2 = 1)
ϕ 2 = GF (in 1 = 1) ∧ (in 2 = 1) ⇐⇒ GF (out 1 = 1) ∧ (out 2 = 1) ψ = GF(link = ) ∧ GF(link = ) =⇒ ϕ 1 ∧ ϕ 2 .
Formula ϕ 1 says that, in each round, both processes agree on their output. Formula ϕ 2 postulates that both processes simultaneously output 1 infinitely often if, and only if, both inputs are simultaneously 1 infinitely often. Finally, ψ requires ϕ 1 and ϕ 2 to hold if both communication links occur infinitely often. We will come back to these formulas later to illustrate the synthesis problem.

Synthesis Problem

A distributed algorithm is a pair f = ( f 1 , f 2 ) of functions f 1 : Views 1 → Y 1 and f 2 : Views 2 → Y 2 that associate with each view an output. Given w = σ 0 σ 1 σ 2 . . . ∈ Σ ω , we define the execution f w = σ 0 , (y 0 1 , y 0 2 ) σ 1 , (y 1 1 , y 1 2 ) . . . ∈ (Σ × Ω) ω where y r p = f p ( σ 0 . . . σ r p ). For a finite word w ∈ Σ * , we define f w ∈ (Σ × Ω) * similarly (in particular, f ε = ε).

Let L ⊆ (Σ × Ω) ω and ϕ ∈ LTL(N ). We say that f fulfills L (respectively ϕ) if, for all w ∈ Σ ω , we have f w ∈ L (respectively f w ∈ L(ϕ)). Moreover, we say that L (respectively ϕ) is realizable if there is some distributed algorithm that fulfills L (respectively ϕ).

We are now ready to define our main decision problem:

Definition 1. For a fixed network model N (recall that we also fixed P, X p , Y p ), the synthesis problem SYNTHESIS(N ) is defined as follows:

Input: ϕ ∈ LTL(N )
Question: Is ϕ realizable?

Example 2. Consider the formulas ϕ 1 , ϕ 2 , ψ from Example 1 over N = { , }. We easily see that ϕ 1 is realizable by the distributed algorithm where both processes always output 1. However, ϕ 1 ∧ ϕ 2 is not realizable: if the communication link is always (an analogous argument holds for ), process 2 has no information about any of the inputs of process 1. Thus, it is impossible for the processes to agree on their outputs in every round while respecting ϕ 2 .

round signal 0 0 0 1 0 1 0 1 0 0 2 0 1 1 0 3 0 0 0 0 4 1 1 0 1 5 0 1 1 0 6 1 0 0 1 7 0 0 1 0 8 0 1 0 0 9 0 1 1 0 Figure 2: Fulfilling ψ
Finally, formula ψ is realizable. We can now assume that both and occur infinitely often. A sequence of signals can be divided into maximal finite blocks with identical communication links as illustrated in Figure 2 for the prefix of an execution. The distributed algorithm proceeds as follows. By default, both processes ouput 0, with the following exception: at the first position of each block, a process outputs 1 if, and only if, the preceding block contains a round where both processes simultaneously received 1. Note that this preceding block is entirely contained in the view of both processes. The algorithm's outputs are illustrated in Figure 2. At rounds 4 and 6, they are 1 because the corresponding preceding blocks contain an input pair of 1's. As every block has finite size, satisfaction of ϕ 2 is guaranteed.

It is well known that the synthesis problem is undecidable if processes are not connected:

Fact 1 (Pnueli-Rosner). The problem SYNTHESIS({-×}) is undecidable.
One also observes that undecidability of the synthesis problem is upward-closed:

Lemma 1. Let N 1 ⊆ N 2 . If SYNTHESIS(N 1 ) is undecidable, then so is SYNTHESIS(N 2 ). Indeed, formula ϕ 1 ∈ LTL(N 1 ) is realizable iff formula ϕ 2 ∈ LTL(N 2 ) is realizable where we let ϕ 2 = G ∈N 1 (link = ) =⇒ ϕ 1 .
Therefore, we will now focus on network models that do not contain -×. Our main result is the following:

Theorem 1. For a network model N , SYNTHESIS(N ) is decidable if and only if - × / ∈ N .
The "only if" direction follows from Fact 1 and Lemma 1. The rest of the paper is devoted to the proof of the "if" direction of Theorem 1. We will first consider N = { , } and then reduce the other cases to this particular network model. By Lemma 1, it is enough to do this reduction for { , , }.

3 Finite-Memory Distributed Algorithms for N = { , }

In this section, we suppose N = { , }. We show that, in this case, synthesis is decidable:

Theorem 2. The problem SYNTHESIS({ , }) is decidable (in 4-fold exponential time).
As our setting features a dynamic architecture and unbounded message size in terms of causal histories, the proof of the theorem requires some new techniques. In particular, we cannot apply the information-fork criterion from [START_REF] Finkbeiner | Uniform distributed synthesis[END_REF], since our specifications can only describe the link between the processes, and cannot constrain the contents of the messages.

The proof is spread over the remainder of this section as well as Section 4. It crucially relies on the fact that, for every realizable specification ϕ, there is a distributed algorithm with a sort of finite memory fulfilling it (as shown in this section). This allows us to reduce, in Section 4, the problem of finding a distributed algorithm to finding a winning strategy in a decidable game (that we will call a (2, 1)-player game thereafter) involving two cooperating players, where one player has imperfect information, and an antagonistic environment. Remark 2. For the sake of technical simplification, we assume in Sections 3 and 4, without loss of generality, that input sequences start with a symbol from Σ = X 1 × { } × X 2 . Instead of the original formula φ, we then simply take ϕ = X φ. That is, we can henceforth consider that Views

1 = { w 1 | w ∈ Σ Σ * } and Views 2 = { w 2 | w ∈ Σ Σ * }
, and that a distributed algorithm f fulfills ϕ ∈ LTL(N ) if, for all w ∈ Σ Σ ω , we have f w ∈ L(ϕ).

Finite-Memory Distributed Algorithms

Deterministic Rabin Word Automata. Our decidability proof and the definition of a finite-memory distributed algorithm rely on deterministic Rabin word automata (cf. [START_REF] Thomas | Automata on Infinite Objects[END_REF]): Definition 2. A deterministic Rabin word automaton (DRWA) over a finite alphabet A is a tuple A = (S, ι, δ , F ), where S is a finite set of states, ι ∈ S is the initial state, δ : S × A → S is the transition function, and F ⊆ 2 S × 2 S is the (Rabin) acceptance condition.

The DRWA A defines a language of infinite words L(A ) ⊆ A ω as follows. We extend δ to a function δ :

S × A * → S letting δ (s, ε) = s and δ (s, aw) = δ (δ (s, a), w). Let w = a 0 a 1 a 2 . . . ∈ A ω . We define Visit ∞ A (w) = {s ∈ S | s = δ (ι, a 0 . . . a i ) for infinitely many i ∈ N}. We say that w is accepted by A if there is (F, F ) ∈ F such that Visit ∞ A (w) ∩ F = / 0 and Visit ∞ A (w) ∩ F = / 0, i.e.
, some state of F is visited infinitely often, whereas all states from F are visited only finitely often. We let

L(A ) = {w ∈ A ω | w is accepted by A }.
Existence of Finite-Memory Distributed Algorithms. We are now ready to state that, if there is a distributed algorithm that fulfills a specification ϕ ∈ LTL(N ), then there is also a distributed algorithm f with finite "synchronization memory" in the following sense: There is a DRWA A over Σ × Ω such that the output of a process for a history wu with u ∈ Σ Σ * only depends on u and the state that A reaches after reading f w . Let

Σ ⊥ = {⊥} × { } × X 2 .
Lemma 2. Let ϕ ∈ LTL(N ). There is a DRWA A = (S, ι, δ , F ), with δ : S × (Σ × Ω) → S, such that the following are equivalent:

(1) There is a distributed algorithm f = ( f 1 , f 2 ) that fulfills ϕ.

(2) There is a distributed algorithm f = ( f 1 , f 2 ) that fulfills ϕ and such that, for all words w, w ∈ {ε} ∪ Σ Σ * satisfying δ (ι, f w ) = δ (ι, f w ), the following hold:

• f 1 (wu) = f 1 (w u) for all u ∈ Σ Σ * • f 2 (wu) = f 2 (w u) for all u ∈ Σ Σ * ⊥
Note that the acceptance condition and the language of A are not important in the lemma.

Distributed Algorithms as Strategy Trees

Section 3.2 is devoted to the proof of Lemma 2. The first step is to represent a distributed algorithm as a strategy tree, whose branching structure reflects the algorithm's choices depending on the various inputs. We then build a tree automaton that accepts a strategy tree iff it represents a distributed algorithm fulfilling the given formula ϕ. The challenge is to define the tree automaton in such a way that its strategies can be cast into hierarchical multiplayer games with finite sets of observations, and that winning strategies within these games are equivalent to distributed algorithms. We show in this section that this is possible by collapsing potentially unboundedly long input sequences into an unbounded branching structure. With this construction, we can show that, if the tree automaton recognizes some strategy tree, then it also accepts one that represents a finite-memory distributed algorithm.

Trees and Rabin Tree Automata. Let A be a nonempty (possibly infinite) alphabet and D be a nonempty (possibly infinite) set of directions. An A-labeled D-tree is a mapping t : D * → A. In particular, ε is the root with label t(ε), and ud is the d-successor of node u ∈ D * , with label t(ud). A run of T on an A-labeled D-tree t is an S-labeled D-tree ρ : D * → S where ρ(ε) = ι (the root is assigned the initial state) and, for all u ∈ D * , ρ(u),t(u), d ∈ D → ρ(ud) ∈ ∆. The latter is the transition applied at u, and we denote it by trans ρ (u).

A path of run ρ is a word

ξ = d 0 d 1 d 2 . . . ∈ D ω , inducing the sequence ε, d 0 , d 0 d 1 , d 0 d 1 d 2 , .
. . of nodes visited along ξ . We let Inf(ξ ) be the set of states that occur infinitely often as the labels of these nodes. Path ξ is accepting if there is (F, F ) ∈ F such that Inf(ξ ) ∩ F = / 0 and Inf(ξ ) ∩ F = / 0. Run ρ is accepting if all its paths are accepting. Finally, T defines the language of A-labeled D-trees L(T ) = {t : D * → A | there is an accepting run of T on t}. Lemma 3. Let A be a singleton alphabet, D a nonempty (possibly infinite) set of directions, and T an RTA over A-labeled D-trees (as A is a singleton, we say that T is input-free). Call a run ρ of T on the unique A-labeled D-tree rational if, for all w, w ∈ D * with ρ(w) = ρ(w ), we have trans ρ (w) = trans ρ (w ). If L(T ) = / 0, then there is a rational accepting run of T .

The lemma essentially follows from the fact that Rabin games are positionally determined for the player that aims at satisfying the Rabin objective [START_REF] Klarlund | Progress Measures, Immediate Determinacy, and a Subset Construction for Tree Automata[END_REF]. To account for our non-standard setting of tree automata with possibly infinite D, we give a direct proof in Appendix A.

Strategy Trees. Recall that our goal is to show Lemma 2 using strategy trees as a representation of distributed algorithms. Strategy trees are trees over the (infinite) set of directions D = Σ Σ * , with the aim to isolate the positions where a resynchronization occurs, via a letter from Σ . By Remark 2, we only have to consider Σ Σ * = (Σ Σ * ) + = D + . Hence, to avoid additional notation, we can identify nonempty words in D * with words in Σ Σ * . It will always be clear from the context whether the underlying alphabet is D or Σ.

Intuitively, a node u ∈ D * represents a given history, and the label of u represents the outputs for possible continuations from Σ Σ * . More precisely, the set Λ of labels is the set of pairs λ = (λ 1 , λ 2 ) where λ 1 :

Σ Σ * → Y 1 and λ 2 : Σ Σ * ⊥ → Y 2 . For w ∈ Σ Σ * , we define λ w ∈ (Σ × Ω)(Σ × Ω) * as expected (cf. the definition of f w for a distributed algorithm f ). Similarly, for w ∈ Σ Σ ω , we obtain a word λ w ∈ (Σ × Ω)(Σ × Ω) ω .
A strategy tree is a Λ-labeled D-tree t : D * → Λ. For u ∈ D * , let (λ u 1 , λ u 2 ) refer to t(u). The distributed algorithm associated with t is denoted by f t and is defined as

f t = ( f 1 , f 2 ) as follows (recall that Σ ⊥ = {⊥} × { } × X 2 ): • f 1 (uu ) = λ u 1 (u ) for all u ∈ {ε} ∪ Σ Σ * and u ∈ Σ Σ * • f 2 (uu ) = λ u 2 (u ) for all u ∈ {ε} ∪ Σ Σ * , and u ∈ Σ Σ * ⊥ ε d dd . . . . . . . . . . . . 0 0 1 0 0 1 1 1 0 0 1 1 0 0 d λ ε 1 1 0 . . . 0 1 . . . 0 0 1 1 0 0 1 1 λ ε 2 1 0 . . . 1 0 0 0 1 1 ⊥ 0 ⊥ 1 λ d 1 0 1 . . . 1 0
. . . In λ u 1 (u ) and λ u 2 (u ), we consider the unique decomposition of u over D so that f 1 and f 2 are welldefined. Remark 3. The mapping t → f t is a bijection. In particular, for every distributed algorithm f , there is a strategy tree t such that f t = f . 3 depicts a part of a strategy tree t. Its nodes are gray-shaded. The labels of nodes of t are themselves represented as (infinite) trees. Consider the input sequence w = 1 1 0 0 1 1 0 0 ∈ Σ Σ * . To know what f t outputs for the first two signals, we look at the blue-colored nodes of the trees associated with the root of t. To determine the outputs for the two remaining signals, we look at the red-colored nodes of the trees associated with node d. We thus get f t w = ( 1 1 , (0, 0))( 0 0 , (0, 1))( 1 1 , (1, 0))( 0 0 , (1, 1)) for the whole word w. Now, Lemma 2 is a consequence of the following lemma: Lemma 4. Let ϕ ∈ LTL(N ). There is a DRWA A = (S, ι, δ , F ), with δ : S × (Σ × Ω) → S, such that the following are equivalent:

0 0 1 1 0 0 1 1 λ d 2 0 0 . . . 1 1 0 0 1 1 ⊥ 0 ⊥ 1
Example 3. Suppose X 1 = X 2 = Y 1 = Y 2 = {0, 1}. Figure
(1) There is a strategy tree t such that f t fulfills ϕ.

(2) There is a strategy tree t such that (a) f t fulfills ϕ, and (b) for all w, w ∈ D * with δ (ι, f t w ) = δ (ι, f t w ), we have t(w) = t(w ).

Proof. Let ϕ ∈ LTL(N ) be the given formula. We first define A and then prove its correctness in terms of the statement of Lemma 4 using an RTA T ϕ over strategy trees.

The DRWA A . It is well known that there is a DRWA A ϕ = (S ϕ , ι ϕ , δ ϕ , F ϕ ) over Σ × Ω, with doubly exponentially many states and exponentially many acceptance pairs, such that L(A ϕ ) = L(ϕ) (cf. [START_REF] Safra | On the Complexity of ω-Automata[END_REF][START_REF] Vardi | Reasoning About Infinite Computations[END_REF]). We refer to states of A ϕ by ∈ S ϕ .

Starting from A ϕ , we now define the DRWA A = (S, ι, δ , F ) such that, for words that contain infinitely many , it is enough to look at the sequence of states reached by A right before thepositions to determine whether the word is in L(A ϕ ) or not. The idea is to keep track of the set of states that are taken between two -positions. Accordingly, the set of states is S = S ϕ × 2 S ϕ , with initial state ι = (ι ϕ , / 0). Concerning the transitions, for ( , R) ∈ S and α = (

x 1 x 2 , (y 1 , y 2 )) ∈ Σ × Ω, we let δ (( , R), α) = (δ ϕ ( , α), {δ ϕ ( , α)} ∪ R) if = (δ ϕ ( , α), {δ ϕ ( , α)}) if = .
Finally, the acceptance condition is given by

F = {(G F , G F ) | (F, F ) ∈ F ϕ } where G F = {( , R) ∈ S | F ∩ R = / 0} and G F = {( , R) ∈ S | F ∩ R = / 0}.
The following claim states that A is correct wrt. executions with infinitely many synchronization points, while the acceptance condition is looking only at states reached right before these synchronizing points (see Appendix B for the proof):

Claim 1. Let w 0 , w 1 , w 2 , . . . ∈ (Σ × Ω)(Σ × Ω) * . Moreover, let w = w 0 w 1 w 2 . . . be the concatenation of all w i . Set s 0 = ι and, for i ∈ N, s i+1 = ( i+1 , R i+1 ) = δ (ι, w 0 . . . w i ). Then, w ∈ L(A ϕ ) ⇐⇒ the sequence s 0 , s 1 , s 2 , . . . satisfies F ⇐⇒ w ∈ L(A ).
The RTA T ϕ . To get finite-memory algorithms, we will rely on Lemma 3, which is based on tree automata. In fact, a crucial ingredient of the proof is an RTA T ϕ over Λ-labeled D-trees such that

L(T ϕ ) = {t | t is a strategy tree such that f t fulfills ϕ}.
It is defined by T ϕ = (S, ι, ∆, F ) where S, ι, and F are taken from A , and ∆ is given by

∆ = (s = ( , R), λ , (s d ) d∈D ) s d = δ (s, λ d ) for all d ∈ Σ Σ * (T1) λ w ∈ L(A ϕ [ ]) for all w ∈ Σ Σ ω (T2)
.

Here, A ϕ [ ] = (S ϕ , , δ ϕ , F ϕ ) is the automaton A ϕ but where ι ϕ has been replaced by as the initial state. While condition (T1) "unfolds" A into the tree structure taking care of input sequences with infinitely many synchronization points, condition (T2) guarantees that the distributed algorithm behaves correctly should there be no more synchronization. Correctness of T ϕ , which relies on Claim 1, is shown in Appendix C.

Putting It Together. We now obtain Lemma 4 as a corollary from Lemma 3 using T ϕ . Direction (2) =⇒ (1) is trivial. Let us show (1) =⇒ (2) and suppose L(T ϕ ) = / 0. Consider the input-free RTA T ϕ = (S, ι, ∆ , F ) obtained from T ϕ by replacing the transition relation with

∆ = {(s, (s d ) d∈D ) | (s, λ , (s d ) d∈D ) ∈ ∆}. Note that L(T ϕ ) = /
0. By Lemma 3, there is an accepting run ρ of T ϕ such that, for all w, w ∈ D * with ρ(w) = ρ(w ), we have trans ρ (w) = trans ρ (w ). For all transitions θ = (s, (s d ) d∈D ) ∈ ∆ , fix λ θ ∈ Λ such that (s, λ θ , (s d ) d∈D ) ∈ ∆. Let t : D * → Λ be the strategy tree defined by t(w) = λ trans ρ (w) .

We have t ∈ L(T ϕ ). Therefore, f t fulfills ϕ, i.e., (2a) holds. It remains to show (2b). Let w, w ∈ D * with δ (ι, f t w ) = δ (ι, f t w ). By induction, we can show that ρ(w) = δ (ι, f t w ) = δ (ι, f t w ) = ρ(w ), i.e., t(w) = t(w ), which proves (2b). Indeed, δ (ι, f t ε ) = ι = ρ(ε) and, for u ∈ D * and d ∈ D, we have δ (ι, 4 From Finite-Memory Distributed Algorithms to Games

f t ud ) = δ (ι, f t u • λ u d ) = δ (δ (ι, f t u ), λ u d ) = δ (ρ(u), λ u d ) = ρ(ud).

Games with Imperfect Information

The existence of finite-memory distributed algorithms shown in Section 3 paves the way for a reduction of the synthesis problem to (2, 1)-player games with imperfect information, where two players form a coalition against an environment in order to fulfill some objective. The main differences between games and the synthesis problem are twofold: Games are played in an arena, on a finite set of nodes (or states), while the input of the synthesis problem is a logical specification. More importantly, in a game, communication between players occurs implicitly, by observing the nodes that are visited. Hence, communication between players is bounded by the finite nature of the arena, whereas in the synthesis problem, processes can send an unbounded amount of information at each communication point. Recall that P = {1, 2} is the set of processes. In the context of games, however, its elements are referred to as players. Definition 4. A (2, 1)-player game is a tuple G = (V, v 0 ,W, Γ, (A p , O p , obs p ) p∈P , τ). Here, V is the finite set of nodes containing the initial node v 0 ∈ V . We assume a Rabin winning condition W ⊆ 2 V × 2 V . Moreover, Γ is the finite set of actions of the environment, A p is the finite set of actions of player p, O p is the finite set of observations of p, and obs p : V × Γ → O p determines what p actually observes for a given node and environment action. Finally, τ :

V × Γ × (A 1 × A 2 ) → V is the transition function.
The game proceeds in rounds r ∈ N, the first round starting in v 0 . When a round starts in v ∈ V , the environment first chooses an action γ ∈ Γ. Players 1 and 2 do not see γ, but only obs 1 (v, γ) and obs 2 (v, γ), respectively. Once the players receive these observations, they simultaneously choose actions a 1 ∈ A 1 and a 2 ∈ A 2 . The next state is τ(v, γ, (a 1 , a 2 )), etc.

Accordingly, a play (starting from v 0 ) is a sequence π = (v 0 , γ 0 )(v 1 , γ 1 ) . . . ∈ (V × Γ) ω such that, for all r ∈ N, there is (a 1 , a 2 ) ∈ A 1 × A 2 such that v r+1 = τ(v r , γ r , (a 1 , a 2 )). The observation that a player p collects in play π until round r is defined as (v 0 , γ 0 ) . . . (v r , γ r ) game p = obs p (v 0 , γ 0 ) . . . obs p (v r , γ r ) ∈ O * p . The play is winning (for the coalition of players 1 and 2) if v 0 v 1 v 2 . . . satisfies the Rabin winning condition in the expected manner.

A strategy for player p is a mapping g p : O + p → A p . A strategy profile is a pair g = (g 1 , g 2 ) of strategies. We say that play π = (v 0 , γ 0 )(v 1 , γ 1 ) . . . is compatible with g if, for all r ∈ N, we have v r+1 = τ(v r , γ r , (a r 1 , a r 2 )) where a r p = g p ( (v 0 , γ 0 ) . . . (v r , γ r ) game p ). Strategy profile g is winning if all plays that are compatible with g are winning.

The following fact has been shown by Peterson and Reif [START_REF] Gary | Multiple-person alternation[END_REF] for games and corresponds to the undecidability result of Pnueli and Rosner [START_REF] Pnueli | Distributed reactive systems are hard to synthesize[END_REF] for two processes without communication.

Fact 2 (Peterson-Reif). The following problem is undecidable: Given a (2, 1)-player game G , is there a winning strategy profile? Therefore, we have to impose a restriction. It turns out that, when we translate the synthesis problem for N = { , } to games in Section 4.2, player 1 (who corresponds to process 1) will have perfect information. We say that player p has perfect information in G if O p = V × Γ and obs p is the identity function.

The following result is by van der Meyden and Wilke [29, Theorem 6] with a proof in [30, Theorem 1].

Fact 3 (van der Meyden-Wilke). The following problem is decidable: Given a (2, 1)-player game G such that player 1 has perfect information, is there a winning strategy profile?

Note that the transition function of our game is deterministic so that we actually obtain decidability in exponential time exploiting a standard technique: We use a small tree automaton to represent the global (full information) winning strategies and another small alternating tree automaton for the local ones of player 2 that conform with some global strategy. The alternating automaton can be checked for nonemptiness in exponential time.

Reduction to Games

The analogies between synthesis and games suggest a natural translation of the former into the latter. However, the crucial difference being the access to histories, we rely on the fact that certain histories in distributed algorithms enjoy a finite abstraction. In fact, it is enough to reveal a bounded amount of information to player 2 at every environment action from Σ . Lemma 5. Let ϕ ∈ LTL(N ) with N = { , }. We can effectively construct a (2, 1)-player game G ϕ such that player 1 has perfect information and the following holds: There is a distributed algorithm that fulfills ϕ iff there is a winning strategy profile in G ϕ .

Proof. By Remark 2, input sequences that do not start with a symbol from Σ are discarded. Hence, we assume that those sequences are all trivially "winning", i.e., (Σ × Ω)(Σ × Ω) ω ⊆ L(ϕ). Let A = (S, ι, δ , F ) be the DRWA according to Lemma 2. Recall that S = S ϕ × 2 S ϕ , where S ϕ is taken from A ϕ , and that the transition function is of the form δ : S × (Σ × Ω) → S.

We construct the game G ϕ = (V, v 0 ,W, Γ, (A p , O p , obs p ) p∈P , τ) as follows. Obviously, player 1 corresponds to process 1 and player 2 to process 2. We simply set V = S and v 0 = ι = (ι ϕ , / 0), and W contains, for all (F ϕ , F ϕ ) ∈ F ϕ , the pair

(F ϕ × 2 S ϕ , F ϕ × 2 S ϕ ).
Moreover, Γ = Σ, the idea being that the environment chooses the inputs and the network graph. Accordingly, processes 1 and 2 choose their outputs so that A 1 = Y 1 and A 2 = Y 2 . Player 1's observations are O 1 = V × Σ and we set obs 1 (s, x 1 x 2 ) = (s, x 1 x 2 ). Thus, player 1 has full information. Player 2's observations are O 2 = (S × Σ ) ∪ Σ ⊥ and we set

obs 2 (s, x 1 x 2 ) = (s, x 1 x 2 ) if = ⊥ x 2 if = .
That is, when the environment chooses a synchronizing input signal, the current state of A is revealed to player 2, which corresponds to passing the (abstracted) history to process 2. Finally, the transitions are given by τ(s, x 1 x 2 , (y 1 , y 2 )) = δ s, ( x 1 x 2 , (y 1 , y 2 )) . Correctness of the reduction is proved in Appendix D.

We have shown Theorem 2 saying that the problem SYNTHESIS({ , }) is decidable.

Complexity. The size of A ϕ is doubly exponential in the length of the formula. It follows that the size of A is triply exponential, and so is the size of G ϕ . Deciding the winner of our (2, 1)-player game where one player has perfect information can be done in exponential time so that the overall decision procedure runs in 4-fold exponential time.

Note that SYNTHESIS({ }), which is equivalent to centralized synthesis in presence of one single process, is 2EXPTIME-complete [START_REF] Pnueli | A framework for the synthesis of reactive modules[END_REF], from which we inherit the best known lower bound for our problem. Moreover, hierarchical information further increases the complexity: for static pipelines with variable number of processes, the problem is no longer elementary [START_REF] Pnueli | Distributed reactive systems are hard to synthesize[END_REF]. However, it may be possible to improve our upper bound, which is left for future work.

As, in the proof, the given LTL formula is translated into a DRWA, synthesis is decidable even when the specification is given by any common finite automaton over ω-words (starting with a nondeterministic Büchi automaton, we actually save one exponential wrt. LTL):

Corollary 1. Over N = { , }, the following problem is decidable: Given an ω-regular language L ⊆ (Σ × Ω) ω , is L realizable?

5 Reduction from { , , } to { , }

In this section, we show decidability for the network model N = { , , }, with input alphabet

Σ = X 1 × N × X 2 and output alphabet Ω = Y 1 × Y 2 .
Recall that this also implies decidability for the network model { , }.

0 1 2 3 4 5 w ⟪w⟫ x 0 x 0 x 1 x 1 x 2 x 2 x 3 x 3 x 4 x 4 x 5 x 5 x 0 x 0 # # x 1 x 1 x 2 x 2 x 3 x 3 x 4 x 4 # # x 5 x 5 0 1 2 3 4 5 6 7
Figure 4:

Illustration of ⟪•⟫ : Σ * → (Σ ) *
The idea is to reduce the problem to the case of the network model N = { , } that we considered in Sections 3 and 4, choosing as input alphabet Σ = X 1 × N × X 2 where X 1 = X 2 = (X 1 ∪ X 2 ) {#}, and as output alphabet

Ω = Y 1 ×Y 2 where Y 1 = Y 2 = (Y 1 ∪Y 2 ) {#}.
To do so, we will rewrite the given specification ϕ ∈ LTL(N ) towards an (automata-based) specification over N in such a way that process 1 can always simulate the "more informed" process and process 2 simulates the other process. Roughly speaking, what we are looking for is a translation ⟪•⟫ : Σ * → (Σ ) * of histories w over N to histories ⟪w⟫ over N such that the view of process 1 in ⟪w⟫ is "congruent" to the view of the more informed process in w, and the view of process 2 in ⟪w⟫ is "congruent" to the view of the less informed process in w. Note that [START_REF] Berwanger | Hierarchical information and the synthesis of distributed strategies[END_REF] also uses a simulation technique to cope with dynamically changing hierarchies.

Example 4. Before defining ⟪•⟫ formally, we illustrate it in Figure 4 for a history w. Round 0 uses so that there is nothing to change. Round 1 employs so that process 1 henceforth simulates process 2 and vice versa. To make sure that the corresponding views in ⟪w⟫ are still "congruent", we insert the dummy signal # # . Actually, the gray-shaded view of process 1 in w after round 2 contains the same information as the gray-shaded view of process 2 in ⟪w⟫ after round 3. Though w encounters in round 3, we decide not to change roles again; we will only do so when facing another (like in round 5).

Formally, ⟪•⟫ : Σ * → (Σ ) * is given by the sequential transducer shown in Figure 5. For the moment, we ignore the red part. A transition with label α | β reads α and transforms it into β . As the transducer is deterministic, it actually defines a function. When we include the red part, i.e., the symbols from Ω and Ω , we obtain an extension to ⟪•⟫ : (Σ × Ω) * → (Σ × Ω ) * . Finally, these mappings are extended to infinite words as expected.

Observe that the state of the transducer reached after reading w ∈ Σ * (or w ∈ (Σ × Ω) * ) reveals the process that process 1 is currently simulating. We denote this process by sim 1 (w). Accordingly, 1 2

x 1 x 2 (y 1 , y 2 ) # # (#, #)
x 2 x 1 (y 2 , y 1 )

x 1 x 2 (y 1 , y 2 ) # # (#, #) x 1 x 2 (y 1 , y 2 ) x 1 x 2 (y 1 , y 2 ) x 1 x 2 (y 1 , y 2 ) x 1 x 2 (y 1 , y 2 ) x 1 x 2 (y 1 , y 2 ) x 1 x 2 (y 1 , y 2 )
x 2 x 1 (y 2 , y 1 )

x 1 x 2 (y 1 , y 2 )

x 2 x 1 (y 2 , y 1 )

Figure 5: The mappings ⟪•⟫ :

Σ * → (Σ ) * and ⟪•⟫ : (Σ × Ω) * → (Σ × Ω ) * sim 2 (w) = 3 -sim 1 (w)
is the process that process 2 simulates after input sequence w. For the example word w in Figure 4, we get sim 1 (w) = 1 and sim 2 (w) = 2. Note that, for all w, w ∈ Σ * and p ∈ {1, 2}, such that w p = w p , we have sim p (w) = sim p (w ). This is because the simulated process only depends on the sequence of links.

Note that the mappings ⟪•⟫ are all injective. Indeed, at the first position that distinguishes w and w , the transducer produces letters that distinguish ⟪w⟫ and ⟪w ⟫. There is an analogous statement for views (proved in Appendix E): Lemma 6. For all w, w ∈ Σ * and p ∈ {1, 2}, the following hold:

(a)

⟪w⟫ p = ⟪w ⟫ p =⇒ w sim p (w) = w sim p (w ) (b) w p = w p =⇒ ⟪w⟫ sim p (w) = ⟪w ⟫ sim p (w )
Moreover, the transducer can be applied to ω-regular languages in the following sense: Lemma 7. Given a DRWA A over the alphabet Σ × Ω, there is a DRWA A over Σ × Ω of linear size such that L(A ) = ⟪L(A )⟫ := {⟪w⟫ | w ∈ L(A )}. Now, decidability for N is due to Lemma 7 and the following result, whose proof crucially relies on injectivity of ⟪•⟫ and Lemma 6 (cf. Appendix F): Lemma 8. Let ϕ ∈ LTL(N ). The following statements are equivalent:

(i) There is a distributed algorithm f (over N ) such that, for all w ∈ Σ ω , f w ∈ L(ϕ).

(ii) There is a distributed algorithm f (over N ) such that, for all w ∈ Σ ω , f ⟪w⟫ ∈ ⟪L(ϕ)⟫.

In other words, an instance ϕ ∈ LTL(N ) of the synthesis problem can be reduced to the existence of a distributed algorithm f over N , Σ , and Ω that fulfills L = M ∪ ⟪L(ϕ)⟫ where M ⊆ (Σ × Ω ) ω is the set of words whose projection to Σ is not contained in ⟪Σ ω ⟫. Using Lemma 7, we obtain a DRWA for L (of doubly exponential size) so that, by Corollary 1, the problem is decidable. Again, the overall procedure runs in 4-fold exponential time.

This concludes the proof of our main result, Theorem 1.

Conclusion

We showed that synthesis in a dynamic, synchronous two-node system is decidable for LTL specifications if and only if the network model does not contain the empty network. Our model covers full-information protocols where nodes communicate their complete unbounded causal history.

Future work is concerned with establishing the precise complexity of our problem and, possibly, improving the 4-fold exponential upper bound. Moreover, it would be interesting to identify the subsets of {-×, , , } ω that give rise to a decidable synthesis problem. For example, one may allow boundedly many empty links in an input sequence. Finally, we plan to extend our model to distributed systems of arbitrary size. We conjecture that synthesis is solvable over a given network model if and only if, in each communication graph, any two nodes are connected via a directed path. This would yield an analogue of the information-fork criterion [START_REF] Finkbeiner | Uniform distributed synthesis[END_REF], which applies to static architectures. It remains to be seen whether the ideas presented in [START_REF] Finkbeiner | Uniform distributed synthesis[END_REF] can be lifted to dynamic architectures with causal memory.

A Proof of Lemma 3 Lemma 3. Let A be a singleton alphabet, D a nonempty (possibly infinite) set of directions, and T an RTA over A-labeled D-trees. Call a run ρ of T on the unique A-labeled D-tree rational if, for all w, w ∈ D * with ρ(w) = ρ(w ), we have trans ρ (w) = trans ρ (w ). If L(T ) = / then there is a rational accepting run of T .

The proof is inspired by [START_REF] Michael | Automata on infinite objects and Church's problem. 13[END_REF][START_REF] Thomas | Automata on Infinite Objects[END_REF] where it is shown that every nonempty language recognized by a classical RTA contains a tree with only finitely many distinct subtress. Note that, here, we deal with trees that are not necessarily bounded branching. Moreover, we show a statement on runs rather than the recognized tree language.

Let T = (S, ι, ∆, F ) be the RTA over A-labeled D-trees. Since A = {a}, we consider the transition relation ∆ to be a subset of S × S D , fixing input a.

Call a state s ∈ S

• absorbing if the only transition in which s occurs is (s, (s

d ) d∈D ) ∈ ∆ with s d = s for all d ∈ D,
• vanishing if it is the initial state ι and has no incoming transition, i.e., there is no transition (s, (s d ) d∈D ) ∈ ∆ with s d = s for some d ∈ D.

• live if it is neither absorbing nor vanishing.

We prove the statement of the theorem by induction on the number of live states in S.

Base case. Suppose there are no live states in S. Let ρ be an accepting run of

T . If ρ(ε) is absorbing, then ρ is rational. If ρ(ε) is vanishing, then ρ(d) is absorbing for all d ∈ D (i.e.
, for all children of the root). Again, it follows that ρ is rational. The base case follows.

Inductive step. Let ρ be an accepting run of T . We distinguish between three cases.

Case 1. There exists a live state s ∈ S that does not appear in ρ. If so, ρ is also an accepting run of the tree automaton T that we obtain from T by removing state s and all transitions in which s occurs. By the induction hypothesis, there exists a rational run ρ of T . But ρ is also a run of T (for all paths ξ in ρ, Inf(ξ ) did not change). The step follows for Case 1.

Case 2. There exists a node u ∈ D * such that s = ρ(u) is live and there exists a state s ∈ S that is live and that does not appear in u's subtree. Define the RTA T 1 obtained from T by removing all transitions from s and adding the "accepting" transition (s, (s d ) d∈D ) where s d = s for all d ∈ D. In fact, the transition is made accepting by adding s to all sets F of (F, F ) ∈ F . By construction, s is absorbing in T 1 . Thus, T 1 has at least one live state (namely s) less. By the induction hypothesis, T 1 has some rational accepting run ρ 1 .

Define another RTA T 2 obtained from T by setting the initial state to s and deleting s from S (as well as all transitions that include s ). Thus, T 2 has at least one live state (namely s ) less. By the induction hypothesis, T 2 has some rational accepting run ρ 2 . Let S 2 be the set of states that occur in ρ 2 . Moreover, for each r ∈ S 2 , let ρ r 2 denote the (unique up to isomorphism) subtree of ρ 2 rooted at an r-node. Note that ρ s 2 = ρ 2 . Next, we define a tree ρ 1 , which we obtain from ρ 1 as follows: Along each path of ρ 1 , we are looking for the first occurrence of a node v such that ρ 1 (v) ∈ S 2 . For every such node v, we replace its subtree by ρ ρ 1 (v) 2 . In particular, every subtree in ρ 1 whose root has state s is replaced by ρ 2 . Observe that ρ 1 is a rational run of T . Further, ρ 1 is accepting: For a path ξ in ρ, we know that it is either a path that stays in ρ 1 (in which case there is

(F, F ) ∈ F with F ∩ Inf(ξ ) = / 0 and F ∩ Inf(ξ ) = / 0),
or it is a path that initially is in ρ 1 and then remains in ρ 2 . In the latter case, Inf(ξ ) is determined only by the suffix ξ 2 in ρ 2 , for which we know that there is (F, F ) ∈ F with F ∩ Inf(ξ 2 ) = / 0 and F ∩ Inf(ξ 2 ) = / 0. The induction step follows for Case 2. Case 3. Otherwise, all live states appear in all subtrees of nodes whose state is live.

Choose a path ξ 0 in ρ such that the set Inf(ξ 0 ) is the set of live states in S. Note that this is possible by assumption of Case 3. Since ρ is accepting, there is a pair (F, F ) ∈ F such that Inf(ξ 0 ) ∩ F = / 0 and Inf(ξ 0 ) ∩ F = / 0. Fix this pair (F, F ) for the remainder of the proof. We observe:

(a) Inf(ξ 0 ) does not contain absorbing or vanishing states.

(b) If nonempty, F only contains absorbing and vanishing states.

(c) Inf(ξ 0 ) ∩ F is nonempty and contains a live state, say, s.

We build a rational run as follows:

Define T 1 as in the second case above. State s is thus absorbing and not a live state in T 1 . Let ρ 1 be an accepting run of T 1 . By the induction hypothesis, we can suppose that ρ 1 is rational.

Define T 3 as T with the following changes: S is replaced by S ∪ {s new } where s new is a fresh "accepting" absorbing state (with corresponding absorbing transition added), each s that appears as s d in a transition ( ŝ, (s d ) d∈D ) in ∆ is replaced by s new , and finally we set s to be the initial state. State s is vanishing and not a live state. State s new is absorbing. Let ρ 3 be a run of T 3 . By the induction hypothesis, we can assume that ρ 3 is rational.

Define run ρ 3,lim as the limit of the following process: Take ρ 3 and replace all subtrees of the nodes whose state is s new with ρ 3 . Let S 3 be the set of states that occur in ρ 3,lim . Moreover, for each r ∈ S 3 , let ρ r 3,lim denote the (unique up to isomorphism) subtree of ρ 3,lim rooted at an r-node. In particular, we have ρ s 3,lim = ρ 3,lim .

Similarly to Case 2, we obtain a tree ρ 1 from ρ 1 as follows: Along each path of ρ 1 , we are looking for the first occurrence of a node u such that ρ 1 (u) ∈ S 3 . For every such node u, we replace its subtree by ρ ρ 1 (u) 3,lim . In particular, every subtree in ρ 1 whose root has state s is replaced by ρ 3,lim .

By construction, ρ 1 is a rational run of T . One also verifies that ρ 1 is accepting: Let ξ be a path in ρ 1 . If the path has a suffix that stays in ρ 1 , acceptance by T follows from acceptance by T 1 . Otherwise, a suffix ξ of ξ remains in ρ 3,lim . If ξ contains a finite number of s, then a suffix of it is in ρ 3 . Acceptance by T follows from acceptance by T 1 .

It remains the case that ξ is in ρ 3,lim and contains s infinitely often. From (c), we have that s ∈ F. Further, Inf(ξ ) cannot contain vanishing states (they have no incoming transitions) and no absorbing states (otherwise, this contradicts the fact that s appears infinitely often). Thus, Inf(ξ ) ⊆ Inf(ξ 0 ). Together with (a) and (b), Inf(ξ ) ∩ F = / 0. It follows that ξ is accepting by T . The induction step follows for Case 3.

B Proof of Claim 1

Claim 1. Let w 0 , w 1 , w 2 , . . . ∈ (Σ × Ω)(Σ × Ω) * . Moreover, let w = w 0 w 1 w 2 . . . be the concatenation of all w i . Set s 0 = ι and, for i ∈ N, s i+1 = ( i+1 , R i+1 ) = δ (ι, w 0 . . . w i ). Then, w ∈ L(A ϕ ) ⇐⇒ the sequence s 0 , s 1 , s 2 , . . . satisfies F ⇐⇒ w ∈ L(A ).

For ∈ S ϕ and w = α 0 . . . α n-1 ∈ (Σ × Ω) * , let

Visit A ϕ ( , w) = {δ ( , α 0 ), . . . , δ ( , α 1 . . . α n-1 )} and λ d 0 d 1 ...d n-1 u ∈ L(A ϕ [ n ]). This implies 1 = δ ϕ (ι ϕ , λ ε d 0 ) 2 = δ ϕ ( 1 , λ d 0 d 1 ) 3 = δ ϕ ( 2 , λ d 0 d 1 d 2 ) . . . n = δ ϕ ( n-1 , λ d 1 ...d n-2 d n-1 ) .
Therefore, together with

λ d 0 d 1 ...d n-1 u ∈ L(A ϕ [ n ]
), we obtain f t w ∈ L(A ϕ ).

• Suppose w = d 0 d 1 d 2 . . . where d 0 , d 1 , d 2 , . . . ∈ Σ Σ * for all n ∈ N. Thus, w contains infinitely many letters from Σ . We have

f t w = λ ε d 0 • λ d 0 d 1 • λ d 0 d 1 d 2 • λ d 0 d 1 d 2 d 3 • . . .
Moreover, we have

s 1 := ρ(d 0 ) = δ (ι, λ ε d 0 ) s 2 := ρ(d 0 d 1 ) = δ (ρ(d 0 ), λ d 0 d 1 ) s 3 := ρ(d 0 d 1 d 2 ) = δ (ρ(d 0 d 1 ), λ d 0 d 1 d 2 ) . . .
As ρ is an accepting run on t, the sequence ι, s 1 , s 2 , . . . satisfies F . By Claim 1, we obtain f t w ∈ L(A ϕ ).

Inclusion ⊇: Suppose t is a strategy tree such that f t fulfills ϕ. Again, for u ∈ D * , let λ u = (λ u 1 , λ u 2 ) refer to t(u). We will construct an accepting run ρ : D * → S of T ϕ on t. First of all, we let ρ(ε) = ι.

Suppose that we defined ρ(u) for u = d 0 d 1 . . . Claim 3. For all u ∈ D * and u ∈ Σ Σ * ∪ Σ Σ ω , the following hold:

f t uu = f t u • λ u u (1)
ρ(u) = δ (ι, f t u ) (2)
Proof of Claim 3. The first statement is due to the definition of f t . The second statement follows from an easy induction on u (see also end of Section 3):

ρ(ε) = δ (ι, ε) ρ(ud) = δ (ρ(u), λ u d ) = δ (δ (ι, f t u ), λ u d ) = δ (ι, f t u • λ u d ) = δ (ι, f t ud )
Note that the last equality is due to [START_REF]I2C-Bus Specification and User Manual[END_REF].

Let u ∈ D * and ( , R) = ρ(u). Let us establish that (ρ(u), λ u , (ρ(ud)) d∈D ) is a transition of T ϕ :

(T1) We have ρ(ud) = δ (ρ(u), λ u d ) by the definition of ρ.

(T2) Let u ∈ Σ Σ ω . As f t fulfills ϕ, we have f t uu ∈ L(A ϕ ). By Claim 3(1),

λ u u ∈ L(A ϕ [δ ϕ (ι ϕ , f t u )]).
By means of Claim 3(2) and the definition of A wrt. to A ϕ , we can deduce λ u u ∈ L(A ϕ [ ]).

Recall that we have

f t w = λ ε d 0 • λ d 0 d 1 • λ d 0 d 1 d 2 • λ d 0 d 1 d 2 d 3 • . . . as well as ρ(d 0 ) = δ (ι, λ ε d 0 ) ρ(d 0 d 1 ) = δ (ρ(d 0 ), λ d 0 d 1 ) ρ(d 0 d 1 d 2 ) = δ (ρ(d 0 d 1 ), λ d 0 d 1 d 2 ) . . . As f t w ∈ L(A ϕ )
, by Claim 1, we have that ξ is accepting.

D Details for Proof of Lemma 5

There are now two directions to show.

Claim 4. If there is a winning strategy profile in G ϕ , then there is a distributed algorithm that fulfills ϕ.

Proof of Claim 4. Let g = (g 1 , g 2 ) be a winning strategy profile in G ϕ , with g p : O + p → Y p . We define ν : Σ * → V and η : Σ * → (V × Σ) * inductively by

ν(ε) = ι η(ε) = ε ν(w x 1 x 2 ) = τ(ν(w), x 1 x 2 , (y 1 , y 2 )) η(w x 1 x 2 ) = η(w) • (ν(w), x 1 x 2 )
where y p = g p ( η(w x 1 x 2 ) game p ). That is, ν(w) is the node which is visited after input word w under strategy profile g, and η(w) is the path corresponding to w in the game, starting at ι and applying g.

For every p ∈ {1, 2} and w ∈ Σ Σ * , we define

f p ( w p ) = g p ( η(w) game p ) .
This is well-defined by construction of the game, using the fact that g is known by both players. Indeed, w 1 = w, then it is possible to compute η(w) game 1 from w 1 . For player 2, one can show inductively that for all w, w ∈ Σ Σ * such that w 2 = w 2 , η(w) game 2 = η(w ) game 2 . Let w = σ 0 σ 1 σ 2 . . . ∈ Σ Σ ω . We have to show that f w ∈ L(ϕ) = L(A ϕ ). Let us determine the sequence s 0 , s 1 , s 2 , . . . of states of A visited while reading f w . Set s 0 = ι and, for every r ∈ N,

s r+1 = δ s r , σ r , f 1 (σ 0 . . . σ r ), f 2 ( σ 0 . . . σ r 2 ) .
For all r ∈ N, we have

s r+1 = δ s r , σ r , f 1 (σ 0 . . . σ r ), f 2 ( σ 0 . . . σ r 2 ) = δ s r , σ r , g 1 (η(σ 0 . . . σ r )), g 2 ( η(σ 0 . . . σ r ) game 2 ) = τ s r , σ r , g 1 (η(σ 0 . . . σ r )), g 2 ( η(σ 0 . . . σ r ) game 2 ) .
Since g is winning and by the winning condition W of the game, we obtain f w ∈ L(A ϕ ), which concludes the proof of Claim 4.

Claim 5. If there is a distributed algorithm that fulfills ϕ, then there is a winning strategy profile in G ϕ .

Proof of Claim 5. Let f = ( f 1 , f 2 ) be a distributed algorithm that fulfills ϕ. Due to Lemma 2, we can assume that for all words w, w ∈ {ε} ∪ Σ Σ * satisfying δ (ι, f w ) = δ (ι, f w ), we have f 2 (wu) = f 2 (w u) for all u ∈ Σ Σ * ⊥ . We have to define a strategy profile g = (g 1 , g 2 ) for the game. Recall that g p : O + p → A p . For every s ∈ S, we will define an "access string" w s ∈ Σ * as follows: Set w ι = ε. Moreover, for s ∈ S \ {ι}, fix any word w s ∈ Σ Σ * such that δ (ι, f w s ) = s. If no such word exists, we let w s = ε.

Note that, if the first environment action is not from Σ , then we can output anything. So fix an arbitrary pair (y 1 , y 2 ) ∈ Y 1 ×Y 2 . Now, g is given as follows:

g 1 :      (V × Σ) + → Y 1 (v 0 , σ 0 ) . . . (v n , σ n ) → f 1 (σ 0 . . . σ n ) if σ 0 ∈ Σ y 1 otherwise g 2 :      O + 2 → Y 2 o → y 2 for o ∈ (Σ ⊥ )O * 2 o • (s, x 1 x 2 ) • u → f 2 (w s • x 1 x 2 • u) for o ∈ {ε} ∪ (S × Σ )O * 2 and u ∈ Σ * ⊥
It remains to show that g is winning. So let π = (s 0 , σ 0 )(s 1 , σ 1 )(s 2 , σ 2 ) . . . be a play that is compatible with g, with s r = ( r , R r ). By our assumption that (Σ × Ω)(Σ × Ω) ω ⊆ L(ϕ), we only need to consider the case σ 0 ∈ Σ . For all r ∈ N, we have

( r+1 , R r+1 ) = τ(( r , R r ), σ r , (a r 1 , a r 2 )) = δ ( r , R r ), (σ r , (a r 1 , a r 2 ))
where a r p = g p ( π ≤r game p

) with π ≤r = (s 0 , σ 0 ) . . . (s r , σ r ). It is enough to show that, for all r ∈ N, we have

( r+1 , R r+1 ) = δ ( r , R r ), σ r , f 1 (σ 0 . . . σ r ), f 2 ( σ 0 . . . σ r 2 ) .
We proceed by induction on the number k of letters from Σ in π ≤r . So suppose

π ≤r = (s 0 , σ 0 ) . . . (s m-1 , σ m-1 ) =: w (s m , x m 1 x m 2 )(s m+1 , x m+1 1 x m+1 2 ) . . . (s r , x r 1 x r 2 ) .
Note that this is well-defined due to Lemma 6(a). We have to show that, for all w ∈ Σ ω , we get f ⟪w⟫ ∈ ⟪L(ϕ)⟫. This follows from the fact that, for all w ∈ Σ * , we have f ⟪w⟫ = ⟪ f w ⟫ which we show by induction (in the following, let f (u) stand for ( f 1 ( u 1 ), f 2 ( u 2 ))):

• From the definitions, we obtain f ⟪ε⟫ = ⟪ f ε ⟫.

• For w ∈ Σ * with sim 1 (w) = 1 and ŵ = w x 1 x 2 (therefore, sim 1 ( ŵ) = 1), we have

f ⟪w x 1 x 2 ⟫ = f ⟪w⟫ x 1 x 2 = f ⟪w⟫ • x 1 x 2 , f (⟪w⟫ x 1 x 2 ) = f ⟪w⟫ • x 1 x 2 , f (⟪ ŵ⟫) (3) = f ⟪w⟫ • x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )) IH = ⟪ f w ⟫ • x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 ))
and from sim 1 ( f w )) = sim 1 (w) = 1 (because the projection of f w to Σ equals w)

= ⟪ f w • ( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )))⟫ = ⟪ f w x 1 x 2 ⟫ = ⟪ f ŵ ⟫ • For w ∈ Σ * with sim 1 (w) = 1 and ŵ = w x 1 x 2 (therefore, sim 1 ( ŵ) = 1), we have f ⟪w x 1 x 2 ⟫ = f ⟪w⟫ x 1 x 2 = f ⟪w⟫ • x 1 x 2 , f (⟪w⟫ x 1 x 2 ) = f ⟪w⟫ • x 1 x 2 , f (⟪ ŵ⟫) (3) = f ⟪w⟫ • x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )) IH = ⟪ f w ⟫ • x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 ))
and from sim 1 ( f w )) = sim 1 (w) = 1

= ⟪ f w • x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )) ⟫ = ⟪ f w x 1 x 2 ⟫ = ⟪ f ŵ ⟫
• For w ∈ Σ * with sim 1 (w) = 1 and ŵ = w x 1 x 2 (therefore, sim 1 ( ŵ) = 2), we have

f ⟪w x 1 x 2 ⟫ = f ⟪w⟫ # # x 2 x 1 = f ⟪w⟫ ( # # , (#, #))( x 2 x 1 , f (⟪w⟫ # # x 2 x 1 )) = f ⟪w⟫ ( # # , (#, #))( x 2 x 1 , f (⟪ ŵ⟫)) (3)
= f ⟪w⟫ ( # # , (#, #))( x 2 x 1 , ( f 2 ( ŵ 2 ), f 1 ( ŵ 1 ))) IH = ⟪ f w ⟫( # # , (#, #))( x 2 x 1 , ( f 2 ( ŵ 2 ), f 1 ( ŵ 1 )))

and from sim 1 ( f w )) = sim 1 (w) = 1 = ⟪ f w ( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )))⟫ = ⟪ f w x 1 x 2 ⟫ = ⟪ f ŵ ⟫

• For w ∈ Σ * with sim 1 (w) = 2 and ŵ = w x 1 x 2 (therefore, sim 1 ( ŵ) = 2), we have f ⟪w x 1 x 2 ⟫ = f ⟪w⟫ x 2 x 1 = f ⟪w⟫ ( x 2 x 1 , f (⟪w⟫ x 2 x 1 )) = f ⟪w⟫ ( x 2 x 1 , f (⟪ ŵ⟫))

(3) = f ⟪w⟫ ( x 2 x 1 , ( f 2 ( ŵ 2 ), f 1 ( ŵ 1 ))) IH = ⟪ f w ⟫( x 2 x 1 , ( f 2 ( ŵ 2 ), f 1 ( ŵ 1 )))

and from sim 1 ( f w )) = sim 1 (w) = 2 = ⟪ f w ( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )))⟫ = ⟪ f w x 1 x 2 ⟫ = ⟪ f ŵ ⟫

• For w ∈ Σ * with sim 1 (w) = 2 and ŵ = w x 1 x 2 (therefore, sim 1 ( ŵ) = 2), we have

f ⟪w x 1 x 2 ⟫ = f ⟪w⟫ x 2 x 1 = f ⟪w⟫ ( x 2 x 1 , f (⟪w⟫ x 2 x 1 )) = f ⟪w⟫ ( x 2 x 1 , f (⟪ ŵ⟫)) (3) = f ⟪w⟫ ( x 2 x 1 , ( f 2 ( ŵ 2 ), f 1 ( ŵ 1 ))) IH = ⟪ f w ⟫( x 2 x 1 , ( f 2 ( ŵ 2 ), f 1 ( ŵ 1 )))
and from sim 1 ( f w )) = sim 1 (w) = 2 = ⟪ f w ( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )))⟫ = ⟪ f w x 1 x 2 ⟫ = ⟪ f ŵ ⟫

• For w ∈ Σ * with sim 1 (w) = 2 and ŵ = w x 1 x 2 (therefore, sim 1 ( ŵ) = 1), we have

f ⟪w x 1 x 2 ⟫ = f ⟪w⟫ # # x 1 x 2 = f ⟪w⟫ ( # # , (#, #))( x 1 x 2 , f (⟪w⟫ # # x 1 x 2 )) = f ⟪w⟫ ( # # , (#, #))( x 1 x 2 , f (⟪ ŵ⟫)) (3)
= f ⟪w⟫ ( # # , (#, #))( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 ))) IH = ⟪ f w ⟫( # # , (#, #))( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )))

and from sim 1 ( f w )) = sim 1 (w) = 2

= ⟪ f w ( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )))⟫ = ⟪ f w x 1 x 2 ⟫ = ⟪ f ŵ ⟫
We next show (ii) → (i). Let f = ( f 1 , f 2 ) be a distributed algorithm over the network model N such that, for all w ∈ Σ ω , f ⟪w⟫ ∈ ⟪L(ϕ)⟫. We can assume that, for all p ∈ P and u ∈ (Σ ) * , we have f p (u # # ) = #. Let f = ( f 1 , f 2 ) be the distributed algorithm over N defined, for all w ∈ Σ + and p ∈ {1, 2}, by f p ( w p ) := f sim p (w) ( ⟪w⟫ sim p (w) ) .

(4) This is well-defined due to Lemma 6(b). We have to show that, for all w ∈ Σ ω , f w ∈ L(ϕ). By injectivity of ⟪•⟫, this follows from the fact that, for all w ∈ Σ * , we have ⟪ f w ⟫ = f ⟪w⟫ .

To show the latter, we again proceed by induction:

• From the definitions, we obtain ⟪ f ε ⟫ = f ⟪ε⟫ .

• For w ∈ Σ * with sim 1 (w) = 1 and ŵ = w x 1 x 2 , we have

⟪ f w x 1 x 2 ⟫ = ⟪ f w ( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )))⟫ (4)
= ⟪ f w ( x 1 x 2 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 )))⟫ and from sim 1 ( f w )) = sim 1 (w) = 1 = ⟪ f w ⟫( x 1 x 2 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 )))

IH = f ⟪w⟫ ( x 1 x 2 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 ))) = f ⟪w x 1 x 2 ⟫ = f ⟪ ŵ⟫
• For w ∈ Σ * with sim 1 (w) = 1 and ŵ = w x 1 x 2 , we have

⟪ f w x 1 x 2 ⟫ = ⟪ f w ( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )))⟫ (4)
= ⟪ f w ( x 1 x 2 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 )))⟫ and from sim 1 ( f w )) = sim 1 (w) = 1 = ⟪ f w ⟫( x 1 x 2 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 ))) IH = f ⟪w⟫ ( x 1 x 2 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 )))

= f ⟪w x 1 x 2 ⟫ = f ⟪ ŵ⟫

• For w ∈ Σ * with sim 1 (w) = 1 and ŵ = w x 1 x 2 , we have

⟪ f w x 1 x 2 ⟫ = ⟪ f w ( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )))⟫ (4)
= ⟪ f w ( x 1 x 2 , ( f 2 ( ⟪ ŵ⟫ 2 ), f 1 ( ⟪ ŵ⟫ 1 )))⟫ and from sim 1 ( f w )) = sim 1 (w) = 1 = ⟪ f w ⟫( # # , (#, #))( x 2 x 1 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 )))

IH = f ⟪w⟫ ( # # , (#, #))( x 2 x 1 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 ))) = f ⟪w⟫ ( # # , (#, #))( x 2 x 1 , ( f 1 ( ⟪w⟫ # # x 2 x 1 1 ), f 2 ( ⟪w⟫ # # x 2 x 1 2 ))) = f ⟪w⟫ # # x 2 x 1 = f ⟪w x 1 x 2 ⟫ = f ⟪ ŵ⟫
• For w ∈ Σ * with sim 1 (w) = 2 and ŵ = w x 1 x 2 , we have

⟪ f w x 1 x 2 ⟫ = ⟪ f w ( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )))⟫ (4)
= ⟪ f w ( x 1 x 2 , ( f 2 ( ⟪ ŵ⟫ 2 ), f 1 ( ⟪ ŵ⟫ 1 )))⟫ and from sim 1 ( f w )) = sim 1 (w) = 2 = ⟪ f w ⟫( x 2 x 1 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 ))) IH = f ⟪w⟫ ( x 2 x 1 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 )))

= f ⟪w⟫ ( x 2 x 1 , ( f 1 ( ⟪w⟫ x 2 x 1 1 ), f 2 ( ⟪w⟫ x 2 x 1 2 )))

= f ⟪w⟫ x 2 x 1 = f ⟪w x 1 x 2 ⟫ = f ⟪ ŵ⟫
• For w ∈ Σ * with sim 1 (w) = 2 and ŵ = w x 1 x 2 , we have

⟪ f w x 1 x 2 ⟫ = ⟪ f w ( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )))⟫ (4)
= ⟪ f w ( x 1 x 2 , ( f 2 ( ⟪ ŵ⟫ 2 ), f 1 ( ⟪ ŵ⟫ 1 )))⟫ and from sim 1 ( f w )) = sim 1 (w) = 2 = ⟪ f w ⟫( x 2 x 1 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 )))

IH = f ⟪w⟫ ( x 2 x 1 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 ))) = f ⟪w⟫ ( x 2 x 1 , ( f 1 ( ⟪w⟫ x 2 x 1 1 ), f 2 ( ⟪w⟫ x 2 x 1 2 ))) = f ⟪w⟫ x 2 x 1 = f ⟪w x 1 x 2 ⟫ = f ⟪ ŵ⟫
• For w ∈ Σ * with sim 1 (w) = 2 and ŵ = w x 1 x 2 , we have

⟪ f w x 1 x 2 ⟫ = ⟪ f w ( x 1 x 2 , ( f 1 ( ŵ 1 ), f 2 ( ŵ 2 )))⟫ (4)
= ⟪ f w ( x 1 x 2 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 )))⟫ and from sim 1 ( f w )) = sim 1 (w) = 2 = ⟪ f w ⟫( # # , (#, #))( x 1 x 2 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 )))

IH = f ⟪w⟫ ( # # , (#, #))( x 1 x 2 , ( f 1 ( ⟪ ŵ⟫ 1 ), f 2 ( ⟪ ŵ⟫ 2 ))) = f ⟪w⟫ ( # # , (#, #))( x 1 x 2 , ( f 1 ( ⟪w⟫ # # x 1 x 2 1 ), f 2 ( ⟪w⟫ # # x 1 x 2 2 ))) = f ⟪w⟫ # # x 1 x 2 = f ⟪w x 1 x 2 ⟫ = f ⟪ ŵ⟫

Definition 3 .

 3 A (nondeterministic) Rabin tree automaton (RTA) over A-labeled D-trees is a tuple T = (S, ι, ∆, F ) with finite set of states S, initial state ι ∈ S, acceptance condition F ⊆ 2 S × 2 S , and (possibly infinite) set of transitions ∆ ⊆ S × A × S D .

Figure 3 :

 3 Figure 3: A strategy tree t.

  The last equation is by (T1) in the definition of the transition relation ∆ of T ϕ .

d n- 1 ∈

 1 D * where d 0 , . . . , d n-1 ∈ D = Σ Σ * , with n ∈ N. For d ∈ D, we let ρ(ud) = δ (ρ(u), λ u d ) .

Finally, we show

  that ρ is accepting. Let d 0 , d 1 , d 2 , . . . ∈ D and consider the path ξ = d 0 d 1 d 2 . . . along with the induced infinite sequence ρ(ε), ρ(d 0 ), ρ(d 0 d 1 ), ρ(d 0 d 1 d 2 ), ρ(d 0 d 1 d 2 d 3 ), . . .

  |= Gϕ if ∀r ≥ 0 : e ≥r |= ϕ e |= ϕUψ if ∃r ≥ 0 : e ≥r |= ψ ∧ ∀0 ≤ r < r : e ≥r |= ϕ

			e ≥1 |= ϕ
	e |= (out p = y) if y 0 p = y	e |= Fϕ if ∃r ≥ 0 : e ≥r |= ϕ
	e |= (link = ) if	0 =	e

Acknowledgment. We thank Dietmar Berwanger for valuable feedback. This work was partly supported by ANR FREDDA (ANR-17-CE40-0013).

Synthesis in Presence of Dynamic Links be the set of states that are traversed by A when reading w. Note that Visit A ϕ ( , w) does not necessarily contain . For all i ∈ N, we have R i+1 = Visit A ϕ ( i , w i ). With this, we get:

Visit A ϕ ( i , w i ) ∩ F = / 0 for infinitely many i ≥ 0 Visit A ϕ ( i , w i ) ∩ F = / 0 for finitely many i ≥ 0 ⇐⇒ ∃(F, F ) ∈ F ϕ : R i+1 ∩ F = / 0 for infinitely many i ≥ 0 R i+1 ∩ F = / 0 for finitely many i ≥ 0 ⇐⇒ ∃(F, F ) ∈ F ϕ : s i+1 ∈ G F for infinitely many i ≥ 0 s i+1 ∈ G F for finitely many i ≥ 0 ⇐⇒ the sequence s 0 , s 1 , s 2 , . . . satisfies the acceptance condition

The last equivalence is due to the fact that the R-component is monotonically increasing when A is reading a word α 0 . . .

C Correctness of T ϕ

We will show L(T ϕ ) = {t | t is a strategy tree such that f t fulfills ϕ}.

We have to consider two inclusions:

There is an accepting run ρ : D * → S of T ϕ on t. Let w ∈ Σ Σ ω . We will show, using Claim 1, that f t w ∈ L(A ϕ ).

• Suppose w = d 0 d 1 . . . d n-1 u where d 0 , . . . , d n-1 ∈ Σ Σ * , with n ∈ N, and u ∈ Σ Σ ω . In particular, seen as a word over Σ, w contains only finitely many letters from Σ . We have

By the definition of ∆, we have

Synthesis in Presence of Dynamic Links

Then,

Equation ( * ) is trivial for m = 0 (i.e., k = 1), as then w s m = ε (by definition). Otherwise, it follows from the induction hypothesis: The word σ 0 . . .

).

E Proof of Lemma 6

Lemma 6. For all w, w ∈ Σ * and p ∈ {1, 2}, the following hold:

Part (a)

First, assume p = 1. Observe that for w ∈ Σ * , ⟪w⟫ ∈ (Σ ) * . Further, within the domain (Σ ) * , • 1 is the identity. Together with the injectivity of ⟪•⟫, ⟪w⟫ p = ⟪w ⟫ p implies w = w ; the lemma's statement follows for p = 1.

Second, assume p = 2 and that ⟪w⟫ 2 = ⟪w ⟫ 2 . For p ∈ P, let ⟪•⟫ p denote the transduction defined by the same transducer but with initial state p . In particular, we have ⟪•⟫ = ⟪•⟫ 1 . We start by observing that the function • 2 is length preserving and the projection onto a sequence of communication graphs is the same in ⟪w⟫ and ⟪w ⟫. Moreover, the latter are of the form

• Suppose û = σ = ε. Then, by the definition of ⟪•⟫, we have w = v and w = v . We deduce w sim 2 (w) = w sim 2 (w ) with sim 2 (w) = 2.

• Suppose that ε = σ = χ 1 χ 2 = # # . Then, w = uv and w = u v for some u, v, u , v such that ⟪u⟫ = û and ⟪u ⟫ = û and ⟪v⟫ sim 1 (u) = σ v and ⟪v ⟫ sim 1 (u) = σ v . By injectivity of ⟪•⟫, we have u = u .

-Suppose sim 1 (u) = 1, i.e., sim 2 (u) = 2. By the definition of ⟪•⟫, we obtain v = σ v and v = σ v . Therefore, w 2 = w 2 = u σ ⊥ x 1 . . . ⊥ x n .

-Suppose sim 1 (u) = 2, i.e., sim 2 (u) = 1. By the definition of ⟪•⟫, we can deduce that

• Suppose that σ = # # . Then, n ≥ 1. Moreover, w = uv and w = u v for some u, v, u , v such that ⟪u⟫ = û and ⟪u ⟫ = û and ⟪v⟫ sim 1 (u) = σ v and ⟪v ⟫ sim 1 (u) = σ v . By injectivity of ⟪•⟫, we have u = u .

-Suppose sim 1 (u) = 1. By the definition of ⟪•⟫, we obtain v = x 1 z 1 . . . x n z n and v = x 1 z 1 . . . x n z n . Therefore, sim 2 (w) = sim 2 (w ) = 1. We have that

Part (b)

Suppose w p = w p . Note that this implies sim p (w) = sim p (w ) =: p w .

First, assume that one of the following holds:

Then, w = w and we are done.

For the remaining cases, we proceed by induction. The statement is obvious for w = ε. Now, assume w = u x 1 x 2 and p = 2. Then, p w = 2 and w 2 = u 2 ⊥ x 2 = w 2 . Thus, we have w = u x 1 x 2 for some u and x 1 such that u 2 = u 2 . The latter implies sim 2 (u) = sim 2 (u ) =: p u . By induction hypothesis, we get ⟪u⟫ p u = ⟪u ⟫ p u .

Suppose p u = 1. Then,

and from p u = 1 and

Suppose p u = 2. Then,

Synthesis in Presence of Dynamic Links and by induction hypothesis

Now, assume w = u x 1 x 2 and p = 1. Then, p w = 2 and w 1 = u 1 x 1 ⊥ = w 1 . Thus, we have w = u x 1 x 2 for some u and x 2 such that u 1 = u 1 . The latter implies sim 1 (u) = sim 1 (u ) =: p u . By induction hypothesis, we get ⟪u⟫ p u = ⟪u ⟫ p u .

Suppose p u = 1. Then,

and from p u = 1 and

and by induction hypothesis

Lemma 8. Let ϕ ∈ LTL(N ). The following statements are equivalent:

(i) There is a distributed algorithm f (over N ) such that, for all w ∈ Σ ω , f w ∈ L(ϕ).

(ii) There is a distributed algorithm f (over N ) such that, for all w ∈ Σ ω , f ⟪w⟫ ∈ ⟪L(ϕ)⟫.

We start by showing (i) → (ii). Let f = ( f 1 , f 2 ) be a distributed algorithm over N that fulfills L(ϕ). Let f = ( f 1 , f 2 ) be a distributed algorithm over N such that, for all w ∈ Σ + , w ∈ (Σ ) + , and p ∈ {1, 2}, f p ( ⟪w⟫ p ) := f sim p (w) ( w sim p (w) ) f p (w # # ) := # .

(3)