Document Open Access Logo

Synthesizing Computable Functions from Rational Specifications over Infinite Words

Authors Emmanuel Filiot , Sarah Winter

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2021.43.pdf
  • Filesize: 0.78 MB
  • 16 pages

Document Identifiers

Author Details

Emmanuel Filiot
  • Université libre de Bruxelles, Brussels, Belgium
Sarah Winter
  • Université libre de Bruxelles, Brussels, Belgium

Funding

  • Filiot, Emmanuel: This work is partially supported by the MIS project F451019F (F.R.S.-FNRS). Emmanuel Filiot is a research associate at F.R.S.-FNRS.
  • Winter, Sarah: Sarah Winter is a postdoctoral researcher at F.R.S.-FNRS.

Acknowledgements

The authors want to thank Nathan Lhote for a discussion on two-way transducers and Martin Zimmermann for pointing out a reference.

Cite AsGet BibTex

Emmanuel Filiot and Sarah Winter. Synthesizing Computable Functions from Rational Specifications over Infinite Words. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 43:1-43:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSTTCS.2021.43

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Transducers
Keywords
  • uniformization
  • synthesis
  • transducers
  • continuity
  • computability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Shaull Almagor and Orna Kupferman. Good-enough synthesis. In International Conference on Computer Aided Verification, pages 541-563. Springer, 2020. Google Scholar
  2. Rajeev Alur, Rastislav Bodík, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo M. K. Martin, Mukund Raghothaman, Shambwaditya Saha, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Dependable Software Systems Engineering, pages 1-25. IEEE, 2015. Google Scholar
  3. Rajeev Alur, Emmanuel Filiot, and Ashutosh Trivedi. Regular transformations of infinite strings. In 2012 27th Annual IEEE Symposium on Logic in Computer Science, pages 65-74. IEEE, 2012. Google Scholar
  4. Roderick Bloem, Rüdiger Ehlers, and Robert Könighofer. Cooperative reactive synthesis. In Bernd Finkbeiner, Geguang Pu, and Lijun Zhang, editors, Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, Proceedings, volume 9364 of Lecture Notes in Computer Science, pages 394-410. Springer, 2015. Google Scholar
  5. Romain Brenguier, Jean-François Raskin, and Ocan Sankur. Assume-admissible synthesis. Acta Informatica, 54(1):41-83, 2017. URL: https://doi.org/10.1007/s00236-016-0273-2.
  6. J. Richard Büchi and Lawrence H. Landweber. Solving sequential conditions finite-state strategies. Trans. Ameri. Math. Soc., 138:295-311, 1969. Google Scholar
  7. Arnaud Carayol and Christof Löding. Uniformization in Automata Theory. In Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science Nancy, July 19-26, 2011, pages 153-178. London: College Publications, 2014. Google Scholar
  8. Krishnendu Chatterjee and Thomas A. Henzinger. Assume-guarantee synthesis. In Orna Grumberg and Michael Huth, editors, 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, volume 4424 of Lecture Notes in Computer Science, pages 261-275. Springer, 2007. Google Scholar
  9. Christian Choffrut and Serge Grigorieff. Uniformization of rational relations. In Jewels are Forever, pages 59-71. Springer, 1999. Google Scholar
  10. Edmund M Clarke, Thomas A Henzinger, Helmut Veith, and Roderick Bloem. Handbook of model checking, volume 10. Springer, 2018. Google Scholar
  11. Rodica Condurache, Emmanuel Filiot, Raffaella Gentilini, and Jean-François Raskin. The complexity of rational synthesis. In Ioannis Chatzigiannakis, Michael Mitzenmacher, Yuval Rabani, and Davide Sangiorgi, editors, 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs, pages 121:1-121:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  12. Vrunda Dave, Emmanuel Filiot, Shankara Narayanan Krishna, and Nathan Lhote. Synthesis of computable regular functions of infinite words. In CONCUR, volume 171 of LIPIcs, pages 43:1-43:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  13. Emmanuel Filiot, Ismaël Jecker, Christof Löding, and Sarah Winter. On equivalence and uniformisation problems for finite transducers. In ICALP, volume 55 of LIPIcs, pages 125:1-125:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  14. Bernd Finkbeiner and Sven Schewe. Bounded synthesis. Int. J. Softw. Tools Technol. Transf., 15(5-6):519-539, 2013. URL: https://doi.org/10.1007/s10009-012-0228-z.
  15. Carsten Gerstacker, Felix Klein, and Bernd Finkbeiner. Bounded synthesis of reactive programs. In Shuvendu K. Lahiri and Chao Wang, editors, Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, volume 11138 of Lecture Notes in Computer Science, pages 441-457. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-01090-4_26.
  16. Erich Gradel and Wolfgang Thomas. Automata, logics, and infinite games: a guide to current research, volume 2500. Springer Science & Business Media, 2002. Google Scholar
  17. Michael Holtmann, Łukasz Kaiser, and Wolfgang Thomas. Degrees of lookahead in regular infinite games. In International Conference on Foundations of Software Science and Computational Structures, pages 252-266. Springer, 2010. Google Scholar
  18. John E Hopcroft and Jeffrey D Ullman. An approach to a unified theory of automata. The Bell System Technical Journal, 46(8):1793-1829, 1967. Google Scholar
  19. F Hosch and Lawrence Landweber. Finite delay solutions for sequential conditions. Technical report, University of Wisconsin-Madison Department of Computer Sciences, 1972. Google Scholar
  20. Felix Klein and Martin Zimmermann. How much lookahead is needed to win infinite games? Log. Methods Comput. Sci., 12(3), 2016. URL: https://doi.org/10.2168/LMCS-12(3:4)2016.
  21. K. Kobayashi. Classification of formal languages by functional binary transductions. Information and Control, 15(1):95-109, July 1969. Google Scholar
  22. Orna Kupferman, Giuseppe Perelli, and Moshe Y. Vardi. Synthesis with rational environments. Ann. Math. Artif. Intell., 78(1):3-20, 2016. Google Scholar
  23. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In ACM Symposium on Principles of Programming Languages (POPL). ACM, 1989. Google Scholar
  24. Jacques Sakarovitch. Elements of automata theory. Cambridge University Press, 2009. Google Scholar
  25. Klaus Weihrauch. Computable analysis: an introduction. Springer Science & Business Media, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact