No Access

Synthesizing Computable Functions from Rational Specifications Over Infinite Words

Emmanuel Filiot

https://orcid.org/0000-0002-2520-5630

Département d’Informatique, Université libre de Bruxelles, Campus de la Plaine, 1050, Bruxelles, Belgium

E-mail Address: [email protected]

Emmanuel Filiot is a senior research associate at F.R.S.-FNRS.

Search for more papers by this author

and

Sarah Winter

https://orcid.org/0000-0002-3499-1995

Département d’Informatique, Université libre de Bruxelles, Campus de la Plaine, 1050, Bruxelles, Belgium

E-mail Address: [email protected]

Corresponding author. Sarah Winter is a postdoctoral researcher at F.R.S.-FNRS.

Search for more papers by this author

https://doi.org/10.1142/S012905412348009XCited by:0 (Source: Crossref)

This article is part of the issue:

Special Issue: Articles Dedicated to the Memory of Magnus Steinby
Guest Editors: Zoltán Fülöp (University of Szeged, Hungary), George Rahonis (University of Thessalonikim Greece) and Kai Salomaa (Queen’s University, Canada)

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 by 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 proved 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.

This work is partially supported by the MIS project F451019F (F.R.S.- FNRS).

Communicated by George Rahonis

Keywords:

References

