Synthesizing Computable Functions from Rational Specifications over Infinite Words
Emmanuel Filiot, Sarah Winter
TL;DR
The paper investigates automatic synthesis of computable streaming functions from rational specifications over infinite words, proving undecidability in general. It introduces an incomplete but sound reduction to an unbounded-delay omega-regular game whose winning strategies yield uniformizers computable by a deterministic two-way transducer, and identifies a sufficient completeness condition that ensures decidability for deterministic rational relations. The authors show ExpTime-completeness for synthesizing from deterministic rational specifications, encompassing automatic relations as a key subclass. They further connect continuity notions to strategies, establishing that for DRAT and AUT specifications, uniformizability by computable functions coincides with realizability by two-way transducers, and discuss the implications for bounded-delay and closed-domain cases. These results illuminate the memory and complexity requirements for reactive synthesis in a broad, asynchronous omega-word setting and point to open questions about sequential realizability and practical constrained implementations.
Abstract
The synthesis problem asks to automatically generate, if it exists, an algorithm from a specification of correct input-output pairs. In this paper, we consider the synthesis of computable functions of infinite words, for a classical Turing computability notion over infinite inputs. We consider specifications which are rational relations of infinite words, i.e., specifications defined non-deterministic parity transducers. We prove that the synthesis problem of computable functions from rational specifications is undecidable. We provide an incomplete but sound reduction to some parity game, such that if Eve wins the game, then the rational specification is realizable by a computable function. We prove that this function is even computable by a deterministic two-way transducer. We provide a sufficient condition under which the latter game reduction is complete. This entails the decidability of the synthesis problem of computable functions, which we prove to be ExpTime-complete, for a large subclass of rational specifications, namely deterministic rational specifications. This subclass contains the class of automatic relations over infinite words, a yardstick in reactive synthesis.