Document Open Access Logo

Synthesis of Computable Regular Functions of Infinite Words

Authors Vrunda Dave, Emmanuel Filiot, Shankara Narayanan Krishna, Nathan Lhote

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.43.pdf
  • Filesize: 0.68 MB
  • 17 pages

Document Identifiers

Author Details

Vrunda Dave
  • IIT Bombay, India
Emmanuel Filiot
  • Université Libre de Bruxelles, Belgium
Shankara Narayanan Krishna
  • IIT Bombay, India
Nathan Lhote
  • MIMUW, University of Warsaw, Poland

Funding

  • Filiot, Emmanuel: This work is partially supported by the MIS project F451019F (F.R.S.-FNRS) and the EOS project Verifying Learning Artificial Intelligence Systems (F.R.S.-FNRS and FWO). Emmanuel Filiot is research associate at F.R.S.-FNRS.

Cite AsGet BibTex

Vrunda Dave, Emmanuel Filiot, Shankara Narayanan Krishna, and Nathan Lhote. Synthesis of Computable Regular Functions of Infinite Words. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 43:1-43:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.43

Abstract

Regular functions from infinite words to infinite words can be equivalently specified by MSO-transducers, streaming ω-string transducers as well as deterministic two-way transducers with look-ahead. In their one-way restriction, the latter transducers define the class of rational functions. Even though regular functions are robustly characterised by several finite-state devices, even the subclass of rational functions may contain functions which are not computable (by a Turing machine with infinite input). This paper proposes a decision procedure for the following synthesis problem: given a regular function f (equivalently specified by one of the aforementioned transducer model), is f computable and if it is, synthesize a Turing machine computing it. For regular functions, we show that computability is equivalent to continuity, and therefore the problem boils down to deciding continuity. We establish a generic characterisation of continuity for functions preserving regular languages under inverse image (such as regular functions). We exploit this characterisation to show the decidability of continuity (and hence computability) of rational and regular functions. For rational functions, we show that this can be done in NLogSpace (it was already known to be in PTime by Prieur). In a similar fashion, we also effectively characterise uniform continuity of regular functions, and relate it to the notion of uniform computability, which offers stronger efficiency guarantees.

Subject Classification

ACM Subject Classification
  • Theory of computation → Transducers
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Computability
Keywords
  • transducers
  • infinite words
  • computability
  • continuity
  • synthesis

Metrics

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

Related Versions

