Distributed LTL Synthesis under Arbitrary Message Adversaries
Benedikt Bollig, Patricia Bouyer-Decitre, Matthias Függer, Dhrubajyoti Ghosh, Thomas Nowak, Nathalie Sznajder
cs.DC
Nov 3, 2026 · v1
cs.FL cs.LO eess.SY
TL;DR
Main results are machine-checked in Lean 4 with Mathlib, including new automata libraries, MSO formalization, and undecidability reductions to Mathlib's halting theorem.
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) \subseteq [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.
Problem
The paper studies distributed reactive synthesis from LTL specifications for two processes that communicate in rounds over unreliable links, where at least one message is delivered per round. The goal is to determine which message adversaries make synthesis decidable.
Approach
Graph histories are mapped to points of the unit interval via iterated chromatic subdivision, giving an image π(A). Undecidability is shown by encoding counters in the growing paths of view complexes. Decidability is obtained via bounded component trees, symbolic trees, and an MSO encoding. Results are formalized in Lean 4 with Mathlib, adding Büchi and parity automata on words and trees, MSO semantics, and counter-machine reductions adapted from the Rocq undecidability library.
Results
For ω-regular message adversaries, synthesis is decidable if and only if π(A) is nowhere dense, which is equivalent to consensus being repeatedly solvable in bounded time. Synthesis is undecidable even under the full adversary with complete causal histories, and the decidable cases are in 4EXPTIME.