1. S. Almagor and O. Kupferman, Good-enough synthesis, In International Conference on Computer Aided Verification (Springer, 2020), pp. 541–563. Crossref, Google Scholar
2. R. Alur, R. Bodík, E. Dallal, D. Fisman, P. Garg, G. Juniwal, H. Kress-Gazit, P. Madhusudan, M. M. K. Martin, M. Raghothaman, S. Saha, S. A. Seshia, R. Singh, A. Solar-Lezama, E. Torlak and A. Udupa, Syntax-guided synthesis, In Dependable Software Systems Engineering (IEEE, 2015), pp. 1–25. Google Scholar
3. R. Alur, E. Filiot and A. Trivedi, Regular transformations of infinite strings, In 2012 27th Annual IEEE Symposium on Logic in Computer Science (IEEE, 2012), pp. 65–74. Crossref, Google Scholar
4. A. V. Arkhangel’skıı̃ and V. V Fedorchuk, The basic concepts and constructions of general topology, In General Topology I (Springer, 1990), pp. 1–90. Crossref, Google Scholar
5. J. Berstel, Transductions and context-free languages, Teubner Studienbücher : Informatik, Vol. 38 (Teubner, 1979). Crossref, Google Scholar
6. R. Bloem, R. Ehlers and R. Könighofer, Cooperative reactive synthesis, In Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings, B. Finkbeiner, G. Pu and L. Zhang (eds.), Lecture Notes in Computer Science, Vol. 9364 (Springer, 2015), pp. 394–410. Google Scholar
7. R. Brenguier, J. Raskin and O. Sankur, Assume-admissible synthesis, Acta Informatica 54(1) (2017) 41–83. Crossref, Web of Science, Google Scholar
8. J. R. Büchi and L. H. Landweber, Solving sequential conditions by finite-state strategies, Trans. Amer. Math. Soc. 138 (1969) 295–311. Crossref, Web of Science, Google Scholar
9. A. Carayol and C. Löding, Uniformization in Automata Theory, In Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science Nancy, July 19-26, 2011 (London: College Publications, 2014), pp. 153–178. Google Scholar
10. O. Carton and G. Douéneau-Tabot, Continuous rational functions are deterministic regular, In MFCS, LIPIcs, Vol. 241 (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022), pp. 28:1–28:13. Google Scholar
11. K. Chatterjee and T. A. Henzinger, Assume-guarantee synthesis, In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings, O. Grumberg and M. Huth (eds.), Lecture Notes in Computer Science, Vol. 4424 (Springer, 2007), pp. 261–275. Google Scholar
12. C. Choffrut and S. Grigorieff, Uniformization of rational relations, In Jewels are Forever (Springer, 1999), pp. 59–71. Crossref, Google Scholar
13. E. M. Clarke, T. A. Henzinger, H. Veith and R. Bloem, Handbook of Model Checking, Vol. 10 (Springer, 2018). Crossref, Google Scholar
14. R. Condurache, E. Filiot, R. Gentilini and J.-F. Raskin, The complexity of rational synthesis, In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, I. Chatzigiannakis, M. Mitzenmacher, Y. Rabani and D. Sangiorgi (eds.), LIPIcs, Vol. 55 (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016), pp. 121:1–121:15. Google Scholar
15. V. Dave, E. Filiot, S. N. Krishna and N. Lhote, Synthesis of computable regular functions of infinite words, In CONCUR, LIPIcs, Vol. 171 (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020), pp. 43:1–43:17. Google Scholar
16. J. Engelfriet and H. J. Hoogeboom, MSO definable string transductions and two-way finite-state transducers, ACM Transactions on Computational Logic (TOCL) 2(2) (2001) 216–254. Crossref, Google Scholar
17. E. Filiot, Logic-automata connections for transformations, In Logic and Its Applications - 6th Indian Conference, ICLA 2015, Mumbai, India, January 8-10, 2015. Proceedings, M. Banerjee and S. N. Krishna (eds.), Lecture Notes in Computer Science, Vol. 8923 (Springer, 2015), pp. 30–57. Google Scholar
18. E. Filiot, I. Jecker, C. Löding and S. Winter, On equivalence and uniformisation problems for finite transducers, In ICALP, LIPIcs, Vol. 55 (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016), pp. 125:1–125:14. Google Scholar
19. E. Filiot and S. Winter, Synthesizing computable functions from rational specifications over infinite words, In FSTTCS, LIPIcs, Vol. 213 (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021), pp. 43:1–43:16. Google Scholar
20. B. Finkbeiner and S. Schewe, Bounded synthesis, Int. J. Softw. Tools Technol. Transf. 15(5–6) (2013) 519–539. Crossref, Google Scholar
21. C. Gerstacker, F. Klein and B. Finkbeiner, Bounded synthesis of reactive programs, In Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7–10, 2018, Proceedings, S. K. Lahiri and C. Wang (eds.), Lecture Notes in Computer Science, Vol. 11138 (Springer, 2018), pp. 441–457. Google Scholar
22. E. Grädel, W. Thomas and T. Wilke, Automata, logics, and infinite games: A guide to current research, Lecture Notes in Computer Science, Vol. 6014 (Springer, 2002). Crossref, Google Scholar
23. M. Holtmann, Ł. Kaiser and W. Thomas, Degrees of lookahead in regular infinite games, In International Conference on Foundations of Software Science and Computational Structures, Lecture Notesin Computer Science, Vol. 2500 (Springer, 2010), pp. 252–266. Crossref, Google Scholar
24. J. E. Hopcroft and J. D. Ullman, An approach to a unified theory of automata, The Bell System Technical Journal 46(8) (1967) 1793–1829. Crossref, Google Scholar
25. F. A. Hosch and L. Landweber, Finite delay solutions for sequential conditions, Technical report, University of Wisconsin-Madison Department of Computer Sciences, 1972. Google Scholar
26. F. Klein and M. Zimmermann, How much lookahead is needed to win infinite games? Log. Methods Comput. Sci. 12(3) (2016). Web of Science, Google Scholar
27. K. Kobayashi, Classification of formal languages by functional binary transductions, Information and Control 15(1) (1969) 95–109. Crossref, Google Scholar
28. O. Kupferman, G. Perelli and M. Y. Vardi, Synthesis with rational environments, Ann. Math. Artif. Intell. 78(1) (2016) 3–20. Crossref, Web of Science, Google Scholar
29. A. Pnueli and R. Rosner, On the synthesis of a reactive module, In ACM Symposium on Principles of Programming Languages (POPL) (ACM, 1989), pp. 179–190. Crossref, Google Scholar
30. S. Safra, Exponential determinization for $ω$ -automata with strong-fairness acceptance condition, In Proceedings of the twenty-fourth annual ACM symposium on Theory of computing (1992), pp. 275–282. Crossref, Google Scholar
31. J. Sakarovitch, Elements of Automata Theory (Cambridge University Press, 2009). Crossref, Google Scholar
32. S. Schewe, Solving parity games in big steps, Comp. and Sys. Sci. 84 (2017) 243–262. Crossref, Web of Science, Google Scholar
33. K. Weihrauch, Computable Analysis: An Introduction (Springer Science & Business Media, 2012). Google Scholar