Distributed LTL Synthesis under Arbitrary Message Adversaries

Distributed LTL Synthesis under Arbitrary Message Adversaries Benedikt Bollig1 Patricia Bouyer-Decitre1 1 Dhrubajyoti Ghosh Thomas Nowak1,2

arXiv:2611.04561v1 [cs.DC] 3 Nov 2026

1

Matthias Függer1 Nathalie Sznajder3

Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF 2 Institut Universitaire de France 3 Sorbonne Université, CNRS, LIP6 Abstract

Reactive synthesis is the problem of generating a program that produces outputs satisfying a logical specification for every input stream. We study distributed synthesis for two processes communicating in rounds over unreliable links, with at least one message delivered in every round. Despite this delivery guarantee, we show that synthesis from linear temporal logic specifications is undecidable, even when messages carry the processes’ complete causal histories. More generally, we give a complete characterization of the communication restrictions that make synthesis decidable. Restrictions are described by a message adversary A, a set of allowed infinite graph histories: sequences of communication graphs, each specifying which messages are delivered in a round. Iterated chromatic subdivision associates these histories with points in the unit interval, yielding an image π(A) ⊆ [0, 1]. For every ω-regular message adversary A, synthesis is decidable if and only if π(A) is nowhere dense. In the decidable cases, our procedure takes a deterministic parity automaton for A and a specification, decides realizability, and constructs a realizing distributed algorithm whenever one exists. Further, our topological arguments shed new light on the fundamental requirements of synthesis. They show that, for ω-regular message adversaries, synthesis is decidable if and only if consensus is repeatedly solvable in bounded time. This links two previously unrelated problems from formal verification and distributed computing through the processes’ uncertainty about communication.

1

Introduction

Reactive synthesis asks for an algorithm that, given a logical specification, constructs a program satisfying it for every input stream, or determines that no such program exists. It addresses a fundamental question in reactive-system design: how to ensure correctness of a program by construction. The problem was introduced by Church [Chu57, Chu63]. In its standard formulation, the input and output alphabets are finite, and the specification is given in monadic second-order logic (MSO) over infinite words. The output program to be constructed is a finite-state transducer that reads one input symbol and produces one output symbol per round. Büchi and Landweber [BL69] proved decidability by viewing synthesis as an infinite game between the environment, which chooses inputs, and a controller, which chooses outputs. A winning strategy for the controller defines a program satisfying the specification. Shortly after, Rabin [Rab72] provided an alternative proof using tree automata, exploiting the tree structure naturally formed by the finite prefixes of a program’s possible executions. Church’s synthesis problem has received sustained attention and has been extended in many directions [Tho08, BCJ18, Fij26]. An extension of particular relevance to distributed systems is synthesis under imperfect information, where a single process observes only part of the input [KV97, AVW03]. Pnueli and Rosner [PR90] posed the question for the distributed setting in which several processes, each observing only part of the input, must jointly realize a global specification. They proved that distributed synthesis is undecidable even for specifications in linear temporal logic (LTL) [Pnu77] and an architecture consisting of just two processes, each receiving a different part of the input and unable to communicate with the other. By contrast, synthesis is decidable for pipeline architectures, in which processes can send messages only to their right neighbor along a line, and only the first process receives external input from the environment. The proof successively eliminates processes from the pipeline, using tree automata to reduce the problem to synthesis for a single process. Kupferman and Vardi [KV01] extended decidability to further architectures and Finkbeiner and Schewe [FS05] gave a complete characterization: the problem is decidable if and only if the architecture has no information fork. Distributed synthesis has also been studied for knowledge-based specifications [vdMW05]. A recurring condition behind decidability in synchronous distributed synthesis is hierarchical information: calling a process p more informed than process q if it can deduce the information of q from its own, information is hierarchical if all processes can be linearly ordered with respect to informedness. Undecidability thus stems from processes holding incomparable information that they cannot reconcile: sharing information between processes is essential to solving the problem. This observation led Gastin, Sznajder, and Zeitoun [GSZ09] to consider specifications that refer only to external inputs and outputs, and not to the communication channels between processes: processes are then free to use these channels to share information, which made it possible to extend the class of decidable architectures. Asynchronous models push this idea further with causal memory: whenever processes synchronize, they exchange their entire causal histories, so that each process knows everything that causally precedes its current state. Synthesis is then decidable for restricted architectures, such as series-parallel systems [GLZ04] or tree architectures [GGMW13, MW14], but even this maximal form of information sharing does not make the problem decidable in general [Gim22]. In synchronous models, another way to relax the rigidity of hierarchical information is to let the hierarchy itself evolve. Indeed, many distributed systems lack such a fixed hierarchy since communication is sporadic and process and communication faults may occur. Moreover, even if it exists, it may be unknown to the processes. Berwanger, Mathew, and van den Bogaard [BMvdB15] studied synthesis in finite games where processes retain their entire observation history and the information hierarchy may change during play. Observations in each round range over fixed finite alphabets, so the model does not directly capture messages carrying arbitrarily long causal histories. Specifications are given by finite automata and depend only on signals observable to all processes. They proved decidability in this setting and showed that each process can infer its position in the hierarchy from its own observation history. The message adversary model [CBS09, AG15] unifies several widely used communication models from the theory of distributed computing, including process crashes and message losses by specifying which messages are received in each round by which process. Reception of a message is expressed as an edge in a directed 1

communication graph, which may change in each round. The adversary is the set of allowed infinite graph histories. In distributed computing, such submodels are used to study which problems can be solved under given communication assumptions. LTL can express commonly used message adversaries and decision tasks as well as long-lived tasks such as repeated consensus [Lam98] and clock synchronization [ST87]. Bérard, Bollig, Bouyer, Függer, and Sznajder [BBB+ 22] studied synthesis for two processes and an unstable communication between them, however, additionally assuming acknowledgments that make each round’s communication graph immediately known to both processes. They allowed messages to carry their complete causal histories, allowing for the synthesis of full information protocols that are not restricted to bounded messages. They proved that, for ω-regular message adversaries, synthesis is decidable if and only if the number of consecutive rounds in which no message is delivered is uniformly bounded. The acknowledgment assumption changes the solvability of even basic tasks, though. For example, two processes can solve consensus in one round if at least one message is delivered and both processes know the communication graph. The decidability of synthesis without this assumption thus remained open. We resolve this question and characterize the message adversaries for which synthesis is decidable in the general case for message adversaries as they are studied in the theory of distributed computing. We develop a new topological approach to establish this characterization. have machine-checked proofs in Lean 4 using Mathlib (v4.30.0). Each Results marked with Lean proof badge links to a dedicated Lean file containing the corresponding statement. Badges of the form on definitions and in the Model and Lossy-Link Synthesis Problem subsections link directly to Lean their formal counterparts. The formalization only supplements the natural-language proofs in this paper and is not meant to replace them. A short overview is given in Appendix B. VERIFIED

FORMALIZED

1.1

Our Results

In this paper, we study the synthesis problem of distributed algorithms for two processes under arbitrary message adversaries. We assume that message adversaries are ω-regular and given by a parity automaton. In particular, any LTL-definable message adversary is covered by our results. This class includes all oblivious message adversaries [CGP15], which have been shown to capture the computational power of synchronous and asynchronous models of computation, with processes communicating via shared registers [AG15] and message passing [CBS09], both without and with process faults [ACGN26]. The class also includes models of dynamic communication networks [CFQS12], including ones with eventual stabilization guarantees [WSS19]. Authentication tells a recipient where a message came from, but need not tell its sender whether it arrived. This distinction also appears in cryptographic channel abstractions, where authenticated communication may leave message delivery under adversarial control [KMTZ13, Section 3.1]. Consider two honest parties, Alice and Bob, communicating over such unreliable links. Even if they exchange their complete causal histories, Alice may remain uncertain whether Bob received her latest message. More precisely, we consider submodels of the lossy link (LL) model [SWK09]. In this model, any infinite graph history over the set Γ = {(1 ← 2), (1 → 2), (1 ↔ 2)} can occur. The parity automaton defining this message adversary is trivial. In the LL model, the consensus problem is not solvable [SW89], but approximate consensus is [CBFN15]. Our first result is the undecidability of distributed synthesis in the LL model: Theorem 1.1 (

VERIFIED

Lean

). The LL-Synthesis problem is undecidable.

To characterize decidability for arbitrary message adversaries, we use the map π : Γω → [0, 1] from infinite graph histories into the unit interval, defined by the limit of the iterated chromatic subdivision of the unit interval, which describes the set of possible local views of both processes [HKR14, GP20]. Decidability of the synthesis problem under a message adversary depends on a topological property of its image in the unit interval: VERIFIED

Theorem 1.2 ( Lean ). Let A be an ω-regular message adversary. The LL-Synthesis(A) problem is decidable if and only if π(A) is nowhere dense.

2

A subset of [0, 1] is nowhere dense if its closure contains no interval of positive length. This is a generalization of Theorem 1.1 since the full LL message adversary A = Γω maps to the full unit interval π(A) = [0, 1], which is not nowhere dense. The decidability direction is constructive and uniform in the message adversary: given a deterministic parity automaton for A with nowhere-dense image π(A) and an LTL formula ϕ, our procedure decides whether ϕ is realizable under A and constructs a realizing distributed algorithm whenever one exists. Key to our decidability result is a connection underlying our characterization between the decidability of synthesis and the repeated solvability of consensus in bounded time. While hierarchical information allows one to solve consensus, the reverse is not true. Our decidability result does not require hierarchical information in each round and holds for adversaries where this is not given. In fact we show that repeated solvability of consensus in bounded time is precisely what is required to solve synthesis. This sheds new light on the nature of reactive synthesis.

1.2

Our Techniques

The proofs presented in this work are based on several new techniques that we summarize in the following. Central to both directions of Theorem 1.2 is the use of the view complex, the graph whose vertices are the possible local views after round r and whose edges are the possible executions up to that round. Distributed algorithms are naturally expressed as labeling each vertex with an output in this formalism. Undecidability via encoding a 2-counter machine in a set of executions To show undecidability, we reduce from the non-halting problem for 2-counter machines [Min67]. In contrast to the undecidability result of Pnueli and Rosner [PR90], our technique does not use independent inputs, but uses the very uncertainty about the system, in our case the communication graphs, to store unbounded integers. Counters turn out to be particularly well suited to be encoded in such uncertainties. The difficulty of this proof approach, however, lies in the fact that process output alphabets are finite, and thus no single execution round can store an unbounded counter value. We therefore distribute the value over all executions of a round: every edge of the round-r path carries one binary weight per counter, and a counter with value c at step r − 1 of the run is represented by a fraction 3−c of edges with weight 1. An increment, a no-op, and a decrement multiply the number of weight-1 edges by 1, 3, and 9, respectively. All vertices of a round additionally output the current control state of the machine and a claim on whether each counter is zero (claim, since this is impossible to test locally, too), so that the sequence of labeled paths encodes the run. Local indistinguishability enables LTL formulas to relate neighboring executions An LTL formula is evaluated on one execution at a time, so in each round it can only compare the outputs at the two endpoints of a single edge. However, to encode unbounded counter sizes, we need to argue about an unbounded number of executions in our formulas. For this we use the fact that processes inherently are forced to behave identically on identical views: the output of a process is a function of its view, and adjacent edges in a view complex share a view. Constraints on individual executions thus propagate along the path and become global constraints on a round. For example, if both processes must always output the same control state and zero claims, then all vertices of a round do. Safety formulas only depend on the closure of an adversary The formula of the undecidability reduction is a safety formula. A violation of such a formula shows after finitely many rounds, and every finite prefix of a history in the closure A is also a prefix of a history in A. Thus an algorithm realizes a safety formula under A if and only if it does so under A: liveness guarantees of an adversary, such as eventual stabilization, do not help for safety specifications. If π(A) is not nowhere dense, then there is a finite graph history h all of whose extensions are prefixes of histories in A, which means that h · Γω ⊆ A. Guarding the formula by “if the graph history starts with h, then the formula holds from round |h| + 1 on” reduces synthesis under the full adversary to synthesis under A, yielding the undecidability direction of Theorem 1.2.

3

Counters require growing uncertainty about the graphs For decidability, we organize connected subgraphs of complexes into a tree and bound their size while preserving the existence of a realizing algorithm. Without inputs and under the full adversary, it is a path with 3r edges, one for each graph history in Γr . If π(A) is not nowhere dense, for which we show undecidability, the complex under A contains arbitrarily long subpaths, which can store the unbounded counters. If π(A) is nowhere dense, the path breaks up into connected components of uniformly bounded size, and our decision procedure exploits this fragmentation. In fact we show that this breaking-into-pieces is directly related to the consensus problem, showing a new relation between consensus and synthesis that was previously unknown. Relating nowhere denseness to repeated consensus solvability Consensus is solvable under A if and only if π(A) ̸= [0, 1] [CG23]. A bounded-time algorithm cannot tell A from its closure, and compactness turns termination under a closed adversary into a uniform round bound. Thus consensus is solvable in bounded time if and only if π(A) is not dense. Removing a finite prefix amounts to rescaling its interval to [0, 1], so consensus is solvable in bounded time after every live prefix if and only if π(A) is nowhere dense. For an ω-regular adversary, finitely many distinct left quotients yield a uniform bound D, computable by exhaustive search. The same bound allows agreement on a broadcaster after each prefix. We use this agreement to show that all histories in a component at round r ≥ D share the view of one process p at round r − D, and the other process has heard from p since then. In this sense, the processes recover a form of hierarchical information, with a delay of D rounds and a hierarchy that can change over time. Synthesis via trees of components We represent an algorithm by a tree whose nodes store connected subgraphs of the view complex at rounds nD, with automaton states on their edges. At each node, we specify what each process outputs in the next D rounds for every possible local view. After these D rounds, each connected component under A becomes a child node. Different components remain disjoint under extension, so their output choices cannot conflict on the same local view. A branch follows a sequence of components. Based on this, we define a run as a sequence of edges along a branch. The tree accepts if every run satisfies the parity condition for the guarded objective: the graph history lies outside A, or the execution satisfies ϕ. We then show that accepting component trees correspond exactly to realizing algorithms. However, this approach faces a challenge: inputs can make their components arbitrarily large, e.g., under A = {(1 → 2)ω } and a fixed input sequence of process 1, the round-r component is a star with one edge for every input sequence of process 2. Decidability via reductions To address this, we replace each component K by a subgraph of bounded size, using a reduction r : K → K that preserves the state labels. The next block then starts from r(K). Using the common earlier view, we reduce each component to a bounded number of representative edges while preserving local indistinguishability and state labels. The main difficulty is preserving acceptance. Repeated replacements can create runs that do not correspond to executions of the original algorithm. We choose representatives of minimum ordinal rank to preserve parity, following the progress-measure argument of Berwanger, Mathew, and Ramanujam [BMR16]. The resulting components have uniformly bounded size, so only finitely many labeled components, reductions, and block transitions remain up to isomorphism. We express local consistency and acceptance of every compatible run in MSO. Rabin’s theorem [Rab69] then decides whether an accepting tree exists and, if so, provides a finite description of one. From this tree, we construct a realizing distributed algorithm.

2

Model and Problem

2.1

Model

FORMALIZED

Lean

Fix the set of processes to be P := {1, 2}. Every process p ∈ P is assigned finite nonempty sets Xp and Yp of possible inputs and outputs respectively. We consider systems where computation and communication proceed in rounds. In round r ≥ 1, process p ∈ P obtains input xp [r] ∈ Xp from the environment (different 4

vp (h) g = (1 → 2) g = (1 ↔ 2) g = (1 ← 2)

p=1 N1 (x1 , u) C1 (x1 , u, x2 , v) C1 (x1 , u, x2 , v)

p=2 C2 (x2 , v, x1 , u) C2 (x2 , v, x1 , u) N2 (x2 , v)

Table 1: Recursive view updates for h = h′ · (x1 , x2 , g), with current inputs x1 , x2 , communication graph g, and previous views u := v1 (h′ ), v := v2 (h′ ). from the processes), sends and receives messages, does a compute step, and finally outputs yp [r] ∈ Yp . We allow processes to send all their knowledge, including their own inputs and messages received so far, without a bound on message size. The value of yp [r] depends on the knowledge acquired by p through round r and is formalized in the next section. The set of possible communication graphs is Γ := {(1 → 2), (1 ↔ 2), (1 ← 2)}. A graph history h ∈ Γ∗ ∪Γω is a finite or infinite sequence of communication graphs. Its r-th graph, denoted h[r], is the communication graph of round r. If h[r] = (1 → 2), then only process 2 hears from process 1 in round r; if h[r] = (1 ← 2), then only process 1 hears from process 2; and if h[r] = (1 ↔ 2), then both processes hear from each other. A message adversary A ⊆ Γω describes the set of possible infinite graph histories that can occur in a system. We call the message adversary A = Γω the full message adversary. Given a process p ∈ P, we write p̄ := 3 − p for the other process.

2.2

Histories and Indistinguishability Relations

Define the set of input signals to be Σ := X1 × X2 × Γ. An input signal (x1 , x2 , g) occurring in round r means that process p receives input xp from the environment and that the communication graph of round r is g. An input signal history h ∈ Σ∗ ∪ Σω is a finite or infinite sequence of input signals. For a finite history u and a finite or infinite history w over the same alphabet, we write u · w or simply uw for their concatenation. We write |h| for the length of a finite history h. For a finite or infinite word h and an integer r ≥ 1, we write h[r] for its r-th letter and h[r . . . ] for the suffix beginning with that letter. For an integer r ≥ 0, we write h[. . . r] for its prefix of length r, with h[. . . 0] = ε. When h is finite, these notations Sb require r ≤ |h|. For integers 0 ≤ a ≤ b, we write Σ[a,b] := t=a Σt . For a language L of infinite words, let Pref(L) denote its set of finite prefixes and Pref r (L) its set of prefixes of length r. We assume that messages contain the sender’s current input and its entire previous view. A view records all information acquired through local inputs and received messages. Once communication is described in this way, a distributed algorithm is determined by its choice of output for each possible local view. In particular, histories that give a process the same view must lead that process to produce the same output, even when those histories require different behavior from a process with access to the global execution. Given a history h ∈ Σ∗ , the view of process p at the end of h, denoted by vp (h), is a labeled tuple defined recursively. Symbols I1 , I2 refer to the initial views of processes 1 and 2, which are simply their own process identifiers. Symbols Np , Cp are taken to mean no-communication and communication respectively and are used to label the tuples. For h = ε, define vp (h) := Ip . Otherwise suppose that h = h′ · (x1 , x2 , g), i.e., h has h′ as a prefix and (x1 , x2 , g) as its last letter. Suppose that v1 (h′ ) = u and v2 (h′ ) = v. Table 1 defines vp (h). Let Viewsp := {vp (h) | h ∈ Σ∗ } be the set of possible views of process p. Define histories h1 and h2 to be indistinguishable to process p, or h1 ∼p h2 , if vp (h1 ) = vp (h2 ). If two histories are indistinguishable to a process in round r + 1, it must be so in round r as well: VERIFIED

Lemma 2.1 ( Lean ). Suppose that h = h0 · (x1 , x2 , g) and h′ = h′0 · (x′1 , x′2 , g ′ ). If h ∼p h′ then h0 ∼p h′0 , and moreover p has an incoming arrow in both g and g ′ or it does not have an incoming arrow in either graph. Proof. Assume that p = 1; the case p = 2 follows similarly. The proof that h0 ∼1 h′0 follows from the fact that each of N1 (x1 , u) = N1 (x′1 , u′ ) and C1 (x1 , u, x2 , v) = C1 (x′1 , u′ , x′2 , v ′ ) implies that u = u′ . 5