References

  1. Alonzo Church. Logic, arithmetic and automata. In Int. Congr. Math., pages 23-35, Stockholm, 1962. Google Scholar
  2. Rajeev Alur, Emmanuel Filiot, and Ashutosh Trivedi. Regular transformations of infinite strings. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 65-74. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/LICS.2012.18.
  3. Félix Baschenis, Olivier Gauwin, Anca Muscholl, and Gabriele Puppis. One-way definability of two-way word transducers. Log. Methods Comput. Sci., 14(4), 2018. URL: https://doi.org/10.23638/LMCS-14(4:22)2018.
  4. Mikolaj Bojanczyk. Polyregular functions. CoRR, abs/1810.08760, 2018. URL: http://arxiv.org/abs/1810.08760.
  5. Michaël Cadilhac, Olivier Carton, and Charles Paperman. Continuity and rational functions. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 115:1-115:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.115.
  6. Michaël Cadilhac, Andreas Krebs, Michael Ludwig, and Charles Paperman. A circuit complexity approach to transductions. In Giuseppe F. Italiano, Giovanni Pighizzini, and Donald Sannella, editors, Mathematical Foundations of Computer Science 2015 - 40th International Symposium, MFCS 2015, Milan, Italy, August 24-28, 2015, Proceedings, Part I, volume 9234 of Lecture Notes in Computer Science, pages 141-153. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48057-1_11.
  7. Olivier Carton, Dominique Perrin, and Jean-Eric Pin. Automata and semigroups recognizing infinite words. In Jörg Flum, Erich Grädel, and Thomas Wilke, editors, Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 of Texts in Logic and Games, pages 133-168. Amsterdam University Press, 2008. Google Scholar
  8. Swarat Chaudhuri, Sriram Sankaranarayanan, and Moshe Y. Vardi. Regular real analysis. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 509-518. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.57.
  9. Christian Choffrut. Minimizing subsequential transducers: a survey. Theor. Comput. Sci., 292(1):131-143, 2003. URL: https://doi.org/10.1016/S0304-3975(01)00219-5.
  10. Vrunda Dave, Emmanuel Filiot, Shankara Narayanan Krishna, and Nathan Lhote. Deciding the computability of regular functions over infinite words. CoRR, abs/1906.04199, 2019. URL: http://arxiv.org/abs/1906.04199.
  11. Joost Engelfriet, Hendrik Jan Hoogeboom, and Bart Samwel. XML navigation and transformation by tree-walking automata and transducers with visible and invisible pebbles. CoRR, abs/1809.05730, 2018. URL: http://arxiv.org/abs/1809.05730.
  12. Léo Exibard, Emmanuel Filiot, and Pierre-Alain Reynier. On computability of data word functions defined by transducers. In Jean Goubault-Larrecq and Barbara König, editors, Foundations of Software Science and Computation Structures - 23rd International Conference, FOSSACS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, volume 12077 of Lecture Notes in Computer Science, pages 217-236. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_12.
  13. Emmanuel Filiot. Logic-automata connections for transformations. In Mohua Banerjee and Shankara Narayanan Krishna, editors, Logic and Its Applications - 6th Indian Conference, ICLA 2015, Mumbai, India, January 8-10, 2015. Proceedings, volume 8923 of Lecture Notes in Computer Science, pages 30-57. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-45824-2_3.
  14. Emmanuel Filiot, Shibashis Guha, and Nicolas Mazzocchi. Two-way parikh automata. In Arkadev Chattopadhyay and Paul Gastin, editors, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, December 11-13, 2019, Bombay, India, volume 150 of LIPIcs, pages 40:1-40:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2019.40.
  15. Emmanuel Filiot, Nicolas Mazzocchi, and Jean-François Raskin. A pattern logic for automata with outputs. In Mizuho Hoshi and Shinnosuke Seki, editors, Developments in Language Theory - 22nd International Conference, DLT 2018, Tokyo, Japan, September 10-14, 2018, Proceedings, volume 11088 of Lecture Notes in Computer Science, pages 304-317. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98654-8_25.
  16. Michael Holtmann, Lukasz Kaiser, and Wolfgang Thomas. Degrees of lookahead in regular infinite games. Log. Methods Comput. Sci., 8(3), 2012. URL: https://doi.org/10.2168/LMCS-8(3:24)2012.
  17. Oscar H. Ibarra. Automata with reversal-bounded counters: A survey. In Helmut Jürgensen, Juhani Karhumäki, and Alexander Okhotin, editors, Descriptional Complexity of Formal Systems - 16th International Workshop, DCFS 2014, Turku, Finland, August 5-8, 2014. Proceedings, volume 8614 of Lecture Notes in Computer Science, pages 5-22. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09704-6_2.
  18. J.R. Büchi and L.H. Landweber. Solving sequential conditions finite-state strategies. Trans. Ameri. Math. Soc., 138:295-311, 1969. Google Scholar
  19. S. Rao Kosaraju. Regularity preserving functions. SIGACT News, 6(2):16–17, April 1974. URL: https://doi.org/10.1145/1008304.1008306.
  20. Jean-Éric Pin and Pedro V. Silva. On uniformly continuous functions for some profinite topologies. Theor. Comput. Sci., 658:246-262, 2017. URL: https://doi.org/10.1016/j.tcs.2016.06.013.
  21. Christophe Prieur. How to decide continuity of rational functions on infinite words. Theor. Comput. Sci., 276(1-2):445-447, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00307-3.
  22. W. Rudin. Principles of Mathematical Analysis. International series in pure and applied mathematics. McGraw-Hill, 1976. URL: https://books.google.pl/books?id=kwqzPAAACAAJ.
  23. Joel I. Seiferas and Robert McNaughton. Regularity-preserving relations. Theor. Comput. Sci., 2(2):147-154, 1976. URL: https://doi.org/10.1016/0304-3975(76)90030-X.
  24. Richard Edwin Stearns and Juris Hartmanis. Regularity preserving modifications of regular expressions. Inf. Control., 6(1):55-69, 1963. URL: https://doi.org/10.1016/S0019-9958(63)90110-4.
  25. Klaus Weihrauch. Computable Analysis - An Introduction. Texts in Theoretical Computer Science. An EATCS Series. Springer, 1st edition, 2000. URL: https://doi.org/10.1007/978-3-642-56999-9.
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