We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Formal Languages and Automata Theory

Title: Synthesizing Computable Functions from Rational Specifications over Infinite Words

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.
Subjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)
Cite as: arXiv:2103.05674 [cs.FL]
  (or arXiv:2103.05674v3 [cs.FL] for this version)

Submission history

From: Sarah Winter [view email]
[v1] Tue, 9 Mar 2021 19:21:00 GMT (486kb)
[v2] Fri, 30 Jul 2021 09:03:27 GMT (512kb,D)
[v3] Wed, 6 Oct 2021 09:43:35 GMT (537kb,D)

Link back to: arXiv, form interface, contact.