If v1 (h) = v1 (h′ ) are of the form N1 (·, ·), then g and g ′ are both of the form (1 → 2). Otherwise they are of the form C1 (·, ·, ·, ·), in which case g and g ′ belong to {(1 ↔ 2), (1 ← 2)}, proving the latter claim.

2.3

Lossy-Link Synthesis Problem

FORMALIZED

Lean

We study the problem of synthesizing a distributed algorithm whose behavior is specified by an LTL formula. The formulas can talk about process inputs, process outputs, and communication graphs at each round. The syntax and semantics are given in Appendix A. In principle, the graph history in an execution is arbitrary from Γω , modeling a highly dynamic network without any restrictions on stability, eventual convergence, etc. The specification is allowed to speak about the communication graphs along a history, however, with the possibility to restrict the behavior of the dynamic network and require process behavior to depend on the network dynamics. A distributed algorithm f is a pair (f1 , f2 ) of functions f1 : Views1 → Y1 and f2 : Views2 → Y2 that associate with each view an output. Given h ∈ Σω , define hr := h[. . . r]. Let Ω := Y1 × Y2 be the set of output signals. The execution of f on h, denoted exec(f, h), has alphabet Σ × Ω with rth letter (h[r], (y1 [r], y2 [r])) , where y1 [r] := f1 (v1 (hr )) and y2 [r] := f2 (v2 (hr )). Define Graph : Σω → Γω to project input signal histories to their graph histories. For h ∈ Σω and r ≥ 1, we have Graph(h)[r] = g whenever h[r] = (x1 , x2 , g). We extend Graph to finite input signal histories by the same round-wise projection, with Graph(ε) = ε. For an execution e ∈ (Σ × Ω)ω , we likewise write Graph(e) for its graph history, ignoring inputs and outputs. For a message adversary A and a language L ⊆ (Σ × Ω)ω , we say that f LL-realizes L under A if exec(f, h) ∈ L for every h ∈ Σω with Graph(h) ∈ A. The language L is LL-realizable under A if such an algorithm exists. For an LTL formula ϕ, these notions apply to L(ϕ) := {e ∈ (Σ × Ω)ω | e |= ϕ}. Unless an adversary is specified, realizability refers to the full adversary Γω ; we henceforth omit the prefix “LL-”. asks, given an LTL formula ϕ, whether ϕ The synthesis decision problem LL-Synthesis(A) Lean is realizable under A. We write LL-Synthesis for the case A = Γω . Lean FORMALIZED

FORMALIZED

2.4

View Complexes

View complexes represent the processes’ indistinguishability relations as a graph. Each vertex represents a possible view of one process (we then say that said process owns that vertex), and an edge joins two views that can occur together. Histories whose edges share a vertex are indistinguishable to the process owning that vertex. A path consequently represents a sequence of histories linked by individual indistinguishability. Since we have only two processes, the view complex is a graph rather than a higher-dimensional simplicial complex [HKR14]. Let A be a message adversary and let r ≥ 0 be a round number. Let Views(A) p (r) := {vp (h) | h ∈ r Σ , Graph(h) ∈ Pref(A)} be the set of possible views of process p under A after r rounds. The view (A) (A) complex under A after round r is defined as the graph with the vertex set Views1 (r) ∪ Views2 (r) and the edges {v1 (h), v2 (h)} where h ∈ Σr and Graph(h) ∈ Pref(A). The uncertainty of process p about the state of the other process p̄ is formalized as the set of views adjacent to its own. Write e(h) := {v1 (h), v2 (h)} for the edge associated with a history h. The pair of views determines the history: by Table 1, it determines the last communication graph, both inputs, and both preceding views. Repeating this reconstruction determines every letter of h. Thus distinct histories give distinct edges. FORMALIZED

Definition 2.2 (View complex with output ). The view complex after round r is labeled with Lean output if each vertex of process p is labeled with a value from Yp . A distributed algorithm f assigns the output label fp (u) to every vertex u of process p. Conversely, define fp (u) as the label of the process-p vertex u. This is well-defined across rounds because a view determines its process and round. Assign arbitrary outputs to views that cannot occur under A. 6

I1

I2

ε

round 0 v1 (h)

v2 (h)

h

round r h0 = h(1 → 2)

h1 = h(1 ↔ 2)

h2 = h(1 ← 2)

round r + 1 h0 (1 → 2) h0 (1 ↔ 2) h0 (1 ← 2) h1 (1 ← 2) h1 (1 ↔ 2) h1 (1 → 2) h2 (1 → 2) h2 (1 ↔ 2) h2 (1 ← 2) round r + 2 process 1

process 2

Figure 1: Successive subdivisions of the inputless view complex. Each history has three extensions; their order reverses when the endpoint owners are exchanged.

2.5

Representing Graph Histories in the Unit Interval

To represent communication patterns geometrically, we erase input values from views. Under the full adversary, the round-r complex is a path with 3r edges. Embed the initial edge as [0, 1], with process 1 on the left; each round trisects every edge, as in Figure 1. This is iterated chromatic subdivision [HKR14], with the index and limit map of Godard and Perdereau [GP20]; see also the geometrization framework of Coutouly and Godard [CG23]. The construction is detailed in Section 4. For h ∈ Γr , let j(h) ∈ {0, . . . , 3r − 1} be the index of its edge, numbered from left to right starting at 0; in particular, j(ε) = 0. Its interval is   j(h) j(h) + 1 J(h) := , . (1) 3|h| 3|h| For h ∈ Γω , the nested intervals J(h[. . . r]) have lengths 3−r . Their unique common point defines π(h). Lemma 2.3 (

VERIFIED

Lean

). For h, k ∈ Γ∗ , h is a prefix of k if and only if J(k) ⊆ J(h).

We equip Γω with the product topology for discrete Γ; the cylinders h · Γω , for h ∈ Γ∗ , form a basis of clopen (open and closed) sets. For B ⊆ X, write B and B ◦ for its closure and interior in X. The set B is dense in X if B = X, and nowhere dense if (B)◦ = ∅. In Γω , closed sets are safety properties and dense sets are liveness properties [AS85, p. 184]. Lemma 2.4 (

VERIFIED

Lean

). The map π : Γω → [0, 1] is continuous and surjective.

It is not injective: both (1 → 2) · (1 ← 2)ω and (1 ↔ 2) · (1 ← 2)ω map to 1/3.

3

Proof Overview

We begin with the connection between repeated consensus and topology, then outline the undecidability reduction and the decision procedure. Sections 4 and 5 develop the geometry of view complexes and the consensus characterization. The detailed synthesis arguments appear in Sections 6 and 7.

3.1

Repeated Consensus

Fix a finite proposal set V with |V | ≥ 2, and take X1 = X2 = V and Y1 = Y2 = V ∪ {⊥}, where ⊥ denotes no decision. A consensus algorithm under A eventually makes both processes decide irrevocably on the same one of their round-1 proposals in every execution with graph history in A; later inputs remain arbitrary. 7

(qinit , 1)

(qinit , 1)

round r = 1

(qinit , ∗)

(qinit , 1)

1

1

= 3−0 (qinit , 0) as 1+1+1 3

1 increment

(q, 0) round r = 2

process 1

(q, 0) 0

(q, 1) 0

(q, 0) 1

process 2

(q, 0) 0

(q, 1) 0

(q, 0) 1

(q, 0) 0

view complexes

(q, ∗)

(q, 1) 0

(q, 1) as 1+1+1 = 3−1 9

1 run of machine

Figure 2: The basic idea for encoding configurations with one counter. Actual process outputs will contain more parameters. Lemma 3.1 ([CG23, Theorem 26] if π(A) ̸= [0, 1].

VERIFIED

Lean

). Consensus is solvable under message adversary A if and only

Consensus is solvable in bounded time if both processes decide by a common round bound R in every execution. For h ∈ Pref(A), define h−1 A := {k ∈ Γω | h · k ∈ A}. Consensus is repeatedly solvable in bounded time if it is solvable in bounded time under every h−1 A, for h ∈ Pref(A), allowing the algorithm and bound to depend on h. If one bound R works for all prefixes, it is repeatedly solvable in uniformly bounded time. VERIFIED

Lemma 3.2 ( Lean ). Consensus is repeatedly solvable in bounded time under message adversary A if and only if π(A) is nowhere dense. In this case, if A is ω-regular, consensus is repeatedly solvable in uniformly bounded time. A process is a broadcaster for a finite graph history if at least one of its messages reaches the other process. Agreement on a broadcaster lets both processes decide on its proposal; conversely, consensus yields agreement on a broadcaster within the same round bound [NSW24, Theorem 7.12]. VERIFIED

Lemma 3.3 ( Lean ). Let A be a message adversary under which consensus is solvable within R rounds. Then there is a distributed algorithm that makes both processes decide at round R on a common process p, which is a broadcaster in the first R rounds.

3.2

Undecidability Result

We outline the counter-machine reduction proving Theorem 1.1. A (deterministic) n-counter machine is a tuple M = (Q, ∆, qinit , F ) with finite state set Q, initial state qinit , set of halting states F ⊆ Q, and counters c1 , . . . , cn . The transition function ∆ assigns to each q ∈ Q \ F either an increment increment(ci ); goto q ′ , or a decrement if ci = 0 then goto q ′ else decrement(ci ); goto q ′′ . Configurations (q, x1 , . . . , xn ) ∈ Q × Nn evolve accordingly, and M halts if its run from (qinit , 0, . . . , 0) reaches a state in F . Halting is undecidable for 2-counter machines [Min67, p. 255–258]. We show that the non-halting problem for 2-counter machines can be reduced to the LL-Synthesis problem. We will then show that it can be further reduced to the LL-Synthesis(A) problem where A is omega-regular and π(A) is not nowhere-dense, proving one direction of Theorem 1.2. Throughout this reduction, the input sets X1 and X2 are singletons, so we identify Σ with Γ by omitting the fixed input values. Specifications are therefore interpreted over (Γ × Ω)ω , where Ω = Y1 × Y2 . The reduction constructs output sets Y1 and Y2 of finite size. To ease the presentation, we explain the reduction from a 1-counter machine. The adaptation to a 2counter machine is straightforward. Let Mcounter = (Q, ∆, qinit , F, {c1 }) be a 1-counter machine. Since the output sets Y1 , Y2 have to be finite, having an unbounded counter means that an LTL formula trying to simulate Mcounter cannot talk about the exact counter values of the machine configurations. The insight here is to use the view complexes of an algorithm realizing ϕ(Mcounter ) and distribute the counter value at step r over the view complex at round r + 1.

8

The encoding of the machine configurations in the view paths is implemented as follows. Consider the sequence of view complexes of an algorithm f realizing ϕ(Mcounter ). Every vertex is required to output an individual binary value for its right edge. The following invariant has to be satisfied when encoding a counter value into the line of a view complex: The fraction of edges at round r with non-zero weights is 3−c , where c is the counter value at step r − 1 in the run of Mcounter . Moreover, every vertex at round r should output the state of Mcounter at round r − 1. One thus obtains a sequence of view complexes with output labels that simulate a run of Mcounter . See Figure 2 for an example. Other issues that ϕ(Mcounter ) needs to address are: (i) ensuring that the view complex simulation correctly detects whether counter c1 is zero or not, (ii) the exact manner of encoding the counter value at each round so that it can be locally checked. We now formally specify the output sets and the formula ϕ(Mcounter ). Every vertex outputs a tuple of the form (q, zero, plan, carry, pos), consisting of a control state q ∈ Q, a zero indicator variable zero ∈ {⊤, ⊥} claiming whether c1 is zero or not, a tuple plan for its right edge, variables carry ∈ {0, . . . , 8} and pos ∈ {0, 1, 2}. A plan is a tuple which specifies the weights of the current (right) edge and its three child edges from left to right, denoted respectively w ∈ {0, 1} and a0 , a1 , a2 ∈ {0, 1}. The pos variable is meant to be equal to the vertex’s position in its view path modulo 3. The modulo operator is needed in order to keep the output set finite. The carry variable is to help a vertex determine how many child edges in a plan should have non-zero weight, in the following way. The number of edges in the view complex at round r + 1 is three times the number of edges in the view complex at round r. When the counter is unchanged (respectively incremented), the number of weight-1 edges must be multiplied by 3 (respectively stay constant), and this could be checked edge by edge. Implementing a decrement is more complicated, since it requires multiplying the total number of edge weights with value 1 by 9. This cannot be checked only by comparing the value of an edge weight and those of its children, and will be enforced through the carries. Assume an edge weight is 0 and its children have weight 0, 1, 1. If we focus only on the current edge, nine times its weight is still 0. At the next level though, the total number of edges with value 1 will be 2. There is an excess of two, compared to the expected value, which will be carried to the neighboring edge. For each plan, if the current weight is 1, the expected total value of edge weights at the next level is 9. If the carry computed by its left neighbor is 7, then it is enough for its own child edges to have weights 0, 1, 1. This meets the requirement of multiplying the number of weight-1 edges by 9. If the child edges have instead weights 1, 1, 1, then there is an excess of 1, that will be carried over to the right neighbor. So the carry is the cumulative excess, scanning the path from left to right, of children of weight 1 produced so far, over those required so far. It must stay between 0 and 8, and must be equal to 0 at both ends, so that the computation does not start with undue carry, and no carry is left over at the end of the line. To be uniform, the same mechanism is used for the other operations, with factors 1 and 3 instead of 9. Realizing ϕ(Mcounter ) means satisfying conditions on the view complex Any algorithm f realizing ϕ(Mcounter ) needs to satisfy locally checkable conditions (C0)–(C5) on its view complex, which we explain below. We will use the following shorthands for the LTL formulas: instead of writing outp = y, since the outputs are tuples, we will write qp = q, zero p = z, and so on, for each component of the output. Moreover, since plan is also a tuple, we will write plan p .w = x, plan p .ai = a, for i ∈ {0, 1, 2}. In the view complex at round r, we refer to the different components of the output of the ith vertex (numbered from 0 to 3r , from left to right) by q(r, i), zero(r, i), carry(r, i), and pos(r, i). Moreover, the different components of plan are referred to by plan(r, i).w, plan(r, i).a0 , plan(r, i).a1 , plan(r, i).a2 . Each condition below can be expressed by LTL formulas on executions: they are able to relate a specific edge of the view complex (i.e., a finite history) with the outputs of its two endpoints (the corresponding views of the processes). However, the specification must determine which process’s view is the left endpoint of the current edge. To this end, each process also outputs the position of its view along the path, modulo 3 to keep the output set finite. The left endpoint is then the vertex whose position precedes the other’s

9

by one, modulo 3. Three labels suffice because the two possible position differences, 1 and −1, are distinct modulo 3. (C0) Position Order: For every round r, pos(r, i) = i mod 3. We will enforce this by an LTL formula thanks to the following inductive reasoning: after a history h, if process 1’s view has integer position u and process 2’s view has integer position v, then we can determine their positions at the next round hg: observe that going from the view of process 1 at position 3u to the view of process 2 at position 3v, we always encounter the following sequence of g: (1 → 2), then (1 ↔ 2), then (1 ← 2). Since v − u = 1 or v − u = −1, depending on whether process 1’s view or process 2’s view is on the left, the different positions encountered are then 3u + (v − u), 3u + 2(v − u), and 3u + 3(v − u) = 3v. Since process 1’s and process 2’s views alternate in the line, this gives the following inductive computation: Let Z3 := {0, 1, 2}, and write a mod 3 ∈ Z3 for the least nonnegative remainder of an integer a modulo 3. For g ∈ Γ, define ChildPosg : Z23 → Z23 by   if g = (1 → 2) (3u mod 3, (2u + v) mod 3) ChildPosg (u, v) := ((u + 2v) mod 3, (2u + v) mod 3) if g = (1 ↔ 2) (2)   ((u + 2v) mod 3, 3v mod 3) if g = (1 ← 2) . For u, v ∈ Z3 and g ∈ Γ, define ϕ(u, v, g) := (pos 1 , pos 2 ) = (u, v) → X [graph = g → (pos 1 , pos 2 ) = ChildPosg (u, v)]

PosOrd :=

^

  ^ ^ ^
graph = g → (pos 1 , pos 2 ) = ChildPosg (0, 1) ∧ G  ϕ(u, v, g)

g∈Γ

(3)

(4)

u∈Z3 v∈Z3 g∈Γ

Formula PosOrd ensures that if the pair of positions of processes 1 and 2 in edge h is (u, v), then for every g ∈ Γ, the pair of positions in edge hg is given by ChildPosg (u, v). Now that the processes are bound to output the position of their view modulo 3 on the line, it is easy to write an LTL formula W to determine whether process 1’s view is on the left endpoint of the current edge, or not: OneIsLeft := (pos 1 = p ∧ pos 2 = q). (p,q)∈Z23 q≡p+1 mod 3

(C1) Path Agreement: For every round r, for all 0 ≤ i, j ≤ 3r , q(r, i) = q(r, j) and zero(r, i) = zero(r, j). The state of the counter machine, as well as the status of the counter with respect to 0 at the ith step of the computation is then claimed consistently by all the processes in round i + 1. This global constraint on each line of the view complex is ensured thanks to the indistinguishability relation linking the different edges. It is enough to require that processes 1 and 2 always agree on these components of their outputs. The current state and current zero-status of the counter are enough to determine how the counter has to be changed, and thus, which multiplication factor has to be applied to the weights of the view complex. Given q ∈ Q and z ∈ {⊤, ⊥} the zero-status of the counter, we let m(q, z) be this factor. The next condition ensures that the ratio of the sum of edge weights to the total number of edges at each round changes appropriately depending on the operation. (C2) Local Sum Check: For every round r, for all 0 ≤ i ≤ 3r − 1, m(q(r, i), zero(r, i)) · plan(r, i).w + carry(r, i + 1).

P2

k=0 plan(r, i).ak + carry(r, i) =

Additionally, we require in the next constraint that carry(r, 0) = carry(r, 3r ) = 0, ensuring that the computation does not start with undue carry, and no carry is left over at the end of the line. Since for all 0 ≤ i, j ≤ 3r , q(r, i) = q(r, j) = q and zero(r, i) = zero(r, j) = z, thanks to (C1), summing over all the vertices of the line 10

