Distributed LTL Synthesis under Arbitrary Message Adversaries

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.