P3r −1 P2 P3r −1 will make carries cancel out and will ensure that i=0 k=0 plan(r, i).ak = m(q, z) · i=0 plan(r, i).w, as required. Importantly, this can be checked locally on the view complexes of f . It is easy to write an LTL formula that, after any history h ∈ Γr , relates the carry and plan outputs of the two processes to ensure the equation of (C2), using OneIsLeft. As for (C1), this local equation propagates along the line because a process’s carry is the same for its left and right edges. (C3) Zero Claim Check: For every round r ≥ 1, carry(r, 0) = carry(r, 3r ) = 0. Moreover, if zero(r, 0) = ⊤, then for all j ≤ 3r − 1, plan(r, j).w = 1, and if zero(r, 0) = ⊥, then plan(r, 0).w = 0. This condition actually ensures two different things: one is the value of the carries for the extreme vertices, as explained above. The second is to check zero claims made by the processes. If checking that the counter is 0 simply requires that all the weights attributed along the line are 1, checking that it is not requires to check that at least one of the weights is 0: but how could it be checked on a single run? Observe that for the decrement mechanism to work, the weight of the first edge is necessarily 0: since the first vertex receives no carry from the left (and a carry cannot become negative), its three child edges contribute at most 3; if its own current edge is 1, it will not be possible to meet the requirement. This is why it is safe for the specification to check the validity of a non-zero claim on the first edge. It remains to explain how the specification can constrain the outputs of the extreme vertices of the view complex. For that, the pos-component of the output is useless. Instead, we use the fact that the view positioned on the left of every round r always corresponds to the view of process 1 after the history (1 → 2)r (and the view of process 2 after the history (1 ← 2)r for the rightmost vertex). Hence the formula LeftMost := [carry 1 = 0 ∧ (zero 1 = ⊥ → plan 1 .w = 0)] W (graph ̸= (1 → 2)). The other formulas for (C3) are given in Section 6 . The following condition ensures correct encoding of the initial configuration of the counter machine. (C4) Initial Check: For all 0 ≤ j ≤ 3, q(1, j) = qinit , and for 0 ≤ j ≤ 2, plan(1, j).w = 1. Lastly, the algorithm should check that the state values output in each round are correct in accordance with the zero claims and that the weight of each edge is equal to the weight promised in the previous round. For that we can define the function next(q, z) that gives the next state given by ∆, according to the current state q and the zero-status of the counter. (C5) Proper Transition: For every round r ≥ 1, q(r + 1, 0) = next(q(r, 0), zero(r, 0)) and, for all 0 ≤ j ≤ 3r − 1, for all x ∈ {0, 1, 2}, plan(r + 1, 3j + x).w = plan(r, j).ax . When the last edge of the history was (1 ↔ 2), the current weight has to be compared with the promise a1 made at the previous round. When it was (1 ← 2) or (1 → 2) however, it has to be compared with either a0 or a2 from the previous round depending on the orientation of the edge with respect to process 1 and process 2. This can be easily computed and ensured thanks to the formula OneIsLeft. V Combining conditions (C0)–(C5) with G( q∈F q1 ̸= q) gives a formula ϕ(Mcounter ). This formula is realizable if and only if Mcounter does not halt. We say that an LTL formula ϕ is a safety formula if its language L(ϕ) is a safety property in (Σ × Ω)ω . A safety property P is such that, for all t ∈ (Σ × Ω)ω \ P , there exists i ≥ 0 such that, for all u ∈ (Σ × Ω)ω , t[. . . i] · u ∈ / P . Formulas in negation normal form built from atomic propositions using only ∧, ∨, X, G, and W are safety formulas [Sis94]. Formula ϕ(Mcounter ) is of this form: antecedents of implications contain only atomic propositions and X, which is self-dual, and no F or U operator occurs. Not Nowhere Dense Adversaries Let A be an ω-regular message adversary such that π(A) is not nowhere dense. There exists a finite graph history h such that h−1 A is dense in Γω . Define Prefixh := V|h| r−1 (graph = h[r]) and, for an LTL formula ϕ, define ϕb := Prefixh → X|h| ϕ . r=1 X For a safety formula ϕ, the guarded formula ϕb is realizable under A if and only if ϕ is realizable under Γω . Applying this to the safety formula ϕ(M ) constructed from a 2-counter machine M yields undecidability of LL-Synthesis(A). Section 6 establishes both the counter-machine encoding and this transfer of realizability. 11

3.3

Decidability Result

We prove the decidability direction of Theorem 1.2 by giving a procedure that also constructs a realizing distributed algorithm whenever one exists. VERIFIED

Theorem 3.4 ( Lean ). Given a deterministic parity automaton for a message adversary A with nowheredense image π(A) and an LTL formula ϕ, one can decide whether a distributed algorithm realizing ϕ under A exists and construct one if it does. We represent distributed algorithms by trees whose nodes carry connected subgraphs of the view complex, with automaton states on edges and outputs on vertices of their extensions. The uniform consensus bound from Lemma 3.2 lets us bound the number of edges at each node while preserving acceptance. Up to isomorphism, their node data range over a finite set. Acceptance is expressible in MSO, so tree-automaton nonemptiness yields a decision procedure. 3.3.1

Notation and Consensus Bound Computation

In the constructions below, K, K ′ , and their indexed variants denote subgraphs of a view complex at a fixed round, with no isolated vertices. Write E(K) for the edge set of K. For an edge e, write ep for its process-p endpoint. Applying Table 1 to the endpoints of e and a signal a ∈ Σ gives an edge ea at the next round. Iterating this operation defines ew for w ∈ Σ∗ , with eε = e. In particular, e(h)w = e(hw). For every integer t ≥ 0, let K (t) be the graph with edge set E(K (t) ) := {ew | e ∈ E(K), w ∈ Σt } . Each edge in K (t) has a unique such decomposition. The graph K (t) includes all continuations over Σ, including those whose graph histories do not extend to A. For every p ∈ P, e, e′ ∈ E(K), and w, w′ ∈ Σt , repeated application of Lemma 2.1 gives (ew)p = (e′ w′ )p =⇒ ep = e′p . Consequently, extensions of distinct connected components cannot share a vertex. In the following, fix a deterministic parity automaton Aadv recognizing a message adversary A with nowhere-dense image π(A). We assume that A ̸= ∅, since otherwise any distributed algorithm suffices. From Aadv , one can construct a deterministic finite automaton Alive = (S, sinit , τ, Flive ) with set of states S, initial state sinit , transition function τ : S × Γ → S, and accepting states Flive , that recognizes Pref(A). Keep the states and transitions of Aadv , and declare a state accepting in Alive if an accepting infinite continuation exists from that state in Aadv . It is further well known that one can construct an automaton that checks whether an execution satisfies ϕ whenever its graph history belongs to A: VERIFIED

Lemma 3.5 ( Lean ). From Aadv and an LTL formula ϕ, one can construct a deterministic parity automaton Aϕ = (Qϕ , qϕ , δϕ , χϕ ), with states Qϕ , initial state qϕ , transition function δϕ : Qϕ × (Σ × Ω) → Qϕ , and priorities χϕ : Qϕ → N, that accepts the executions e ∈ (Σ × Ω)ω with Graph(e) ∈ / A or e |= ϕ. Proof. From ϕ, construct the parity automaton A′ϕ that accepts the executions (Σ × Ω)ω with e |= ϕ. Complementing Aadv and taking the union with A′ϕ yields Aϕ . Both operations are computable [Tho90]. For an input signal history h ∈ Σ∗ , we write s(h) for the state of Alive reached on Graph(h). We also write s(e(h)) := s(h) and call an edge e live if s(e) ∈ Flive . A uniform bound on the rounds needed for consensus after every live prefix can be computed from Aadv . VERIFIED

Lemma 3.6 ( Lean ). From Aadv , one can compute a D ≥ 1 such that consensus is solvable within D rounds under h−1 A for every h ∈ Pref(A). In the following, let D ≥ 1 be a uniform consensus bound for adversary A, computed using Lemma 3.6. 12

3.3.2

Component Trees

We group rounds into blocks of length D, with outputs still produced in every round. Using the automata Alive and Aϕ constructed above, we obtain an automaton that reads these blocks and also records whether the communication prefix is live. VERIFIED

Lemma 3.7 ( Lean ). One can construct a deterministic parity automaton B = (Q, qinit , δ, χ) over ΣD × ΩD that accepts exactly the executions, grouped into blocks, that satisfy ϕ or whose graph history is outside A. Moreover, one can compute a subset Qlive ⊆ Q such that, after any finite sequence of blocks, the automaton is in Qlive if and only if the corresponding graph history extends to an infinite graph history in A. A position (K, q) at round nD consists of a nonempty connected subgraph K of the view complex under A and an edge labeling q : E(K) → Q. For each e = e(h) ∈ E(K), there must be an output sequence such that B reaches q(e) after reading the resulting execution in blocks of length D. Thus q(e) ∈ Qlive . The initial position (K0 , q0 ) consists of the single edge einit := {I1 , I2 }, labeled with qinit . An output labeling from K assigns an output λp (v) ∈ Yp to every process-p vertex v of each extension graph K (t) , 1 ≤ t ≤ D. For an edge e ∈ E(K) and an input signal history u ∈ Σ[1,D] , write
λ(e, u) := λ1 ((eu)1 ), λ2 ((eu)2 ) . Since each local view receives a single output label, each process’s output depends only on its view. For a complete block u ∈ ΣD , let qλ (e, u) be the successor of q(e) in B on u with the successive outputs (D) λ(e, u[. . . 1]), . . . , λ(e, u). We call χ(qλ (e, u)) the block priority. Let Klive be the subgraph of K (D) with edge set (D) E(Klive ) := {eu | e ∈ E(K), u ∈ ΣD , qλ (e, u) ∈ Qlive } . Its edges are precisely the extensions allowed under A. FORMALIZED

). An uncompressed component tree is a rooted tree carrying a position (K, q) Definition 3.8 ( Lean and an output labeling λ from K at each node. The root carries (K0 , q0 ). At a node carrying (K, q) and λ, (D) every connected component K ′ of Klive gives exactly one child carrying (K ′ , q ′ ), where q ′ (eu) := qλ (e, u) for all eu ∈ E(K ′ ). These are all its children. The same output labeling is used for every child. A run consists of an infinite branch from the root with successive positions (Kn , qn ), edges en ∈ E(Kn ), and blocks un ∈ ΣD such that e0 = einit ,

en+1 = en un ∈ E(Kn+1 ) .

(5)

The tree is accepting if the state sequence (qn (en ))n≥0 of every run satisfies the parity condition. Every edge of K has an extension allowed under A, so every node has a child. A branch specifies successive components, while a run follows successive edges through them. Several runs may therefore share a branch; see Figure 3. A finitely branching labeled tree is effectively given if, after numbering the children at each node, an algorithm computes the label and the number of children at any valid finite node address. To effectively construct such a tree means to construct such an algorithm. We now relate accepting uncompressed component trees to realizing distributed algorithms. VERIFIED

Lemma 3.9 ( Lean ). A distributed algorithm realizing ϕ under A exists if and only if an accepting uncompressed component tree exists. From an effectively given accepting uncompressed tree, one can compute the local output functions of a realizing algorithm.

13

Figure 3: One block of an uncompressed component tree. On the left, colored vertices represent process views, black edges join views that can occur together, and crosses mark extensions that cannot be continued (D) under A. Each connected component of (Kn )live gives a child; the middle child is highlighted. On the right, dots represent edges along one branch, and the green path is a run. The state at its next edge determines the block priority. An algorithm provides the vertex labels. Conversely, distinct components have disjoint vertex sets, and Lemma 2.1 implies that their extensions cannot share a vertex. The labels at different nodes therefore define consistent local output functions. Components can have arbitrarily many edges, and their views grow with the round. We use the uniform consensus bound to choose, at each node, a reduction r : K → K that preserves edge labels and has a bounded image. The next block starts from r(K). Suitable choices give accepting trees whose nodes have a uniformly bounded number of edges. Up to isomorphism, only finitely many labeled graphs and block transitions remain. We call trees of these finite descriptions symbolic component trees. Each child also records which reduced parent edge and block generated each of its edges. MSO checks that these labels fit together and that every compatible run accepts, yielding a decision procedure by Rabin’s theorem [Rab69]. Section 7 constructs these bounded representations and the resulting decision procedure.

4

Properties of the Inputless View Complex

Formally, for a finite graph history h ∈ Γ∗ , define the inputless view vp0 (h) by vp0 (ε) := Ip and the recursion in Table 1 with all input arguments omitted. Let Ep be the map that recursively erases input values from a view of process p. An induction on |h′ | using the view updates gives, for every input signal history h′ ∈ Σ∗ , Ep (vp (h′ )) = vp0 (Graph(h′ )) .

(6)

The inputless round-r view complex under A has the edges {v10 (h), v20 (h)} for the graph histories h ∈ Γr that extend to an element of A, and their endpoints as vertices. Throughout this subsection, we use the full message adversary A = Γω and write vp (h) for vp0 (h). To establish the link of these subdivisions of [0, 1] with the view complexes, we show that the round-r view complex is a line of length 3r and that the histories that correspond to its edges line up with the above construction. Figure 4 shows the main argument. Suppose an original edge has endpoint views u := vp (h) on the left and v := vp̄ (h) on the right. Its three extensions form a path with successive vertices Np (u),

Cp̄ (v, u),

Cp (u, v),

Np̄ (v) .

(7)

The outer endpoints retain their positions, but their view labels change from u and v to Np (u) and Np̄ (v). Neighboring extensions share a receiving process’s view: that process cannot distinguish whether its own 14

u = vp (h)

v = vp̄ (h)

round r

process p

h Np (u)

Cp̄ (v, u)

Cp (u, v)

Np̄ (v)

process p̄

round r + 1 h(p → p̄)

h(p ↔ p̄)

h(p ← p̄)

Figure 4: View labels in a single subdivision. The left endpoint of the original edge is a view of process p, its right endpoint one of process p̄. The three extensions share the two receiving views, while the outer endpoints carry the updated nonreceiving views. message was also delivered. Moreover, subdivisions of neighboring original edges meet at the same updated view Np (u) whenever their common endpoint was u of process p. Consequently, the subdivisions fit together into a single path. The endpoints of the line are those in which one of the processes has perfect information about the graph history. A process that does not receive a message in a round knows that its message was received by the other process. Thus, the view of a process that never received a message is an endpoint of the line. There are exactly two such views; one for each process. VERIFIED

Lemma 4.1 ( Lean ). Let h ∈ Γr . Then the subgraph of the inputless round-(r + 1) view complex induced by the set of views {vp (hg) | p ∈ P ∧ g ∈ Γ} is a line of length 3. Proof. By the recusive definition of vp (hg) in Table 1, the induced subgraph has the four vertices N1 (u), C2 (v, u), C1 (u, v), and N2 (v) joined by the edges {N1 (u), C2 (v, u)}, {C2 (v, u), C1 (u, v)}, and {C1 (u, v), N2 (v)}, where u := v1 (h) and v := v2 (h). Lemma 4.2 (

VERIFIED

Lean

). The inputless round-r view complex is a line of length 3r .

Proof. By induction on r. The base case r = 0 is trivial. Now suppose that the inputless round-r view complex is a line of length 3r . By Lemma 4.1, the round-(r + 1) view complex contains at least 3r lines of length 3 each. These 3r lines are edge-disjoint, but not vertex-disjoint: If {vp (h), vp̄ (h)} and {vp̄ (h′ ), vp (h′ )} are two distinct incident edges in the round-r view complex, with vp̄ (h) = u = vp̄ (h′ ), then vp̄ (hg) = Np̄ (u) = vp̄ (h′ ·g) where g = (p ← p̄). By Lemma 2.1, the 3r lines share no other vertices. Thus, the round-(r+1) view complex contains a line of length 3r+1 . Since there are no more than 3r+1 round-(r + 1) graph histories in Γr+1 , the complex does not contain any other edges. The round-(r + 1) view complex is thus a line of length 3r+1 .
Lemma 4.3 ( Lean ). The view vp (p → p̄)r has a single adjacent view in the inputless round-r view complex. VERIFIED

Proof. By induction on r. The base
case r = 0 is trivial since there are only two views in the view complex.
Now suppose that u = vp (p → p̄)r has v = vp̄ (p → p̄)r as the only adjacent view in the inputless
round-r r+1 = Np (u) view complex. Then, by the recursive definition in Table 1 and Lemma 2.1, the view v (p → p̄) p
has vp̄ (p → p̄)r+1 = Cp̄ (v, u) as the only adjacent view in the inputless round-(r + 1) view complex. The order of the three extensions depends on which process’s view is the left endpoint. If this process is p, then the extensions appear from left to right as h(p → p̄),

h(p ↔ p̄),

h(p ← p̄) .

(8)

Thus, the bidirectional graph always corresponds to the middle subinterval. The two unidirectional graphs exchange positions when the processes at the endpoints are reversed. This happens, for example, when subdividing the middle edge h1 in Figure 1.

15

By convention we will take the view v1 (1 → 2)r as the left endpoint of the inputless round-r view complex. Based on this orientation, we assign consecutive positions to the edges in the complex, starting with position 0 on the leftmost edge. Since the edges in the complex are in a one-to-one correspondence with the length-r graph histories, this amounts to assigning positions j(h) to the
length-r graph histories h ∈ Γr . By the above convention, the history (1 → 2)r has position j (1 → 2)r = 0 and the graph history (1 ← 2)r
graph r r has position j (1 ← 2) = 3 − 1. For the recurrence below, define the offsets δ((1 → 2)) := 0, Lemma 4.4 (

VERIFIED

Lean

δ((1 ↔ 2)) := 1,

δ((1 ← 2)) := 2 .

). For all h ∈ Γ∗ and g ∈ Γ, we have ( δ(g) if j(h) is even j(hg) = 3j(h) + 2 − δ(g) if j(h) is odd .

(9)

Proof. Let r := |h|. As shown in the proof of Lemma 4.2, each edge of the round-r view complex is replaced by the line of length 3 from Lemma 4.1, with each old vertex w of process p replaced by Np (w). Since
N1 v1 ((1 → 2)r ) = v1 ((1 → 2)r+1 ), this replacement preserves the left endpoint and hence the order of the edges. Thus, the three extensions of h occupy positions 3j(h), 3j(h) + 1, and 3j(h) + 2. Every edge joins views of different processes, and the leftmost vertex belongs to process 1. Hence, the left endpoint of the edge corresponding to h belongs to process 1 if j(h) is even, and to process 2 if j(h) is odd. By the recursive definition in Table 1, the three extensions are ordered from left to right as h(1 → 2), h(1 ↔ 2), h(1 ← 2) in the even case, and in the reverse order in the odd case. The offset of j(hg) from 3j(h) is therefore δ(g) in the even case and 2 − δ(g) in the odd case. Proof of Lemma 2.3. (⇒): By Lemma 4.4, the intervals J(hg), for g ∈ Γ, are the three equal subdivisions of J(h). Repeated application shows that J(k) ⊆ J(h) whenever h is a prefix of k. (⇐): Suppose that J(k) ⊆ J(h). Since these intervals have lengths 3−|k| and 3−|h| , respectively, we have |k| ≥ |h|. Let u be the prefix of k of length |h|. By the (⇒) direction, we have J(k) ⊆ J(u) and thus J(k) ⊆ J(h) ∩ J(u). Thus, this intersection has positive length. By the definition of J, distinct histories of the same length correspond to intervals with disjoint interiors. Hence u = h, which proves that h is a prefix of k. ′

The product topology on Γω is metrizable via the ultrametric d(h, h′ ) := 2− inf{r≥1|h[r]̸=h [r]} [PP04, Ch. III, Prop. 3.2]. Proof of Lemma 2.4. We prove uniform continuity. Let ε > 0 and choose an integer r ≥ 0 such that 3−r < ε. If h, h′ ∈ Γω satisfy d(h, h′ ) < 2−r , then they have a common prefix k of length r. By Lemma 2.3 and the definition of π, both π(h) and π(h′ ) belong to J(k). Hence |π(h) − π(h′ )| ≤ 3−r < ε ,

(10)

proving continuity. For surjectivity, let x ∈ [0, 1]. By Lemma 4.4, the three intervals J(hg), for g ∈ Γ, cover J(h). Starting from x ∈ J(h0 ) = J(ε) = [0, 1], we can therefore recursively choose hr+1 = hr g such that x ∈ J(hr+1 ). These compatible prefixes define an infinite history h ∈ Γω . Both x and π(h) belong to J(hr ) for every r, so their distance is at most 3−r for every r. Thus π(h) = x.

5

Nowhere-Dense Message Adversaries and Consensus

We characterize bounded-time consensus using the topology of graph histories, extend this characterization to repeated consensus, and relate consensus to agreement on a broadcaster.

16

5.1

Consensus and Bounded Termination

A decision problem is defined by finite nonempty sets I of possible inputs and O of possible outputs, and a relation ∆ ⊆ I 2 × O2 of allowed input–output pairs. We take X1 = X2 = I and Y1 = Y2 = O ∪ {⊥}, where ⊥ ∈ / O denotes that no decision has been made. The inputs received in round 1 are the proposals for the decision problem. Subsequent inputs remain arbitrary, but the validity of the decisions depends only on the proposals. Let A ⊆ Γω be a message adversary. A distributed algorithm f solves a decision problem under message adversary A if (1) all its non-⊥ outputs are irrevocable (i.e., don’t change over time) and (2) in every execution with graph history in A and round-1 inputs (i1 , i2 ), both processes eventually output non-⊥ values (o1 , o2 ) such that ((i1 , i2 ) , (o1 , o2 )) ∈ ∆. This notion of solvability agrees with the usual model in which inputs are supplied only initially. An algorithm for that model can ignore subsequent inputs. Conversely, an algorithm that solves the problem with arbitrary subsequent inputs can be simulated using each process’s proposal as its input in every round. The consensus problem with value set V is the decision problem with I = O = V and ∆ defined by requiring both outputs to be equal and to be one of the inputs. To make the problem nontrivial, we choose any finite V with |V | ≥ 2. The construction of π describes graph histories independently of the input values. We use them to study the message adversary A ⊆ Γω , while algorithms solving decision problems operate on views containing inputs. Lemma 3.1 relates consensus solvability in this model to the geometry of A. Ordinary consensus permits the decision time to depend on the execution. The geometric characterization reflects this flexibility: it is enough that π(A) omit a single point, even if admissible histories have images arbitrarily close to that point. Requiring a common decision bound imposes a stronger condition. We say that a distributed algorithm solves a decision problem in bounded time under A if it solves it under A and there is a round number R such that all ⊥ outputs happen before round R in all executions considered for solvability. Taking the closure of an adversary introduces no new finite graph histories. Consequently, an algorithm that decides within a fixed number of rounds cannot use the distinction between an adversary and its closure. Conversely, compactness turns termination under a closed adversary into a uniform decision bound. This explains why bounded-time consensus is governed by the closure of π(A), and hence by the existence of an interval missing from its image. Lemma 5.1 (

VERIFIED

Lean

). For any message adversary A ⊆ Γω , we have π(A) = π(A).

Proof. Since Γω is compact by Tychonoff’s theorem [Bou98, Ch. I, §9.5, Thm. 3] and [0, 1] is Hausdorff, continuity of π (Lemma 2.4) implies π(A) = π(A) [Bou98, Ch. I, §9.4, Cor. 2 to Thm. 2 and Ch. I, §5.4, Prop. 9]. VERIFIED

Lemma 5.2 ( Lean ). Consensus is solvable in bounded time under message adversary A if and only if π(A) is not dense in [0, 1]. Proof. (⇐): Since π(A) is not dense in [0, 1], using Lemma 5.1, we have π(A) = π(A) ̸= [0, 1]. By Lemma 3.1, consensus is solvable under the message adversary A by some distributed algorithm f . The space of admissible infinite input signal histories under A is naturally identified with (I × I)ω × A, which is compact since I is finite and A is closed. In every execution, both processes have decided after some finite prefix of the input signal history. Any admissible history with the same prefix yields the same outputs up to that round, so both processes have also decided by then. For each such prefix, the set of admissible histories extending it is open. These sets cover all admissible histories. A finite subcover gives a uniform decision bound [LM95, Lemma 1.1]. Thus f solves consensus in bounded time under A, and under A as well since A ⊆ A. (⇒): Assume by contradiction that f solves consensus in bounded time under A and that π(A) is dense in [0, 1], i.e., that π(A) = [0, 1]. Let R be an upper bound for ⊥ outputs of f under A. Consider the message adversary B := Pref R (A) · Γω whose graph histories are the length-R prefixes of A followed by an arbitrary infinite graph history. Let f ′ follow f until each process’s first non-⊥ output, which that process then repeats forever. Every length-R input signal history under B extends to an infinite input signal history

17

under A with the same inputs and graphs in the first R rounds. Hence f ′ makes valid, agreeing decisions by round R under B, and solves consensus under B. Since B is a safety property, hence closed [AS85, p. 184], and A ⊆ B, we have A ⊆ B and thus [0, 1] = π(A) = π(A) ⊆ π(B) ⊆ [0, 1]. But then π(B) = [0, 1], which contradicts the fact that f ′ solves consensus under B by Lemma 3.1.

5.2

Removing Finite Prefixes

A decision bound from the beginning of an execution does not ensure that consensus remains solvable after an arbitrary prefix. The prefix restricts the possible continuations, and the gap that originally permitted consensus may lie outside the part of the adversary that remains relevant. We must therefore apply the characterization to each left quotient of the adversary. For a finite graph history h ∈ Pref(A), define the left quotient h−1 A := {k ∈ Γω | h · k ∈ A}. Geometrically, this requires restricting attention to histories extending h and expressing their images in the coordinates of J(h). Removing the prefix rescales this interval to [0, 1], reversing its orientation when j(h) is odd. The next three lemmas establish this correspondence at the level of edge positions, finite intervals, and infinite histories. ( j(h · k) − 3|k| j(h) if j(h) is even Lemma 5.3 ( Lean ). j(k) = |k| 3 (j(h) + 1) − j(h · k) − 1 if j(h) is odd VERIFIED

Proof. By induction on |k|. The base case k = ε follows from j(ε) = 0. Now let k = ℓg and assume the claim holds for ℓ. Set r := |ℓ| and a := j(ℓg) − 3j(ℓ). If j(h) is even, the induction hypothesis gives j(h · ℓ) = 3r j(h) + j(ℓ). Hence j(h · ℓ) and j(ℓ) have the same parity. By Lemma 4.4, appending g therefore gives the same offset a in both cases, so j(h · k) = 3j(h · ℓ) + a = 3r+1 j(h) + 3j(ℓ) + a r+1

=3

(11)

j(h) + j(k) .

If j(h) is odd, the induction hypothesis gives j(h · ℓ) = 3r (j(h) + 1) − j(ℓ) − 1. Hence j(h · ℓ) and j(ℓ) have opposite parity. By Lemma 4.4, the offset for appending g to h · ℓ is therefore 2 − a, so j(h · k) = 3j(h · ℓ) + 2 − a = 3r+1 (j(h) + 1) − 3j(ℓ) − 1 − a r+1

=3

(12)

(j(h) + 1) − j(k) − 1 .

Rearranging these equalities proves the claim. ( 3|h| J(h · k) − j(h) Lemma 5.4 ( Lean ). J(k) = j(h) + 1 − 3|h| J(h · k) VERIFIED

if j(h) is even if j(h) is odd

Proof. Let r := |k|. By the definition of J, 3|h| J(h · k) =



j(h · k) j(h · k) + 1 , 3r 3r

 .

(13)

If j(h) is even, Lemma 5.3 shows that this interval is j(h) + J(k). If j(h) is odd, the same lemma shows that it is   j(k) + 1 j(k) j(h) + 1 − , j(h) + 1 − r = j(h) + 1 − J(k) . (14) 3r 3 Rearranging gives the claimed identities.

18

Lemma 5.5 (

VERIFIED

Lean

−1

). π(h

( 3|h| π(A ∩ h · Γω ) − j(h) A) = j(h) + 1 − 3|h| π(A ∩ h · Γω )

if j(h) is even if j(h) is odd

Proof. Let k ∈ Γω and denote its length-r prefix by kr . By the definition of π, the intervals J(kr ) and J(h·kr ) shrink to π(k) and π(h · k), respectively. Applying Lemma 5.4 and taking limits gives ( 3|h| π(h · k) − j(h) if j(h) is even π(k) = (15) |h| j(h) + 1 − 3 π(h · k) if j(h) is odd . As k ranges over h−1 A, the history h · k ranges over A ∩ h · Γω . Taking the sets of values on both sides proves the claim.

5.3

Repeated Consensus

The preceding identities allow us to compare consensus after different prefixes. We now require solvability under every left quotient and distinguish bounds that depend on the prefix from a common bound. We say that a decision problem is repeatedly solvable under a message adversary A if it is solvable starting after any finite prefix, i.e., if it is solvable under all h−1 A where h ∈ Pref(A). Analogously, it is repeatedly solvable in bounded time if it is solvable in bounded time under all h−1 A. Finally, it is repeatedly solvable in uniformly bounded time if there is a uniform bound R and distributed algorithms fh such that, for all h ∈ Pref(A), the algorithm fh solves the problem under h−1 A and all ⊥ outputs happen before time R. Lemma 5.6 ( adversary A.

VERIFIED

Lean

). If π(A) has empty interior, then consensus is repeatedly solvable under message

Proof. Let π(A) have empty interior and let h ∈ Pref(A). We have π(A ∩ h · Γω ) ⊆ π(A) ∩ π(h · Γω ) = π(A) ∩ J(h) ⊊ J(h) since J(h) is an interval of positive length and π(A) has empty interior. But then, by Lemma 5.5, we get π(h−1 A) ⊊ [0, 1]. Lemma 3.1 then shows that consensus is solvable under h−1 A. The converse does not hold. Let A consist of the infinite graph histories k whose ternary digits j(kr ) − 3j(kr−1 ) are not eventually zero, where kr is the length-r prefix of k. Then π(A) = (0, 1], while π(h−1 A) is (0, 1] if j(h) is even and [0, 1) if j(h) is odd, for every finite graph history h. Thus consensus is repeatedly solvable under A by Lemma 3.1, although π(A) has nonempty interior. Repeated bounded-time consensus requires a gap after every admissible prefix. In the interval representation, these requirements amount to finding interval gaps at arbitrarily small scales throughout [0, 1]. Nowhere density captures precisely this condition. The next two lemmas allow us to pass between the restricted adversaries and their intervals. Lemma 5.7 (

VERIFIED

Lean

). For every finite graph history h ∈ Γ∗ , we have π −1 (J(h)◦ ) ⊆ h · Γω .

Proof. Let k ∈ π −1 (J(h)◦ ), i.e., π(k) ∈ J(h)◦ . Then, by definition of π, since J(h)◦ is open, there exists a finite prefix ℓ of k such that J(ℓ) ⊆ J(h)◦ ⊆ J(h). But this, by Lemma 2.3, implies that h is a prefix of ℓ. Hence h is also a prefix of k, which means that k ∈ h · Γω . VERIFIED

Lemma 5.8 ( Lean ). For every finite graph history h ∈ Γ∗ , the set h · Γω of infinite graph histories extending h is clopen. Proof. The set h · Γω is open since it is equal to the open ball of radius 2−|h| using the ultrametric d. It is also closed since we can write it as [ h · Γω = Γω \ k · Γω , (16) k∈Γ|h| k̸=h

that is, as the complement of an open set.

19

The remaining distinction concerns the decision bounds: they may initially depend on the prefix, but an ω-regular adversary has only finitely many distinct left quotients, allowing a common bound to be chosen. Proof of Lemma 3.2. (⇐): Let π(A) be nowhere dense and let h ∈ Pref(A). Using Lemmas 5.1 and 5.8, and the fact that A ∩ B = A ∩ B if B is clopen [Bou98, Ch. I, §1.6, Prop. 5], we have π(A ∩ h · Γω ) = π(A ∩ h · Γω ) = π(A ∩ h · Γω ) ⊆ π(A) ∩ π(h · Γω ) = π(A) ∩ J(h) ⊊ J(h)

(17)

since J(h) is an interval of positive length and π(A) has empty interior. But then, by Lemmas 5.1 and 5.5, we get π(h−1 A) = π(h−1 A) ⊊ [0, 1]. Lemma 5.2 then shows that consensus is solvable in bounded time under h−1 A. (⇒): Let consensus be repeatedly solvable in bounded time under A and assume by contradiction that I ⊆ [0, 1] is a nonempty open interval included in π(A). Since π is surjective (Lemma 2.4) and len(J(h)) → 0 as |h| → ∞, there exists an h ∈ Pref(A) such that J(h) ⊆ I ⊆ π(A). By Lemma 5.7, we have J(h)◦ = J(h)◦ ∩ π(A) = J(h)◦ ∩ π(A) ⊆ π(A ∩ h · Γω ) = π(A ∩ h · Γω ) = π(A ∩ h · Γω ) .

(18)

Since the rightmost set in this inclusion chain is closed, we have J(h) = J(h)◦ ⊆ π(A ∩ h · Γω ). But, by Lemmas 5.1 and 5.2, we have π(h−1 A) ⊊ [0, 1], and thus π(A ∩ h · Γω ) ⊊ J(h) by Lemma 5.5, a contradiction. Finally, let A be ω-regular and π(A) be nowhere dense. Then there are only finitely many distinct left quotients h−1 A [Tho90, Sec. 2, p. 142]. Since consensus is solvable in bounded time under each of them, the maximum of their finitely many time bounds is a uniform bound.

5.4

Agreement on a Broadcaster

Call a process a broadcaster for a finite graph history if at least one of its messages is delivered to the other process. Consensus is equivalent to agreement on a broadcaster [NSW24, Theorem 7.12]. In fact, once both processes have selected the same broadcaster, they can decide on its proposal. Lemma 3.3 establishes the converse without increasing the number of rounds. Proof of Lemma 3.3. Let f solve consensus under A within R rounds. Choose two distinct proposal values, identified with 1 and 2, and let p be the common decision. Suppose that p̄ has received no message from p during the first R rounds. Changing the simulated inputs of p to p̄ leaves the view of p̄ unchanged, so it still decides p. But both proposals are now p̄, contradicting validity. Hence p is a broadcaster in the first R rounds.

6

Undecidability under Not-Nowhere-Dense Message Adversaries

Throughout this section, we use the notation and constructions of Section 3.2. In particular, input sets are singletons, and we identify input signal histories with graph histories.

6.1

Undecidability under the Full Message Adversary

We consider algorithms f = (f1 , f2 ) with fp : Viewsp → Yp . We let fp (vp (h))q , fp (vp (h))zero , fp (vp (h))plan , fp (vp (h))carry , and fp (vp (h))pos be the projections of fp (vp (h)) onto the respective components of the output. The first lemma relies on the indistinguishability relation that forms a line in the view complex and shows that local agreement implies global agreement for all histories at a given round. VERIFIED

Lemma 6.1 ( Lean ). Let f be a distributed algorithm, and let r ≥ 1. If processes 1 and 2 output the same value in round r of every execution, then all vertices of the inputless round-r view complex have the same output label under f .

20

Proof. Every edge of the view complex represents a history that extends to an execution, so its endpoints have equal output labels by assumption. Since the inputless round-r view complex is connected by Lemma 4.2, all vertices have the same output label. We next verify that PosOrd encodes vertex positions modulo 3 and determines the orientation of each edge. VERIFIED

Lemma 6.2 ( Lean ). Let f realize PosOrd. For all r ≥ 1, in the view complex of f at round r, pos(r, i) = i mod 3 for all 0 ≤ i ≤ 3r . Moreover, for all h ∈ Γr , the left endpoint of J(h) is process 1’s view if and only if f2 (v2 (h))pos ≡ f1 (v1 (h))pos + 1 mod 3. Proof. We prove the first statement using induction on r. For all h ∈ Γω , we have exec(f, h) |= PosOrd. Thus, for each such h, (f1 (v1 (h[. . . 1]))pos , f2 (v2 (h[. . . 1]))pos ) = ChildPosh[1] (0, 1) . As ChildPos(1→2) (0, 1) = (0, 1), ChildPos(1↔2) (0, 1) = (2, 1), and ChildPos(1←2) (0, 1) = (2, 0), the statement holds for r = 1. We also have for all h ∈ Γr and g ∈ Γ that     f1 (v1 (h))pos , f2 (v2 (h))pos = (u, v) =⇒ f1 (v1 (hg))pos , f2 (v2 (hg))pos = ChildPosg (u, v) . (19) r r Suppose the first statement is true  ≤ 3 − 1 and let h ∈ Γ such that j(h) =  at round r ≥ 1. Let m m. By the induction hypothesis, f1 (v1 (h))pos , f2 (v2 (h))pos is either (m mod 3, (m + 1) mod 3) or ((m +

1) mod 3, m mod 3). In either case, doing casework on g ∈ Γ and using (19) gives that the vertices at the left and right endpoints of J(hg) output j(hg) mod 3 and (j(hg) + 1) mod 3 as their pos-outputs respectively. Iterating m over 0, 1, . . . , 3r − 1 completes the inductive step. As a consequence of the first statement, if process 1’s view is the left endpoint of J(h) then f2 (v2 (h))pos − f1 (v1 (h))pos ≡ 1 mod 3 and if process 2’s view is the left endpoint then f2 (v2 (h))pos − f1 (v1 (h))pos ≡ −1 mod 3. As 1 and −1 are distinct modulo 3, the condition in the second statement is necessary and sufficient. We provide an LTL formula PathAgr for ensuring (C1).   PathAgr := G (q1 = q2 ) ∧ (zero 1 = zero 2 ) Lemma 6.3 (

VERIFIED

Lean

). Let f realize PathAgr. The view complexes of f satisfy (C1).

Proof. Let h ∈ Γr be an edge at round r in the view complex. Since for all h ∈ Γω , exec(f, h) |= PathAgr, we have that f1 (v1 (h))q = f2 (v2 (h))q and f1 (v1 (h))zero = f2 (v2 (h))zero . Lemma 6.1 applied to the q and the zero components of f gives that all the vertices at round r output the same state q and truth value for zero. Given q ∈ Q and z ∈ {⊤, ⊥} we let m(q, z) be the multplying factor applied to the number of weight-1 edges, defined as follows: Change of counter c 7→ c + 1 c 7→ c c 7→ c − 1

m(q, z) 1 3 9

We give an LTL formula LocalSum for (C2). Observe that since every component ranges over a finite set, every arithmetic constraint over them can be expressed in LTL as a disjunction, over all the possible

21

valuations, of conjunctions of atomic equalities of the form a = p. Hence we use such constraints as atomic propositions. For p ∈ {1, 2}, let p̄ be the other process. For q ∈ Q and z ∈ {⊤, ⊥}, define the LTL formulas ! 2 X ψp (q, z) := (qp = q ∧ zero p = z) → plan p .ak + carry p = m(q, z) · plan p .w + carry p̄ . (20) k=0

Define the LTL formula LocalSum as   ^ ^ LocalSum := G  (OneIsLeft → ψ1 (q, z)) ∧ (¬OneIsLeft → ψ2 (q, z)) .

(21)

q∈Q z∈{⊤,⊥}

Lemma 6.4 (

VERIFIED

Lean

). Let f realize LocalSum and PosOrd. The view complexes of f satisfy (C2).

Proof. Let h ∈ Γω , and h′ ∈ Γr its prefix of length r. Assume, without loss of generality, that the left endpoint of h′ in the view complex of f is process 1’s view. Since f realizes PosOrd, by Lemma 6.2, f2 (v2 (h′ ))pos ≡ f1 (v1 (h′ ))pos + 1 mod 3. Then exec(f, h)[r . . . ] |= OneIsLeft and exec(f, h)[r . . . ] |= ψ1 (q, z) P2 for all q ∈ Q and z ∈ {⊤, ⊥}. Let q := f1 (v1 (h′ ))q and z := f1 (v1 (h′ ))zero . Then, k=0 f1 (v1 (h′ ))plan .ak + f1 (v1 (h′ ))carry = m(q, z) · f1 (v1 (h′ ))plan.w + f2 (v2 (h′ ))carry . If the left endpoint of h′ is the ith vertex, and corresponds to v1 (h′ ), then the (i+1)th vertex is its right endpoint, and it corresponds to v2 (h′ ), by definition of the view complex. Then the view complex of f satisfies (C2). We define, ZeroInd := G [(OneIsLeft ∧ (zero 1 = ⊤ → plan 1 .w = 1)) ∨ (¬OneIsLeft ∧ (zero 2 = ⊤ → plan 2 .w = 1))] , (22) LeftMost := [carry 1 = 0 ∧ (zero 1 = ⊥ → plan 1 .w = 0)] W (graph ̸= (1 → 2)) ,

(23)

RightMost := (carry 2 = 0) W [graph ̸= (1 ← 2)] .

(24)

and based on this, ZeroCheck := ZeroInd ∧ LeftMost ∧ RightMost .

(25)

For ZeroCheck we then show: Lemma 6.5 ( (C3).

VERIFIED

Lean

). Let f realize ZeroCheck, PathAgr, and PosOrd. The view complexes of f satisfy

Proof. Let r ≥ 1. Let h := (1 → 2)r and consider any continuation h′ ∈ Γω . Since f realizes LeftMost, exec(f, h′ ) |= carry 1 = 0 W (graph ̸= (1 → 2)). Since for all d ≤ r, exec(f, h′ )[d . . . ] |= graph = (1 → 2), we have exec(f, h′ )[d . . . ] |= carry 1 = 0 and hence f1 (v1 ((1 → 2)r ))carry = 0. Similarly, since it realizes RightMost, f2 (v2 ((1 ← 2)r ))carry = 0. Hence, carry(r, 0) = carry(r, 3r ) = 0, by Lemma 4.3. Assume now that zero(r, 0) = ⊤ in the view complex of f , i.e., that f1 (v1 ((1 → 2)r ))zero = ⊤. Let h ∈ Γr and assume that its left endpoint is p’s view. Since f realizes PathAgr and PosOrd, by Lemma 6.3, for all h ∈ Γr , f1 (v1 (h))zero = f2 (v2 (h))zero . Applying Lemma 6.1 to the zero part of the output shows that fp (vp (h))zero = ⊤. Since f realizes ZeroInd, fp (vp (h))plan .w = 1. Finally, assume that zero(r, 0) = ⊥. Let h := (1 → 2)r and consider any continuation h′ ∈ Γω . Since zero(r, 0) = ⊥ in the view complex of f , f1 (v1 (h))zero = ⊥. Since f realizes LeftMost, exec(f, h′ ) |= (zero 1 = ⊥ → plan 1 .w = 0) W (graph ̸= (1 → 2)). Since for all d ≤ r, exec(f, h′ )[d . . . ] |= graph = (1 → 2), we have exec(f, h′ )[r . . . ] |= (zero 1 = ⊥ → plan 1 .w = 0) and hence f1 (v1 ((1 → 2)r ))plan .w = 0. To check (C4), we define the LTL formula InitCheck := (q1 = qinit ) ∧ (zero 1 = ⊤) .

22

(26)

VERIFIED

Lemma 6.6 ( Lean of f satisfy (C4).

). Let f realize InitCheck, ZeroCheck, PathAgr, and PosOrd. The view complexes

Proof. Let g ∈ Γ. Since f realizes InitCheck, f1 (v1 (g))q = qinit , and since it realizes PathAgr and PosOrd, f2 (v2 (g))q = f1 (v1 (g))q = qinit . Hence, for every g ∈ Γ, its two endpoints’ outputs are qinit on their qcomponents in the view complex of f , i.e., q(1, j) = qinit for 0 ≤ j ≤ 3. Moreover, f1 (v1 (g))zero = ⊤. Hence, zero(1, 0) = ⊤ in the view complex of f . Since f realizes ZeroCheck, PathAgr and PosOrd, Lemma 6.5 implies that plan(1, j).w = 1, for all 0 ≤ j ≤ 2. For ℓ1 ∈ {⊤, ⊥} that is equal to ⊤ if and only if process 1 is on the left side of the edge, and g ∈ Γ define the function D(τ, g) as follows: D(ℓ1 , g) ℓ1 = ⊤ ℓ1 = ⊥

g = (1 → 2) g = (1 ↔ 2) g = (1 ← 2) 0 1 2 2 1 0

(27)

We can then define formulas Dk (ℓ1 , g), for k ∈ {0, 1, 2}, that are true if and only if D(ℓ1 , g) = k. We use the following shorthand formulas: let x denote one of the components of plan, plan ℓ .x(v) := (OneIsLeft ∧ plan 1 .x = v) ∨ (¬OneIsLeft ∧ plan 2 .x = v) Dk (g) := (OneIsLeft ∧ Dk (⊤, g)) ∨ (¬OneIsLeft ∧ Dk (⊥, g)) Define ^

StateTrans :=

^

[(q1 = q ∧ zero 1 = z) → X (q1 = next(q, z))]

(28)

q∈Q z∈{⊤,⊥}

^

WeightTrans :=

^

^h

i
X(graph = g) ∧ Dk (g) ∧ plan ℓ .ak (b) → X(plan ℓ .w(b))

(29)

k∈{0,1,2} b∈{0,1} g∈Γ

Based on this we set: PropTrans := G (StateTrans ∧ WeightTrans) .

(30)

We can now show the following: Lemma 6.7 (

VERIFIED

Lean

). Let f realize PropTrans and PosOrd. The view complexes of f satisfy (C5).

Proof. Let r ≥ 1, with q(r, 0) = q ∈ Q, and zero(r, 0) = z ∈ {⊤, ⊥} in the view complex of f . Since f realizes PropTrans, we have f1 (v1 ((1 → 2)r+1 ))q = next(q, z); hence q(r + 1, 0) = next(q(r, 0), zero(r, 0)). Let h ∈ Γr and g ∈ Γ, and let h′ ∈ Γω be a continuation of hg. Assume that the left endpoint of h in the inputless view complex is the ith vertex. Following the description of the mapping of the inputless view complex into [0, 1] in Section 2.5, we know that if p is the left endpoint of h, then p̄ is the left endpoint of hg if and only if g = p ↔ p̄. Moreover, condition (C5) requires that if g = p → p̄,

plan p (r, i).a0 = plan p (r + 1, 3i).w,

if g = p ↔ p̄,

plan p (r, i).a1 = plan p̄ (r + 1, 3i + 1).w,

otherwise if g = p ← p̄,

plan p (r, i).a2 = plan p (r + 1, 3i + 2).w .

Assume that process 1 owns the left endpoint of h in the view complex of f . Then, since f realizes PosOrd, by Lemma 6.2, exec(f, h′ )[r . . . ] |= OneIsLeft. Moreover, if g = (1 → 2), D0 (g) holds. If f1 (v1 (h))plan .a0 = b, then, since exec(f, h′ )[r . . . ] |= WeightTrans, we conclude that f1 (v1 (hg))plan .w = b. By construction of the mapping, this implies that w(r +1, 3i) = b. If g = 1 ↔ 2, then, D1 (g) is true. Moreover, again by Lemma 6.2, exec(f, h′ )[r + 1 . . . ] |= ¬OneIsLeft. Then, if a1 (r, i) = b, then w(r + 1, 3i + 1) = b. We can repeat this reasoning for all the other graphs, and similarly if process 2 owns the left endpoint of h.

23

Define the formula  ϕ(Mcounter ) := PosOrd∧PathAgr∧LocalSum∧ZeroCheck∧InitCheck∧PropTrans∧G 

 ^

q1 ̸= q  . (31)

q∈F

We next show: VERIFIED

Lemma 6.8 ( Lean ). Algorithm f realizes ϕ(Mcounter ) if and only if it satisfies conditions (C0)–(C5) and no halting state is output. Proof. (⇒): Assume that f realizes ϕ(Mcounter ). Then, Lemmas 6.2, 6.3,6.4, 6.5, 6.6, V and 6.7 ensure that the view complex of f meets the requirements (C0)–(C5). Moreover, the conjunct G( q∈F q1 ̸= q) excludes halting states from process 1’s outputs, and PathAgr gives the same conclusion for process 2. (⇐): Suppose that f satisfies (C0)–(C5) and outputs no halting state. We next show that f realizes each conjunct of ϕ(Mcounter ). f realizes PosOrd. Indeed, such a view complex implies that f1 (v1 ((1 → 2)))pos = 0, f2 (v2 ((1 → 2)))pos = f2 (v2 ((1 ↔ 2)))pos = 1, f1 (v1 ((1 ↔ 2)))pos = f1 (v1 ((1 ← 2)))pos = 2, and

f2 (v2 ((1 ← 2)))pos = 0 .

V So, for all h ∈ Γω , exec(f, h) |= g∈Γ graph = g → (pos 1 , pos 2 ) = ChildPosg (0, 1) . Let h ∈ Γr have its left endpoint at vertex i, and set u := f1 (v1 (h))pos and v := f2 (v2 (h))pos . If the left endpoint is process 1’s view, then (C0) gives u = i mod 3 and v = (i+1) mod 3. The pairs of integer positions of processes 1 and 2 in h(1 → 2), h(1 ↔ 2), and h(1 ← 2) are, respectively, (3i, 3i + 1), (3i + 2, 3i + 1), and (3i + 2, 3i + 3). Reducing each coordinate modulo 3 gives ChildPos(1→2) (u, v), ChildPos(1↔2) (u, v), and ChildPos(1←2) (u, v), respectively. If the left endpoint is process 2’s view, then (C0) gives u = (i + 1) mod 3 and v = i mod 3. The pairs of integer positions in h(1 → 2), h(1 ↔ 2), and h(1 ← 2) are now (3i + 3, 3i + 2), (3i + 1, 3i + 2), and (3i + 1, 3i). Again, reducing each coordinate modulo 3 gives the corresponding value of ChildPosg (u, v). Thus, in both cases, (C0) yields, for every g ∈ Γ,
f1 (v1 (hg))pos , f2 (v2 (hg))pos = ChildPosg (u, v) . V  V V So, for all h′ ∈ Γω , exec(f, h′ ) |= G ϕ(u, v, g) . Hence, f realizes PosOrd. u∈Z3 v∈Z3 g∈Γ f realizes PathAgr. Since this view complex also satisfies (C1), f realizes PathAgr. Indeed, otherwise there exist r ≥ 1 and h ∈ Γr such that f1 (v1 (h))q ̸= f2 (v2 (h))q or f1 (v1 (h))zero ̸= f2 (v2 (h))zero . But then, the two endpoints of h are labeled by two different values on their q or zero-components, contradicting (C1). f realizes LocalSum. Let r ≥ 1, h ∈ Γr , and h′ ∈ Γω a continuation of h. Assume that the left endpoint of h is process 1’s view (then its right endpoint is process 2’s). Since f realizes PosOrd, f2 (v2 (h))pos ≡ f1 (v1 (h))pos + 1 mod 3, by Lemma 6.2. Hence, exec(f, h′ )[r . . . ] |= OneIsLeft. Moreover, if f1 (v1 (h))q = q and f1 (v1 (h))zero = z, condition (C2) ensures that 2 X

f1 (v1 (h))plan .ak + f1 (v1 (h))carry = m(q, z) · f1 (v1 (h))plan .w + f2 (v2 (h))carry ,

k=0

and exec(f, h′ )[r . . . ] |= ψ1 (q, z). If its left endpoint is process 2’s view, then exec(f, h′ )[r . . . ] |= ¬OneIsLeft and again, one can see that (C2) yields that exec(f, h′ )[r . . . ] |= ψ2 (q, z). Hence f realizes LocalSum. f realizes ZeroCheck. Let r ≥ 1 such that zero(r, 0) = ⊤. Let h ∈ Γr , and h′ ∈ Γω be a continuation of h. Assume that the left endpoint of h is process 1’s view. Then again, since the view complex satisfies (C0), 24

exec(f, h′ )[r . . . ] |= OneIsLeft. Since the view complex satisfies (C1), f1 (v1 (h))zero = zero(r, 0) = ⊤. Since the view complex satisfies (C3), we know that f1 (v1 (h))plan .w = 1, hence exec(f, h′ )[r . . . ] |= OneIsLeft ∧ (zero 1 = ⊤ → plan 1 .w = 1) . If the left endpoint of h is process 2’s view, we have exec(f, h′ )[r . . . ] |= ¬OneIsLeft ∧ (zero 2 = ⊤ → plan 2 .w = 1) , and f realizes ZeroInd. Let h := ((1 → 2))r , and h′ ∈ Γω a continuation of h. By construction, the view of process 1 of h is the leftmost vertex of the view complex at round r. Since carry(r, 0) = 0, exec(f, h′ )[r . . . ] |= carry 1 = 0. Moreover, if zero(r, 0) = f1 (v1 (h))zero = ⊥, plan(r, 0).w = f1 (v1 (h))plan .w = 0, hence exec(f, h′ )[r . . . ] |= zero 1 = ⊥ → (plan 1 .w = 0). Since this holds for all r ≥ 1, exec(f, h′ ) |= [carry 1 = 0 ∧ (zero 1 = ⊥ → plan 1 .w = 0)] W (graph ̸= (1 → 2)) . Similarly, let h := ((1 ← 2))r , and h′ ∈ Γω a continuation of h. By construction, the view of process 2 of h is the rightmost vertex of the view complex at round r. Since carry(r, 3r ) = 0, exec(f, h′ )[r . . . ] |= carry 2 = 0. This being true for any r ≥ 1, we have that exec(f, h′ ) |= (carry 2 = 0) W (graph ̸= (1 ← 2)) . f realizes InitCheck. Condition (C4) implies that fp (vp (g))q = qinit , for p ∈ {1, 2} and g ∈ Γ. Moreover, (C4) gives f1 (v1 ((1 → 2)))plan .w = 1. If f1 (v1 (g))zero = ⊥, then, since by Path Agreement condition (C1), f1 (v1 ((1 → 2)))zero = ⊥, Zero Claim Check condition (C3) states that f1 (v1 ((1 → 2)))plan .w = 0, which is a contradiction. Hence f1 (v1 (g))zero = ⊤, for all g ∈ Γ, and for all h ∈ Γω , exec(f, h) |= InitCheck. f realizes PropTrans. The view complex of f satisfies Proper Transition condition (C5), hence at every round r of the view complex, q(r + 1, 0) = next(q(r, 0), zero(r, 0)). Moreover, since it also satisfies Path Agreement condition (C1), for all h ∈ Γr and g ∈ Γ, f1 (v1 (hg))q = f1 (v1 ((1 → 2)r+1 ))q = next(f1 (v1 ((1 → 2)r ))q , f1 (v1 ((1 → 2)r ))zero ) . Again, by the Path Agreement condition, f1 (v1 ((1 → 2)r ))q = f1 (v1 (h))q and

f1 (v1 ((1 → 2)r ))zero = f1 (v1 (h))zero .

Hence, f realizes G StateTrans. Assume now that f does not realize G WeightTrans. There exist r ≥ 1, h ∈ Γr , g ∈ Γ, 0 ≤ k ≤ 2, 0 ≤ b ≤ 1 such that f2 (v2 (h))pos ≡ f1 (v1 (h))pos + 1

mod 3,

f1 (v1 (h))plan .ak = b, D(⊤, g) = k and

fp (vp (hg))plan .w ̸= b

with p the process whose view is the left endpoint of hg (the case where f2 (v2 (h))pos ̸≡ f1 (v1 (h))pos + 1 mod 3 is symmetric). By Lemma 4.4, if the left endpoint of h is i (even), the left endpoint of hg is the (3i + D(⊤, g))th vertex at round r + 1. But Proper Transition condition (C5) ensures that plan p (r + 1, 3i + k).w = plan 1 (r, i).ak , which is a contradiction. Hence f realizes G WeightTrans V and G StateTrans, and therefore PropTrans. Finally, since no halting state is output, f realizes G( q∈F q1 ̸= q). Together with the preceding conjuncts, this shows that f realizes ϕ(Mcounter ). 25

Correctness of the reduction. izing ϕ(Mcounter ). Lemma 6.9 (

VERIFIED

Lean

We first recover a non-halting run of Mcounter from any algorithm real-

). Suppose that there exists f that realizes ϕ(Mcounter ). Then Mcounter does not halt.

Proof. Lemma 6.8 gives that f satisfies the conditions (C0)–(C5). For r ≥ 1, Path Agreement gives that q(r, i) and zero(r, i) are constant over i ≤ 3r . We denote these constants by q[r] and zero[r], using square brackets for the resulting sequences indexed by round. For i ≤ 3r − 1, define w(r, i) := plan(r, i).w,

sum[r] :=

r 3X −1

w(r, i),

C[r] := − log3 (sum[r] · 3−r ).

i=0

From Local Sum Check, the boundary carry conditions in Zero Claim Check, and Proper Transition, we have sum[r + 1] = m(q[r], zero[r]) · sum[r]. As sum[1] = 3 and m(q[r], zero[r]) ∈ {1, 3, 9}, we get that sum[r] ≥ 3 and hence C[r] ≥ 0 for all r ≥ 1. For r ≥ 1, Zero Claim Check gives that zero[r] = ⊤ if and only if ∀ i ≤ 3r − 1, w(r, i) = 1, which holds if and only if C[r] = 0. We prove the following by induction: (q[1], C[1]), (q[2], C[2]), . . . is the non-halting run of Mcounter . The Initial Check condition gives that q[1] = qinit and C[1] = 0, so the statement holds for r = 1. Suppose that (q[r], C[r]) is the configuration of Mcounter at step r of its run. The Proper Transition condition gives that q[r + 1] = next(q[r], zero[r]). As C[r] = 0 if and only if zero[r] = ⊤, the state of Mcounter at step r + 1 is equal to q[r + 1]. We show the counter value is correctly simulated. We note that: 3−C[r+1] = sum[r + 1] · 3−(r+1) =

m(q[r], zero[r]) −C[r] m(q[r], zero[r]) · sum[r] · 3−r = ·3 . 3 3

Doing casework on q[r] and zero[r] gives: • If ∆(q[r]) is an increment operation, then m(q[r], zero[r]) = 1, so C[r + 1] = C[r] + 1, • if zero[r] = ⊤ and ∆(q[r]) is a decrement operation, then m(q[r], zero[r]) = 3, so C[r + 1] = C[r], • if zero[r] = ⊥ and ∆(q[r]) is a decrement operation, then m(q[r], zero[r]) = 9, so C[r + 1] = C[r] − 1. Thus the value of C[r + 1] corresponds to the counter value of Mcounter in step r + 1. This V concludes the inductive step. Thus (q[1], C[1]), (q[2], C[2]), . . . is the run of Mcounter . As f realizes G( q∈F q1 ̸= q), we have that q[r] ∈ / F for all r ≥ 1.Thus the run is non-halting. It remains to show that there exists a distributed algorithm whose view complex satisfies (C0)–(C5). The following lemma gives a recursive procedure for a process to compute the position of its view in its view complex. VERIFIED

Lemma 6.10 ( Lean ). Let Pos(v) denote the position of view v in its view complex. For h ∈ Γ∗ , denoting vp := vp (h) and vp̄ := vp̄ (h), Pos(I1 ) = 0,

Pos(Np (vp )) = 3 · Pos(vp ),

Pos(Cp (vp , vp̄ )) = Pos(vp ) + 2 · Pos(vp̄ ) ,

Pos(I2 ) = 1,

Pos(Np̄ (vp̄ )) = 3 · Pos(vp̄ ),

Pos(Cp̄ (vp̄ , vp )) = Pos(vp̄ ) + 2 · Pos(vp ) .

(32)

Proof. Views I1 and I2 have positions 0 and 1 by construction. Without loss of generality, assume that vp is on the left vertex of the edge corresponding to h, so Pos(vp̄ ) = Pos(vp )+1. From Figure 4 it is straightforward to see that Pos(Np (vp )) = 3 · Pos(vp ) and Pos(Np̄ (vp̄ )) = 3 · Pos(vp̄ ). It also follows from the same figure that Pos(Cp̄ (vp̄ , vp )) = 3 · Pos(vp ) + 1 = Pos(vp̄ ) + 2 · Pos(vp ) and Pos(Cp (vp , vp̄ )) = 3 · Pos(vp ) + 2 = Pos(vp ) + 2 · Pos(vp̄ ). 26

Algorithm 1: Algorithm f at process p for round r = 1, 2, . . . do Send and receive messages, update view accordingly; 3 if r = 1 then (q, cnt) ← (qinit , 0) else (q, cnt) ← successor configuration of (q, cnt) under ∆(q); 4 view ← view of p; 5 pos ← Pos(view ); 6 if cnt = 0 then zero ← ⊤ else zero ← ⊥; 7 mul ← m(q, zero); 8 w ← ⌊(pos + 1)/3cnt ⌋ − ⌊pos/3cnt ⌋; 9 carry ← ⌊mul · pos/3cnt ⌋ − mul ⌊pos/3cnt ⌋; 10 cnt ′ ← value of counter obtained from successor configuration of (q, cnt) under ∆(q); 11 for k = 0,j 1, 2 do k j k 1

2

12

ak ← (3 · pos + k + 1)/3cnt

′

′

− (3 · pos + k)/3cnt ;

end plan ← (w, a0 , a1 , a2 ); 15 return (q, zero, plan, carry, pos mod 3); 16 end 13 14

Thus at each round of a history, the processes can compute the position of their current views using Pos. Lemma 6.11 (

VERIFIED

Lean

). If Mcounter does not halt, then f given by Algorithm 1 realizes ϕ(Mcounter ).

Proof. In the view complex of f at round r, at the i-th vertex whose view is that of p, for every variable X ∈ {q, cnt, view , pos, mul , carry, cnt ′ , w, a0 , a1 , a2 }, we let X(r, i) denote the value of X at p in round r. Using the fact that x − 1 < ⌊x⌋ ≤ x gives that in any round, w = ⌊(pos + 1)/3cnt ⌋ − ⌊pos/3cnt ⌋ < (pos + 1)/3cnt − pos/3cnt + 1 ≤ 2, implying that w ∈ {0, 1}, and carry = ⌊mul · pos/3cnt ⌋ − mul ⌊pos/3cnt ⌋ < mul · pos/3cnt − mul (pos/3cnt − 1) = mul ≤ 9, implying that carry ∈ {0, . . . , 8}. Lemma 6.10 implies that pos(r, i) = Pos(view ) = i, so f satisfies the Position Order condition. Let the run of Mcounter be (q1 , c1 ), (q2 , c2 ), . . . where (q1 , c1 ) = (qinit , 0). We prove by induction that q(r, i) = qr and cnt(r, i) = cr for all i ≤ 3r . By line 3, q(1, i) = qinit and cnt(1, i) = 0 for 0 ≤ i ≤ 3. In every round r ≥ 2, the values of q and cnt computed in line 3 depend only on their values in the previous round. So if a process always has q = qr and cnt = cr in round r of any run, then it always has q = qr+1 and cnt = cr+1 in round r + 1, which completes the inductive step. From line 6, we deduce that zero(r, i) is constant over all i ≤ 3r . Thus f satisfies Path Agreement. We henceforth write q[r], cnt[r], cnt ′ [r], and zero[r] for the common values at roundPr. 2 We now prove that k=0 ak (r, i) + carry(r, i) = m(q[r], zero[r]) · w(r, i) + carry(r, i + 1). This can be derived from the following formulas, thus showing that f satisfies the Local Sum Check condition. For all k ∈ {0, 1, 2} and j ∈ {i, i + 1}, we have     3 · pos(r, i) + k + 1 3 · pos(r, i) + k − ak (r, i) = 3cnt ′ [r] 3cnt ′ [r]     pos(r, i) + 1 pos(r, i) w(r, i) = − cnt[r] 3 3cnt[r]     mul(r, j) · pos(r, j) pos(r, j) carry(r, j) = − mul(r, j) 3cnt[r] 3cnt[r] ′ cnt [r] = cnt[r] + 1 − log3 m(q[r], zero[r]) mul(r, i) = m(q[r], zero[r]) . If zero[r] = ⊤, then cnt[r] = 0 and so for all i ≤ 3r − 1, we have w(r, i) = ⌊pos + 1⌋ − ⌊pos⌋ = 1. If zero[r] = ⊥, then cnt[r] ≥ 1 and so w(r, 0) = 1/3cnt[r] = 0. As pos(r, 0) = 0, using the above formula for 27

carry(r, j) with j = 0 gives carry(r, 0) = 0. Finally, for r ≥ 1, since cnt[r] < r, we have that 3cnt[r] divides pos(r, 3r ) = 3r , giving that carry(r, 3r ) = 0. Thus f satisfies Zero Claim Check. In round r = 1, q = qinit and cnt = 0, so w(1, i) = 1 for 0 ≤ i ≤ 2. Thus f satisfies Initial Check. From lines 3 and 6, we have that q[r by line 12 in round r we have j k +j1] = next(q[r], zero[r]). Lastly, k ′

′

ak (r, i) = (3 · pos(r, i) + k + 1)3−cnt [r] − (3 · pos(r, i) + k)3−cnt [r] and by line 8 in round r + 1 we have     w(r +1, 3i+k) = (3 · pos(r, i) + k + 1)3−cnt[r+1] − (3 · pos(r, i) + k)3−cnt[r+1] . Both cnt ′ [r] and cnt[r +1] are equal to the counter value in the successor configuration of (q[r], cnt[r]) under ∆(q[r]), thus ak (r, i) = w(r+1, 3i+k). Thus f satisfies the Proper Transition condition. Since Mcounter does not halt and q(r, i) = qr , no halting state is output. By Lemma 6.8, f realizes ϕ(Mcounter ). Finally, Lemmas 6.9 and 6.11 yield the following characterization. Theorem 6.12 (

6.2

VERIFIED

Lean

). Machine Mcounter does not halt if and only if ϕ(Mcounter ) is realizable.

Extension to General Not-Nowhere-Dense Adversaries

We first need a general observation on safety properties. VERIFIED

Lemma 6.13 ( Lean ). Let ϕ be a safety formula and let f be a distributed algorithm. Then f realizes ϕ under A if and only if it realizes ϕ under A. Proof. (⇒): Assume by contradiction that f realizes ϕ under A and that it does not realize ϕ under A. In particular, there exists a graph history h ∈ A \ A such that exec(f, h) ̸∈ L(ϕ). Since L(ϕ) is a safety property, there exists a finite round number R such that exec(f, h′ ) ̸∈ L(ϕ) whenever exec(f, h′ ) agrees with exec(f, h) on the first R rounds. But since the round-R prefix of exec(f, h′ ) only depends on the round-R prefix of h′ , we deduce that exec(f, h′ ) ̸∈ L(ϕ) whenever the round-R prefixes of h and h′ are equal, i.e., when d(h, h′ ) < 2−R . But since A is dense in A, there is an h′ ∈ A with d(h, h′ ) < 2−R . Hence exec(f, h′ ) ̸∈ L(ϕ) for some h′ ∈ A, a contradiction. (⇐): This is trivial since A ⊆ A. We now show how we can exploit the fact that A is not nowhere-dense to obtain undecidability. FORMALIZED

). Let A ⊆ Γω be a message adversary. A finite graph history h ∈ Γ∗ is live Definition 6.14 ( Lean under A if h ∈ Pref(A), i.e., if there exists k ∈ Γω such that h · k ∈ A. An edge of the full inputless view complex is called live under A if its corresponding graph history is live under A. VERIFIED

Lemma 6.15 ( Lean ). Let A ⊆ Γω be a message adversary. Then π(A) is nowhere dense in [0, 1] if and only if, for every h ∈ Γ∗ , there exists k ∈ Γ∗ such that h · k is not live under A. Proof. By Lemma 4.4, the intervals J(u) with u ∈ Γr form a uniform subdivision of [0, 1] into intervals of length 3−r . Hence every nonempty open interval in [0, 1] contains some interval J(u). (⇒): Let h ∈ Γ∗ . Since π(A) is nowhere dense, there exists a nonempty open interval U ⊆ J(h)◦ disjoint from π(A). Choose u ∈ Γ∗ such that J(u) ⊆ U . By Lemma 2.3, we have u = h · k for some k ∈ Γ∗ . If h · k were live, an infinite extension belonging to A would have its image under π in J(h · k) ⊆ U , a contradiction. (⇐): Let 0 ≤ a < b ≤ 1. Choose h ∈ Γ∗ such that J(h) ⊆ (a, b), and then k ∈ Γ∗ such that h · k is not live. By Lemma 5.7,
J(h · k)◦ ∩ π(A) ⊆ π A ∩ h · k · Γω = ∅ . (33) By Lemma 2.3, the nonempty open interval J(h · k)◦ lies in (a, b). Thus every nonempty open interval contains a nonempty open subinterval disjoint from π(A), proving nowhere denseness. VERIFIED

Lemma 6.16 ( Lean ). If π(A) is not nowhere dense, then there exists a finite graph history h ∈ Γ∗ such that h−1 A is dense in Γω . 28

Proof. By Lemma 6.15, there exists an h ∈ Γ∗ such that h · k is live for every k ∈ Γ∗ . Let k ∈ Γω . Denote by k[. . . r] the round-r prefix of k. Since h·k[. . . r] is live, there exists an mr ∈ Γω such that h·k[. . . r]·mr ∈ A. We have k[. . . r] · mr ∈ h−1 A and d(k, k[. . . r] · mr ) < 2−r . Hence k[. . . r] · mr → k as r → ∞. This shows that k ∈ h−1 A and concludes the proof. For the next lemma, use the history h and formula ϕb constructed at the end of Section 3.2. Lemma 6.17 (

VERIFIED

Lean

). A safety formula ϕ is realizable under Γω if and only if ϕb is realizable under A.

Proof. (⇒): Let f be a distributed algorithm that realizes ϕ under Γω . Define algorithm fˆ by outputting arbitrarily during the first |h| rounds and then following f after compressing the initial round-|h| views into a single initial view for each process. Then fˆ realizes X|h| ϕ under h · Γω . Now let k ∈ A. If k ̸∈ h · Γω , then b If k ∈ h · Γω , then exec(fˆ, k) |= Prefixh and exec(fˆ, k) |= X|h| ϕ, so exec(fˆ, k) ̸|= Prefixh , so exec(fˆ, k) |= ϕ. exec(fˆ, k) |= ϕb as well. (⇐): Let fˆ be a distributed algorithm that realizes ϕb under A. The formula ϕb is a safety formula. b its graph prefix is h and its suffix e[|h| + 1 . . . ] violates ϕ. A finite Indeed, if an execution e violates ϕ, b By Lemma 6.13, bad prefix of this suffix, together with the first |h| rounds, forms a finite bad prefix for ϕ. −1 ω ω ˆ b algorithm f realizes ϕ under A. Since h A is dense in Γ , every h · k ∈ h · Γ is a limit of graph histories in A. Thus h · Γω ⊆ A, and fˆ realizes X|h| ϕ under h · Γω . Now define f by replacing the initial view of process p by vp (h) and applying fˆ. Then f realizes ϕ under Γω . Fix A such that π(A) is not nowhere dense. By Lemma 6.16, choose a finite graph history h such that h−1 A is dense in Γω . For a 2-counter machine M , apply the counter encoding to both counters, sharing the control state. The resulting safety formula ϕ(M ) is realizable under Γω if and only if M does not \) is realizable under A. Since h is halt, by Theorem 6.12. By Lemma 6.17, this holds if and only if ϕ(M \ fixed independently of M , the map M 7→ ϕ(M ) is computable. Thus the undecidable non-halting problem for 2-counter machines reduces to LL-Synthesis(A), proving the undecidability direction of Theorem 1.2. Taking A = Γω also proves Theorem 1.1.

7

Decidability via Bounded Component Trees

We prove Theorem 3.4 using the component trees of Section 3.3. We first compute a uniform consensus bound and establish the correspondence between component trees and distributed algorithms. We then bound the number of edges at each node by compression and represent the compressed trees as symbolic trees over a finite alphabet. Finally, we describe the accepting symbolic trees by an MSO formula.

7.1

The Block Automaton and Component Trees

We first compute the consensus bound and construct the block automaton, then prove the correspondence between uncompressed component trees and distributed algorithms. Proof of Lemma 3.6. Construct the automaton Alive recognizing Pref(A) as in Section 3.3. By Lemma 3.2, for every graph history h ∈ Pref(A), consensus started anew after h with fresh proposals is solvable within a bounded number of further rounds under the allowed graph continuations. Because Aadv is deterministic, these continuations depend only on the state reached after h. There are finitely many live states reachable from sinit , so choosing one such algorithm for each state and taking the maximum of their round bounds gives a uniform bound. Iterating over R ≥ 1, compute the following: For each live state s reachable from sinit , compute all live graph histories of length R starting from s. Since there are finitely many local views after R rounds, we can enumerate all distributed algorithms that decide at round R. For each such algorithm, check whether it solves consensus for every live graph history of length R starting from s and every pair of binary proposals. On arbitrary later inputs, the processes simulate these views using their initial proposals and keep their 29

decisions after round R. Conversely, any consensus algorithm deciding within R rounds yields one of these algorithms by fixing each process’s inputs to its proposal and delaying decisions until round R. Thus the test succeeds exactly when consensus is solvable within R rounds under the graph continuations allowed from that state. Stop when the test succeeds for every reachable live state and return D = R. The existence of a uniform bound guarantees that the above search terminates. Proof of Lemma 3.7. Use the automata Alive and Aϕ constructed in Section 3.3. Put M := χϕ (Qϕ ) ∪ {0} and take Q := S × Qϕ × M,

qinit := (sinit , qϕ , 0) ,

Qlive := Flive × Qϕ × M,

χ(s, z, m) := m .

For a block (u, o) ∈ ΣD × ΩD , let z0 = z, z1 , . . . , zD be the states of Aϕ along that block, and define   ∗ δ((s, z, m), (u, o)) := τ (s, Graph(u)), zD , min χϕ (zr ) . 0≤r<D

The successor state stores the minimum priority of the completed block. The minimum includes the starting state and excludes the endpoint, which contributes to the next block. Since blocks have fixed finite length, their minima have the same least infinitely recurring priority as the original run. The extra initial priority 0 does not affect acceptance. The first coordinate gives the required test for allowed prefixes. Proof of Lemma 3.9. (⇒): Suppose that f realizes ϕ under A. Build an uncompressed component tree by labeling every process-p vertex v with fp (v). Inductively, the edge label q(e(h′ )) at each node is the state reached by B on h′ with the outputs of f . Every run follows an infinite input signal history h ∈ Σω . If Graph(h) ∈ A, its execution satisfies ϕ by assumption. Otherwise, B accepts the execution by Lemma 3.7. This also covers graph histories outside A whose every finite prefix is allowed under A. Thus the tree is accepting. (⇐): Fix an accepting uncompressed component tree. Every edge of the round-nD view complex under A belongs to exactly one depth-n node: the assertion holds at the root, and the children partition the allowed extensions of their parent’s edges. Moreover, edges sharing a vertex belong to the same node. Indeed, their preceding block prefixes share a vertex by Lemma 2.1. Inductively, those prefixes lie at the same parent, and the two extensions then lie in the same child component. At every node carrying (K, q), assign its chosen output to each vertex of K (1) , . . . , K (D) that occurs under A. Every possible view at a positive round receives an output. If two occurrences of a view receive outputs from depth-n nodes, their prefixes at round nD share a vertex by Lemma 2.1. They therefore belong to the same node, whose labeling assigns one output to their common view. Assign a fixed default output to initial views and to views that do not occur under A. These assignments define a distributed algorithm f . For h ∈ Σω with Graph(h) ∈ A, the edges en := e(h[. . . nD]) give a run of the tree. Induction on blocks shows that its state labels are the states reached by B under f . Acceptance therefore implies that exec(f, h) |= ϕ. If the tree is effectively given, compute an output from a view by enumerating the finitely many allowed edges at its round. For an incident edge, follow its prefixes through the component tree and read the prescribed output; if there is no such edge, use the default output. The consistency just proved makes the result independent of the chosen edge.

7.2

Compressing Components

Let K and L be subgraphs of view complexes, possibly at different rounds. A map of view complexes T : K → L is a map from the vertices of K to those of L that preserves the owning process and sends edges to edges. For an edge e = {v1 , v2 }, we write T (e) := {T (v1 ), T (v2 )} for its induced image in E(L). The following lemma extends such maps to later rounds.

30

VERIFIED

Lemma 7.1 ( Lean ). Let T : K → L be a map of view complexes as above. For every t ≥ 0, there is a map T (t) : K (t) → L(t) such that T (t) (ew) = T (e)w for all e ∈ E(K) and w ∈ Σt . These extensions preserve identities and composition. Proof. Set T (0) := T . Given T (t) , define the image of a vertex at the next round by Np (x, u) 7−→ Np (x, T (t) (u)) , Cp (x, u, y, v) 7−→ Cp (x, T (t) (u), y, T (t) (v)) . The constructors are disjoint and injective, so these prescriptions give a well-defined map on vertices. By Table 1, the endpoints of an edge ewa are sent to the endpoints of T (e)wa. Thus the map preserves edges and vertex owners. This proves the assertion by induction on t. The same recursion shows that extending an identity gives an identity and that (U ◦ T )(t) = U (t) ◦ T (t) . A reduction at a position (K, q) is a map of view complexes r : K → K such that r ◦ r = r,

q(r(e)) = q(e)

for all e ∈ E(K). Thus r fixes its image and preserves the automaton state on each edge, and hence its priority. Its image r(K) is a nonempty connected subgraph of K. The uniform consensus bound gives the following equality of earlier views within every connected subgraph under A. VERIFIED

Lemma 7.2 ( Lean ). Let A be a message adversary under which consensus is repeatedly solvable in uniformly bounded time D. Let r ≥ D, and let K be a nonempty connected subgraph of the round-r view complex under A. There exists a process p ∈ P such that vp (h[. . . r − D]) = vp (h′ [. . . r − D]) for all h, h′ ∈ Σr with e(h), e(h′ ) ∈ E(K). Proof. Let h ∈ Σr−D satisfy Graph(h) ∈ Pref(A). Under Graph(h)−1 A, consensus is solvable within D rounds. By Lemma 3.3, choose an algorithm fh that makes both processes agree at round D on a broadcaster in these rounds. Simulate fh with fixed local inputs on the communication graphs of the next D rounds. For an edge e(hu) of K, where |h| = r − D and |u| = D, let p be the common decision of this simulation and label the edge by (p, vp (h)). We show that the label depends only on either endpoint. Consider the endpoint vi (hu) of process i. If i received a message in these D rounds, its view contains both round-(r − D) views: its own, and the other process’s view recovered from the received message using Lemma 2.1. These two views determine h by Section 2.4. The endpoint therefore determines which algorithm fh is simulated, its local decision p, and the earlier view vp (h). If i received no message in these rounds, the other process was not a broadcaster, so the common decision must be i. The edge label is then (i, vi (h)), which is again determined by vi (hu). Thus edges sharing a vertex have the same label. Connectivity of K makes this label constant, proving the claim. The number of edges in a component can grow without bound. For example, under A = {(1 → 2)ω } and a fixed input sequence of process 1, the round-r component is a star with one edge for every input sequence of process 2. We use the block that produces a component to construct a reduction with bounded image. (D) Fix a position (K, q), an output labeling λ from K, and a connected component K ′ of Klive . For eu ∈ E(K ′ ), let q ′ (eu) := qλ (e, u). Partition the edges of K that have an extension in K ′ into classes: e and e′ belong to the same class if the following two conditions hold. For every u ∈ ΣD , eu ∈ E(K ′ ) ⇐⇒ e′ u ∈ E(K ′ ) . 31

For every u ∈ ΣD such that eu ∈ E(K ′ ), we also require qλ (e, u) = qλ (e′ , u) . Put a := |Σ|D ,

N := (1 + |Q|)a ,

B := N a,

b := Ba .

(34)

For each block, either the extension is outside K ′ or it has one of |Q| state labels. Thus there are at most N classes, and each edge has at most a extensions. Lemma 7.3 ( such that

VERIFIED

Lean

). Choose one representative of each class. There is a reduction r : K ′ → K ′ at (K ′ , q ′ ) r(eu) = e′ u

(35)

for all eu ∈ E(K ′ ), where e′ is the chosen representative of e. Its image has at most B edges. If |E(K)| ≤ B, (D) then |E(Klive )| ≤ b. Proof. Let K be a subgraph of the round-nD view complex under A. By Lemma 7.2, all edges of K with an extension in K ′ share one process-p vertex. Since distinct edges have distinct pairs of endpoints, their processp̄ endpoints are distinct. Fix the common vertex and send each other endpoint to that of its representative edge. This defines a map T from the subgraph formed by these edges to itself. Its extension T (D) exists by Lemma 7.1. By the definition of the classes, eu ∈ E(K ′ ) implies T (e)u ∈ E(K ′ ). The extension therefore restricts to a map r : K ′ → K ′ satisfying (35). Representatives are fixed by T , so r is idempotent on edges and hence on vertices, since the graphs have no isolated vertices. The same definition gives equality of successor states, and hence of their block priorities. Thus r is a reduction at (K ′ , q ′ ). Its image has at most N representative prefixes, each with at most a extensions, hence at most N a = B (D) edges. If |E(K)| ≤ B, then |E(Klive )| ≤ |E(K)|a ≤ b. FORMALIZED

Definition 7.4 ( Lean ). A compressed component tree carries a position (K, q), a reduction r : K → K with |E(r(K))| ≤ B, and an output labeling λ from r(K) at each node. The root carries (K0 , q0 ). Use (D) the restriction of q to r(K) to compute successor states. Every connected component K ′ of (r(K))live gives exactly one child carrying (K ′ , q ′ ), where q ′ (eu) := qλ (e, u) for all e ∈ E(r(K)) and u ∈ ΣD such that eu ∈ E(K ′ ). These are all its children. A compatible run consists of an infinite branch from the root with positions (Kn , qn ) and reductions rn , together with edges en ∈ E(Kn ) and blocks un ∈ ΣD such that e0 = einit ,

en+1 = rn (en )un ∈ E(Kn+1 ) .

(36)

The tree is accepting if (qn (en ))n≥0 satisfies parity for every compatible run. Every reduced graph has at most B edges, so its allowed extensions have at most b edges. Thus every node has at most b edges and b children. The priority at en+1 is the priority of block n. Figure 5 shows one step of the construction. Preserving state labels alone does not guarantee acceptance: repeated compressions can give compatible runs that do not follow any execution of the original tree. We construct the reductions using an ordinal progress measure to preserve parity. VERIFIED

Theorem 7.5 ( Lean ). An accepting uncompressed component tree exists if and only if an accepting compressed component tree exists. From an effectively given accepting compressed tree, one can effectively construct an accepting uncompressed tree.

32

Figure 5: A reduction and one block along a branch. The reduction rn maps Kn onto rn (Kn ), labelled Kn′ in the figure. Purple arrows show its action on edges, with e′ = rn (e). An output labeling from rn (Kn ) (D) gives the allowed extensions (rn (Kn ))live . Each connected component gives a child Kn+1 ; the middle child is highlighted. Colored vertices represent process views. Proof. (⇒): Fix an accepting uncompressed tree U. Every edge under A at a round divisible by D occurs in exactly one node. Write qU (e) for its state label. Consider the rooted tree whose vertices are these edges and whose transitions are e → eu for allowed extensions eu with u ∈ ΣD . Give this transition the block priority χ(qU (eu)). Every infinite path gives a run of U and satisfies parity. Following the ordinal-rank construction of Berwanger, Mathew, and Ramanujam [BMR16, proof of Theorem 5], we assign to each e a tuple µ(e) of ordinals indexed by the odd priorities in increasing order. For an odd priority d, write f ≺d e when f properly extends e, all transition priorities between them are at least d, and d occurs among them. An infinite descending chain would concatenate to a rejecting path with least infinitely recurring priority d. Thus ≺d is well founded and has ordinal rank µd (e) := sup{µd (f ) + 1 | f ≺d e} , where the supremum of the empty set is zero. Suppose that a nonempty segment from e to f has minimum priority c. For every odd d ≤ c, each ≺d -successor of f is also a ≺d -successor of e, so µd (f ) ≤ µd (e). If c is odd, then f ≺c e, giving a strict decrease in coordinate c. Writing µ≤c for the coordinates at most c, we obtain µ≤c (e) ≥lex µ≤c (f ) , (37) with strict inequality if c is odd. If there are no odd priorities, the tuple is empty. Construct the compressed tree recursively. Associate each of its nodes v with a node w of U at the same depth, maintaining Kv ⊆ Uw , qv = qbw |E(Kv ) , where (Uw , qbw ) is the position at w. The root positions agree, and its reduction is the identity. Suppose that v and its reduction rv have been constructed. Restrict the output labeling at w to the extensions of rv (Kv ). For (D) each component K ′ of (rv (Kv ))live , use the classes of Lemma 7.3 and choose a representative with minimum lexicographic µ-value in each class. Each class is finite and nonempty. The connected graph K ′ lies in a unique child component Uw′ of w. Associate the child v ′ carrying K ′ with w′ , and give it the reduction rv′ : K ′ → K ′ supplied by Lemma 7.3. Every edge of K ′ has its original state label, preserving the invariant. Several compressed children may be associated with the same child of U . Consider a compatible step from v to v ′ using an edge e and a block u. Put f := rv (e), so the next edge is f u, and put g := rv′ (f u). If f ′ is the representative of f chosen for K ′ , then g = f ′ u. Since f and f ′ belong to the same class, qv′ (f u) = qλ (f, u) = qλ (f ′ , u) = qU (g) . 33

Put c := χ(qv′ (f u)). The minimum choice gives µ(f ′ ) ≤lex µ(f ), also after restriction to any initial segment of coordinates. Applying (37) to the transition f ′ → f ′ u yields µ≤c (f ) ≥lex µ≤c (f ′ ) ≥lex µ≤c (g) , with the second inequality strict when c is odd. If a compatible run had odd least infinitely recurring priority d, then eventually all its priorities would be at least d, with d occurring infinitely often. The µ≤d -values of its reduced edges rn (en ) would then be nonincreasing with infinitely many strict decreases, contradicting well-foundedness of lexicographic order on finite tuples of ordinals. The compressed tree is accepting. (⇐): Fix an accepting compressed tree, with positions (Kv , qv ), reductions rv , and output labelings λv . Construct an uncompressed tree whose nodes w carry positions (Uw , qbw ). Associate each w with a compressed node v at the same depth and a map of view complexes Tw : Uw → Kv satisfying qbw (e) = qv (Tw (e))

(38)

for all e ∈ E(Uw ). At the root, take the identity map. Put Tw′ := rv ◦ Tw , with image in rv (Kv ). For each (r) process-p vertex z of Uw , 1 ≤ r ≤ D, set bw )p (z) := (λv )p ((T ′ )(r) (z)) . (λ w The extensions exist by Lemma 7.1, so this defines one output per vertex. The reduction preserves starting states, so copied outputs give qλbw (e, u) = qλv (Tw′ (e), u) for all e ∈ E(Uw ) and u ∈ ΣD . This preserves both the test for allowed extensions and the block priority. (D) (D) For each component U ′ of Uw live , its image under (Tw′ )(D) is a connected subgraph of (rv (Kv ))live . It therefore lies in a single component K ′ at v. Associate the child w′ carrying U ′ with the compressed child v ′ carrying K ′ , and define Tw′ := (Tw′ )(D) |U ′ . This map preserves vertex owners, edges, and successor states, so (38) holds at w′ . On edges this map satisfies Tw′ (eu) = rv (Tw (e))u . Thus every run of the constructed uncompressed tree gives a compatible run of the compressed tree with the same state labels. It is accepting. All steps use finite graphs, output labelings, and the data of the associated compressed node, so the construction is effective when that tree is effectively given.

7.3

Symbolic Component Trees

The graphs in a compressed component tree have bounded size. Up to isomorphism, their reductions, output labelings, and successor components therefore range over finite sets. We use these finite descriptions as the labels of a symbolic component tree. We proceed as follows. Forget the views naming the vertices, retaining each vertex’s owning process and each edge’s automaton state. Choose one representative of each isomorphism class of nonempty connected bipartite graphs with at most b edges, one part per process, and edge labels in Qlive . Choose their vertex sets disjoint, with (K0 , q0 ) representing its class. There are only finitely many representatives. Let E be the union of the edge sets of the chosen representatives. Each node will record its component, how to continue from it, and how its edges were generated from its parent. The alphabet Θ consists of all tuples ℓ = (K, q, r, λ, gen) such that:

34

• (K, q) is one of the chosen representatives; • r : K → K is a reduction at (K, q) with |E(r(K))| ≤ B; • λ is an output labeling from r(K); • gen is either the dummy symbol ∗ for the root or a map E(K) → E × ΣD . For a non-root node w, an entry genw (e′ ) = (b e, u) means that the child edge e′ represents the extension ebu, where eb is an edge of the reduced parent graph. Thus genw describes how the node was reached, while rw , λw describe how to continue from it. The alphabet Θ is finite and effectively computable: all its fields range over finite, effectively enumerable sets. To check how parent and child labels fit together, apply the view constructors for D rounds, starting from distinct formal views at the parent’s vertices. The constructors are disjoint and injective, so this gives exactly the same view equalities as at any concrete realization of the graph. Automaton transitions determine the allowed extensions and their state labels. There are at most b such extensions from the reduced graph, so b child directions suffice. Add a padding letter # for unused child directions. FORMALIZED

). A symbolic component tree is a labeling of the full b-ary tree over Θ ∪ {#} Definition 7.6 ( Lean satisfying the following conditions. The root carries (K0 , q0 ) and the dummy predecessor field ∗. Padding nodes have only padding children. At each non-padding node v, write the label as (Kv , qv , rv , λv , genv ). 1. For each non-padding child w of v, the field genw is a map into E(rv (Kv )) × ΣD . Define βw (e′ ) := ebu (D) whenever genw (e′ ) = (b e, u). There must be a connected component K ′ of (rv (Kv ))live such that βw : E(Kw ) → E(K ′ ) is a bijection and, for all e′ , e′′ ∈ E(Kw ) and p ∈ P, e′p = e′′p

⇐⇒

(βw (e′ ))p = (βw (e′′ ))p .

Thus βw induces an owner-preserving graph isomorphism Kw → K ′ . 2. Each such entry satisfies qw (e′ ) = qλv (b e, u). 3. The sets βw (E(Kw )), as w ranges over the non-padding children of v, are exactly the edge sets of the (D) connected components of (rv (Kv ))live , each occurring once. A compatible run consists of an infinite branch v0 v1 · · · from the root through non-padding nodes, edges en ∈ E(Kvn ) with e0 = einit , and blocks un ∈ ΣD such that, for every n ≥ 0, genvn+1 (en+1 ) = (rvn (en ), un ) .

(39)

Its state sequence is
qvn (en ) n≥0 . The first state is qv0 (e0 ) = qinit , and the priority of block un is χ(qvn+1 (en+1 )).
The tree is accepting if, for every compatible run, the least priority occurring infinitely often in χ(qvn (en )) n≥0 is even. The symbolic encoding preserves acceptance and allows us to reconstruct a compressed component tree. VERIFIED

Lemma 7.7 ( Lean ). An accepting compressed component tree exists if and only if an accepting symbolic component tree exists. From an effectively given accepting symbolic component tree, one can effectively construct an accepting compressed component tree.

35

Proof. By Lemma 7.1, an isomorphism β extends to an isomorphism at every subsequent round, since the extensions of β and β −1 remain inverse maps. It sends a reduction r to β ◦ r ◦ β −1 and transports output labelings and successor components. Corresponding edges read the same signals and outputs from equal states, so their successor states agree. (⇒): Given a compressed component tree, identify each node’s labeled graph with its chosen representative, using the identity at the root. Transport the reductions and output labelings along these isomorphisms, order the children arbitrarily, and add padding. For a child edge e′ , apply the inverse child isomorphism, followed by the extended parent isomorphism, to obtain a formal extension ebu. Set genw (e′ ) := (b e, u) and give the root the dummy field. These tables satisfy the local conditions, since the concrete children are exactly the full components of the allowed extensions. (⇐): Start with the concrete initial position. At each node, transport the recorded reduction and output labeling back along the current isomorphism. For each non-padding child, its generating table induces an isomorphism to one formal successor component by Definition 7.6. Compose it with the inverse of the extended parent isomorphism to identify the child’s representative with a concrete successor component. The local conditions preserve successor states and include every component exactly once. Continue recursively at these children. Under these identifications, the concrete compatibility condition en+1 = rn (en )un is exactly (39). Thus compatible runs correspond in both directions with the same state labels, and acceptance is preserved. Every finite part of the reconstructed compressed tree is computable from the symbolic labels, which include the generating tables.

7.4

Acceptance and the Decision Procedure

It remains to express acceptance of symbolic component trees in MSO. VERIFIED

Lemma 7.8 ( Lean ). One can construct an MSO formula Acc(X) over the full b-ary tree whose models are exactly the accepting symbolic component trees. Proof. Let X = (Xℓ )ℓ∈Θ∪{#} specify the node labels. Let Local(X) require these sets to partition the nodes and satisfy the root, child, and padding conditions of Definition 7.6. The conditions on a node and its children are finite tests on their labels: the generating tables must induce the required isomorphisms, preserve successor states, and cover all successor components exactly once. Since b and the alphabet are finite, these tests are first-order expressible. Describe a compatible run by a set P and a tuple H containing one set He for each edge e of a representative. Require P to contain the root, be closed under ancestors, and contain exactly one child of each of its nodes. The ancestor relation is MSO-definable, so these conditions say that P is an infinite branch. Require the sets He to partition P , with He (v) indicating that the run uses edge e at node v. The root must use einit , and every chosen edge must belong to the representative at its node. For each step along P , require (39). This is a finite test on the parent and child labels and the two chosen edges. Together these conditions define an MSO formula Run(X, P, H) for compatible runs. For each c ∈ χ(Q), let Pric (v) be the finite disjunction of Xℓ (v) ∧ He (v) over letters ℓ and edges e whose recorded state has priority c. With x ≺ y denoting strict ancestry, put
Inf c (X, P, H) := ∀x x ∈ P → ∃y (y ∈ P ∧ x ≺ y ∧ Pric (y)) . On a compatible run, this says that priority c occurs infinitely often. Thus the parity condition is expressed by   Parity(X, P, H) :=

_  ^  Inf d ∧ ¬ Inf c    ,

d∈χ(Q) d even

c∈χ(Q) c<d

where the arguments of Inf c are suppressed on the right. The required formula is
Acc(X) := Local(X) ∧ ∀P ∀H Run(X, P, H) → Parity(X, P, H) . 36

(40)

The generating tables are part of X, so all quantified runs use the same tables, reductions, and output labelings at a node. Padding carries no edges, so compatible runs cannot enter it. Thus Acc holds exactly when the labeling is a symbolic component tree and all its compatible runs satisfy the parity condition. By Rabin’s theorem [Rab69], the models of Acc form an effectively regular tree language with decidable nonemptiness. When nonempty, this language contains a tree that can be effectively generated by a finite labeled graph with one successor per direction. Its labels include the generating tables, so the generator also supplies the correspondence data needed for reconstruction. Proof of Theorem 3.4. Emptiness of A is decidable; if A = ∅, any distributed algorithm suffices. Otherwise, compute D by Lemma 3.6, construct the block automaton B, and compute the bounds in (34). Construct the formula Acc of Lemma 7.8. The preceding results give ϕ is realizable under A ⇐⇒ an accepting uncompressed component tree exists ⇐⇒ an accepting compressed component tree exists ⇐⇒ an accepting symbolic component tree exists ⇐⇒ Acc has a model . The last condition is decidable. In the positive case, construct a finite generator of a model. The effective constructions of Lemmas 3.9 and 7.7 and Theorem 7.5 yield a realizing distributed algorithm, reconstructing finite parts of the component trees as needed. This yields computable local output functions. We do not claim finite-state implementations.

8

Conclusion

In this work, we presented a characterization of the communication assumptions under which distributed synthesis is decidable for two processes. Our results shed new light on the limits of distributed synthesis by relating decidability to the uncertainty processes have about the system. In the inputless setting, paths describe chains of indistinguishable histories. If a path keeps refining without gaps, its growing length allows us to encode unbounded counters and also prevents consensus from being repeatedly solved in bounded time. Otherwise, if gaps always appear within a fixed number of rounds, repeated consensus becomes possible, which we use to decide synthesis. The same uncertainty thus links the two previously unrelated problems from formal verification and distributed computing. We conjecture that a link between the two problems also holds in larger systems. A further natural open question is to characterize the message adversaries for which synthesis is decidable when the empty communication graph is also allowed, with a promising observation that our technique also proves undecidability for two processes with independent inputs and no communication as studied by Pnueli and Rosner [PR90]. The idea is to use an LTL safety assumption to prune the input histories so that the view complexes form the same growing paths as in our proof. We can then directly reuse our counter encoding. Concerning time complexity, for each fixed ω-regular adversary A with nowhere-dense image, our construction places LL-Synthesis(A) in 4Exptime. Here n is the total size of the specification and the input and output alphabets. An automaton for A and its uniform consensus bound D are treated as constants. The size of B and the bounds B and b (see (34)) are at most doubly exponential in n. It follows that the size of the symbolic alphabet and its transition tables is at most triply exponential in n. Local consistency and acceptance of every compatible run can be checked by a universal parity tree automaton of size polynomial in these tables. Its nonemptiness can be decided in exponential time [Wil01], giving the stated upper bound. A lower bound already holds for the fixed adversary A = {(1 ↔ 2)ω }: this case is equivalent to centralized LTL synthesis, which is 2Exptime-complete [PR88]. Thus synthesis in the decidable cases is 2Exptime-hard. Determining the exact complexity and improving this upper bound remain open. Finally, a natural open question is whether binary outputs suffice for the undecidability direction of our characterization. 37

AI Statement The question of synthesis in the LL model without acknowledgments arose following the 2022 Information and Computation paper [BBB+ 22]. Conjecturing decidability, we worked on algorithms, realizing a close relation to consensus to determine a changing leader. After years of discussions and proofs of decidability for special cases by hand, without AI assistance, we started to also work towards undecidability for other cases. We later supplied drafts of these results to AI models, whose initial attempts did not resolve the general problem. We then redirected the prompts toward proving undecidability, suggesting the use of indistinguishability chains to encode a computation, initially through tilings. After weeks of discussions with different models in this direction, OpenAI’s GPT-6 Astra finally produced an undecidability proof based on a 2-counter machine. The subsequent development involved extensive collaboration with the model through further prompting, revisions, and simplifications of the arguments. These included replacing a parity-game formulation by a tree-language formulation and introducing and using view complexes, among many other changes. The formulation of the decidability boundary in terms of nowhere dense sets, and the results connecting this boundary to consensus, were developed entirely by the authors, without AI assistance. The AI-assisted work initially yielded a Lean formalization and a LATEX draft. Starting from these results, we wrote a new manuscript from scratch, without reusing any text from the AI-generated LATEX draft. AI tools were subsequently used to help revise and edit the manuscript. Finally, we used AI again to formalize in Lean the statements and proofs as written in this paper. The authors take full responsibility for the results and the content of the paper.

Acknowledgments We would like to thank Béatrice Bérard for many fruitful discussions on the synthesis problem and for her helpful comments on a preliminary version of the manuscript. We also thank Betsalel Guinard for discussion on the “smile” algorithm. This work received funding from ANR through DREAMY (ANR-21-CE48-0003) and COSTXPRESS (ANR-23-CE45-0013), and from the France 2030 investment plan through SAIF (ANR23-PEIA-0006), administered by ANR.

A

LTL Syntax and Semantics

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 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 of LTL formulas is given by the following grammar, in which p ∈ P, x ∈ Xp , y ∈ Yp , and g ∈ Γ: ϕ ::=(inp = x)|(outp = y)|(graph = g)|

atomic formulas

Xϕ | Fϕ | Gϕ | ϕ U ϕ | ϕ W ϕ ¬ϕ | ϕ ∨ ϕ | ϕ ∧ ϕ | ϕ → ϕ | ϕ ↔ ϕ

temporal modalities Boolean connectives

Let e ∈ (Σ × Ω)ω be an execution, and let h := Graph(e) be its graph history. Write the round-r letter of e as e[r] = ((x1 [r], x2 [r], h[r]), (y1 [r], y2 [r])) (r ≥ 1) .

38

Boolean connectives are interpreted as usual. Moreover:

B

e |= (inp = x)

if xp [1] = x

e |= (outp = y)

if yp [1] = y

e |= (graph = g)

if h[1] = g

e |= X ϕ

if e[2 . . . ] |= ϕ

e |= F ϕ

if ∃r ≥ 1 : e[r . . . ] |= ϕ

e |= G ϕ

if ∀r ≥ 1 : e[r . . . ] |= ϕ

e |= ϕ U ψ

if ∃r ≥ 1 : (e[r . . . ] |= ψ ∧ ∀1 ≤ r′ < r : e[r′ . . . ] |= ϕ)

e |= ψ W ϕ

if e |= G ψ ∨ ψ U ϕ

Lean Formalization

For the Lean formalization, we used a two-agent workflow [FN26], where one agent proposes the Lean formalization and the other checks its correspondence with the natural-language statements and proofs. We reuse definitions and results from Mathlib (v4.30.0) wherever possible, including its real numbers and topology, finite-type and encoding infrastructure, and computability theory. For example, primitive recursiveness and algorithmic decidability use Mathlib’s Primrec and ComputablePred, respectively, and nowhere denseness uses its topological definition IsNowhereDense in the relative topology on [0, 1]. For every ω-regular message adversary A, our main theorem (Theorem 1.2) is expressed in the formalization as ComputablePred (Realizable A) ↔ IsNowhereDense (geometricMap '' A) Here, geometricMap '' A denotes π(A), and realizability quantifies existentially over pairs of local strategies and universally over all executions whose graph history belongs to adversary A, with unrestricted private input streams. Instances include the finite nonempty input and output alphabets, the interpretation of atomic propositions, and the LTL formula. The positive result additionally provides a primitive-recursive Boolean decision procedure for each fixed ω-regular adversary with nowhere dense geometric image. LTL syntax and its semantics on infinite words are defined in our development. Our MSO formalization extends Mathlib’s first-order syntax and semantics with quantification over arbitrary sets, including infinite sets. To support the LTL and MSO translations, our automata library provides Büchi and parity automata on infinite words and parity automata on infinite trees, which are not available in Mathlib at the time of writing. It includes Piterman’s determinization [Pit07], whose correctness is proved in the development. The undecidability proof ultimately rests on Mathlib’s halting undecidability theorem, through a verified chain of reductions incorporating Lean adaptations of counter-machine constructions from the Rocq library of undecidability proofs [FLWD+ 20].

References [ACGN26]

Hagit Attiya, Armando Castañeda, Dhrubajyoti Ghosh, and Thomas Nowak. Equivalence and separation between Heard-Of and asynchronous message-passing models. In Chryssis Georgiou, editor, Proceedings of the 33rd International Colloquium on Structural Information and Communication Complexity (SIROCCO 2026), volume 16488 of Lecture Notes in Computer Science, pages 53–72, Cham, 2026. Springer. doi:10.1007/978-3-032-26465-7_4.

[AG15]

Yehuda Afek and Eli Gafni. A simple characterization of asynchronous computations. Theoretical Computer Science, 561:88–95, 2015. doi:10.1016/j.tcs.2014.07.022.

[AS85]

Bowen Alpern and Fred B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, 1985. doi:10.1016/0020-0190(85)90056-0. 39

[AVW03]

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-3 975(02)00442-5.

[BBB+ 22]

Béatrice Bérard, Benedikt Bollig, Patricia Bouyer, Matthias Függer, and Nathalie Sznajder. Synthesis in presence of dynamic links. Information and Computation, 289:104856, 2022. doi: 10.1016/j.ic.2021.104856.

[BCJ18]

Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann. Graph games and reactive synthesis. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 921–962. Springer, Cham, 2018. doi:10.1007/97 8-3-319-10575-8_27.

[BL69]

J. Richard Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295–311, 1969. doi:10.1 090/S0002-9947-1969-0280205-0.

[BMR16]

Dietmar Berwanger, Anup Basil Mathew, and R. Ramanujam. A retraction theorem for distributed synthesis, 2016. arXiv:1604.07564 [cs.DC]. doi:10.48550/arXiv.1604.07564.

[BMvdB15] Dietmar Berwanger, Anup Basil Mathew, and Marie van den Bogaard. Hierarchical information patterns and distributed strategy synthesis. In Bernd Finkbeiner, Geguang Pu, and Lijun Zhang, editors, Proceedings of the 13th International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), volume 9364 of Lecture Notes in Computer Science, pages 378–393, Cham, 2015. Springer. doi:10.1007/978-3-319-24953-7_28. [Bou98]

Nicolas Bourbaki. General Topology: Chapters 1–4. Elements of Mathematics. Springer, Heidelberg, 1998. doi:10.1007/978-3-642-61701-0.

[CBFN15]

Bernadette Charron-Bost, Matthias Függer, and Thomas Nowak. Approximate consensus in highly dynamic networks: The role of averaging algorithms. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Proceedings of the 42nd International Colloquium on Automata, Languages, and Programming (ICALP 2015), volume 9135 of Lecture Notes in Computer Science, pages 528–539, Heidelberg, 2015. Springer. doi:10.1007/978-3-662-47666-6_42.

[CBS09]

Bernadette Charron-Bost and André Schiper. The Heard-Of model: computing in distributed systems with benign faults. Distributed Computing, 22(1):49–71, 2009. doi:10.1007/s00446 -009-0084-6.

[CFQS12]

Arnaud Casteigts, Paola Flocchini, Walter Quattrociocchi, and Nicola Santoro. Time-varying graphs and dynamic networks. International Journal of Parallel, Emergent and Distributed Systems, 27(5):387–408, 2012. doi:10.1080/17445760.2012.668546.

[CG23]

Yannis Coutouly and Emmanuel Godard. A topology by geometrization for sub-iterated immediate snapshot message adversaries and applications to set-agreement. In Rotem Oshman, editor, Proceedings of the 37th International Symposium on Distributed Computing (DISC 2023), volume 281 of Leibniz International Proceedings in Informatics, pages 15:1–15:20, Dagstuhl, 2023. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.DISC.2023.1 5.

[CGP15]

Étienne Coulouma, Emmanuel Godard, and Joseph Peters. A characterization of oblivious message adversaries for which consensus is solvable. Theoretical Computer Science, 584:80–90, 2015. doi:10.1016/j.tcs.2015.01.024.

40

[Chu57]

Alonzo Church. Application of recursive arithmetic to the problem of circuit synthesis. In Summaries of Talks Presented at the Summer Institute for Symbolic Logic, volume 1, pages 3–50, Ithaca, 1957. Cornell University.

[Chu63]

Alonzo Church. Logic, arithmetic, and automata. In V. Stenström, editor, Proceedings of the 14th International Congress of Mathematicians (ICM 1962), pages 23–35, Djursholm, 1963. Institut Mittag-Leffler.

[Fij26]

Nathanaël Fijalkow, editor. Games on Graphs: From Logic and Automata to Algorithms. Cambridge University Press, Cambridge, 2026. doi:10.1017/9781009500678.

[FLWD+ 20] Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, and Maximilian Wuttke. A Coq library of undecidable problems. The Sixth International Workshop on Coq for Programming Languages (CoqPL 2020), 2020. URL: https://popl20.sigplan.org/details/CoqPL-202 0-papers/5/A-Coq-Library-of-Undecidable-Problems. [FN26]

Matthias Függer and Thomas Nowak. Adding “verified” badges to our paper, one lemma at a time. Bulletin of the EATCS, 149:24–32, 2026. URL: https://eatcs.org/images/bulletin/ beatcs149.pdf.

[FS05]

Bernd Finkbeiner and Sven Schewe. Uniform distributed synthesis. In Prakash Panangaden, editor, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS 2005), pages 321–330, Piscataway, 2005. IEEE. doi:10.1109/LICS.2005.53.

[GGMW13] Blaise Genest, Hugo Gimbert, Anca Muscholl, and Igor Walukiewicz. Asynchronous games over tree architectures. In Fedor V. Fomin, Rūsiņš Freivalds, Marta Kwiatkowska, and David Peleg, editors, Proceedings of the 40th International Colloquium on Automata, Languages, and Programming (ICALP 2013), volume 7966 of Lecture Notes in Computer Science, pages 275– 286, Heidelberg, 2013. Springer. doi:10.1007/978-3-642-39212-2_26. [Gim22]

Hugo Gimbert. Distributed asynchronous games with causal memory are undecidable. Logical Methods in Computer Science, 18(3):30:1–30:22, 2022. doi:10.46298/lmcs-18(3:30)2022.

[GLZ04]

Paul Gastin, Benjamin Lerman, and Marc Zeitoun. Distributed games with causal memory are decidable for series-parallel systems. In Kamal Lodaya and Meena Mahajan, editors, Proceedings of the 24th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2004), volume 3328 of Lecture Notes in Computer Science, pages 275–286, Heidelberg, 2004. Springer. doi:10.1007/978-3-540-30538-5_23.

[GP20]

Emmanuel Godard and Eloi Perdereau. Back to the coordinated attack problem. Mathematical Structures in Computer Science, 30(10):1089–1113, 2020. doi:10.1017/S0960129521000037.

[GSZ09]

Paul Gastin, Nathalie Sznajder, and Marc Zeitoun. Distributed synthesis for well-connected architectures. Formal Methods in System Design, 34(3):215–237, 2009. doi:10.1007/s10703 -008-0064-7.

[HKR14]

Maurice Herlihy, Dmitry N. Kozlov, and Sergio Rajsbaum. Distributed Computing Through Combinatorial Topology. Morgan Kaufmann, Waltham, 2014. doi:10.1016/C2011-0-07032-1.

[KMTZ13]

Jonathan Katz, Ueli Maurer, Björn Tackmann, and Vassilis Zikas. Universally composable synchronous computation. In Amit Sahai, editor, Proceedings of the 10th Theory of Cryptography Conference (TCC 2013), volume 7785 of Lecture Notes in Computer Science, pages 477–498, Heidelberg, 2013. Springer. doi:10.1007/978-3-642-36594-2_27.

41

[KV97]

Orna Kupferman and Moshe Y. Vardi. Synthesis with incomplete information. In Howard Barringer, Michael Fisher, Dov Gabbay, and Graham Gough, editors, Proceedings of the 2nd International Conference on Temporal Logic (ICTL 1997), pages 91–106, Manchester, 1997. University of Manchester.

[KV01]

Orna Kupferman and Moshe Y. Vardi. Synthesizing distributed systems. In Joseph Y. Halpern, editor, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), pages 389–398, Piscataway, 2001. IEEE. doi:10.1109/LICS.2001.932514.

[Lam98]

Leslie Lamport. The part-time parliament. ACM Transactions on Computer Systems, 16(2):133–169, 1998. doi:10.1145/279227.279229.

[LM95]

Ronit Lubitch and Shlomo Moran. Closed schedulers: a novel technique for analyzing asynchronous protocols. Distributed Computing, 8(4):203–210, 1995. doi:10.1007/BF02242738.

[Min67]

Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs, 1967.

[MW14]

Anca Muscholl and Igor Walukiewicz. Distributed synthesis for acyclic architectures. In Venkatesh Raman and S. P. Suresh, editors, Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014), volume 29 of Leibniz International Proceedings in Informatics, pages 639–651, Dagstuhl, 2014. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.FSTTCS.2014.639.

[NSW24]

Thomas Nowak, Ulrich Schmid, and Kyrill Winkler. Topological characterization of consensus in distributed systems. Journal of the ACM, 71(6):1–48, 2024. doi:10.1145/3687302.

[Pit07]

Nir Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. Logical Methods in Computer Science, 3(3:5):1–21, 2007. doi:10.2168/LMCS-3(3: 5)2007.

[Pnu77]

Amir Pnueli. The temporal logic of programs. In Paul Young, editor, Proceedings of the 18th Annual IEEE Symposium on Foundations of Computer Science (FOCS 1977), pages 46–57, Piscataway, 1977. IEEE. doi:10.1109/SFCS.1977.32.

[PP04]

Dominique Perrin and Jean-Éric Pin. Infinite Words: Automata, Semigroups, Logic and Games, volume 141 of Pure and Applied Mathematics. Elsevier, Amsterdam, 2004. doi:10.1016/S007 9-8169(04)X8001-6.

[PR88]

Amir Pnueli and Roni Rosner. A framework for the synthesis of reactive modules. In Frederich H. Vogt, editor, Proceedings of the International Conference on Concurrency (CONCURRENCY 1988), volume 335 of Lecture Notes in Computer Science, pages 4–17, Heidelberg, 1988. Springer. doi:10.1007/3-540-50403-6_28.

[PR90]

Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In Mihalis Yannakakis, editor, Proceedings of the 31st Annual IEEE Symposium on Foundations of Computer Science (FOCS 1990), volume II, pages 746–757, Piscataway, 1990. IEEE. doi:10.1109/FSCS.1990.89597.

[Rab69]

Michael O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1–35, 1969. doi:10.1090/S0002-9947-1 969-0246760-1.

[Rab72]

Michael Oser Rabin. Automata on Infinite Objects and Church’s Problem, volume 13 of CBMS Regional Conference Series in Mathematics. American Mathematical Society, Providence, 1972. doi:10.1090/cbms/013. 42

[Sis94]

A. Prasad Sistla. Safety, liveness and fairness in temporal logic. 6(5):495–511, September 1994. doi:10.1007/BF01211865.

[ST87]

T. K. Srikanth and Sam Toueg. Optimal clock synchronization. Journal of the ACM, 34(3):626– 645, 1987. doi:10.1145/28869.28876.

[SW89]

Nicola Santoro and Peter Widmayer. Time is not a healer. In Burkhard Monien and Robert Cori, editors, Proceedings of the 6th Annual Symposium on Theoretical Aspects of Computer Science (STACS 1989), volume 349 of Lecture Notes in Computer Science, pages 304–313, Heidelberg, 1989. Springer. doi:10.1007/bfb0028994.

[SWK09]

Ulrich Schmid, Bettina Weiss, and Idit Keidar. Impossibility results and lower bounds for consensus under link failures. SIAM Journal on Computing, 38(5):1912–1951, 2009. doi: 10.1137/s009753970443999x.

[Tho90]

Wolfgang Thomas. Automata on infinite objects. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pages 133–191. Elsevier, Amsterdam, 1990. doi:10.1016/B978-0-444-88074-1.50009-3.

[Tho08]

Wolfgang Thomas. Church’s problem and a tour through automata theory. In Arnon Avron, Nachum Dershowitz, and Alexander Rabinovich, editors, Pillars of Computer Science, volume 4800 of Lecture Notes in Computer Science, pages 635–655. Springer, Heidelberg, 2008. doi: 10.1007/978-3-540-78127-1_35.

[vdMW05]

Ron van der Meyden and Thomas Wilke. Synthesis of distributed systems from knowledgebased specifications. In Martı́n Abadi and Luca de Alfaro, editors, Proceedings of the 16th International Conference on Concurrency Theory (CONCUR 2005), volume 3653 of Lecture Notes in Computer Science, pages 562–576, Heidelberg, 2005. Springer. doi:10.1007/115394 52_42.

[Wil01]

Thomas Wilke. Alternating tree automata, parity games, and modal µ-calculus. Bulletin of the Belgian Mathematical Society – Simon Stevin, 8(2):359–391, 2001. doi:10.36045/bbms/1102 714178.

[WSS19]

Kyrill Winkler, Manfred Schwarz, and Ulrich Schmid. Consensus in rooted dynamic networks with short-lived stability. Distributed Computing, 32(5):443–458, 2019. doi:10.1007/s00446 -019-00348-0.

43

Form. Asp. Comput.,

Related documents

• RTLCurator: Label-Efficient Data Curation for RTL Generation#422273
• PCCL: Process Group-Aware Scalable and Generic Collective Algorithm Synthesizer#266145
• Toward Secure Code Generation: Bridging Correctness and Security via Task-Adaptive Vulnerability Modeling and Execution-Based Benchmarking#1083973
• When Simulation Lies: A Sim-to-Real Benchmark and Domain-Randomized RL Recipe for Tool-Use Agents#1297129
• Isabelle/STARK: A Formalization of zk-STARK in Isabelle/HOL#1061765