FO-Definable Transformations of Infinite Strings

Authors Vrunda Dave, Shankara Narayanan Krishna, Ashutosh Trivedi

Thumbnail PDF


  • Filesize: 0.58 MB
  • 14 pages

Document Identifiers

Author Details

Vrunda Dave
Shankara Narayanan Krishna
Ashutosh Trivedi

Cite AsGet BibTex

Vrunda Dave, Shankara Narayanan Krishna, and Ashutosh Trivedi. FO-Definable Transformations of Infinite Strings. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 12:1-12:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


The theory of regular and aperiodic transformations of finite strings has recently received a lot of interest. These classes can be equivalently defined using logic (Monadic second-order logic and first-order logic), two-way machines (regular two-way and aperiodic two-way transducers), and one-way register machines (regular streaming string and aperiodic streaming string transducers). These classes are known to be closed under operations such as sequential composition and regular (star-free) choice; and problems such as functional equivalence and type checking, are decidable for these classes. On the other hand, for infinite strings these results are only known for regular transformations: Alur, Filiot, and Trivedi studied transformations of infinite strings and introduced an extension of streaming string transducers over infinte strings and showed that they capture monadic second-order definable transformations for infinite strings. In this paper we extend their work to recover connection for infinite strings among first-order logic definable transformations, aperiodic two-way transducers, and aperiodic streaming string transducers.
  • Transducers
  • FO-definability
  • Infinite Strings


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


  1. R. Alur, A. Durand-Gasselin, and A. Trivedi. From monadic second-order definable string transformations to transducers. In LICS, pages 458-467, 2013. Google Scholar
  2. Rajeev Alur and Loris D'Antoni. Automata, Languages, and Programming: 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II, chapter Streaming Tree Transducers, pages 42-53. Springer Berlin Heidelberg, Berlin, Heidelberg, 2012. Google Scholar
  3. Rajeev Alur, Emmanuel Filiot, and Ashutosh Trivedi. Regular transformations of infinite strings. In Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer Science, LICS'12, pages 65-74, Washington, DC, USA, 2012. IEEE Computer Society. Google Scholar
  4. Rajeev Alur and P. Madhusudan. Adding nesting structure to words. J. ACM, 56(3):16:1-16:43, May 2009. Google Scholar
  5. Rajeev Alur and Pavol Černý. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11, pages 599-610. ACM, 2011. Google Scholar
  6. Rajeev Alur and Pavol Černý. Expressiveness of streaming string transducers. In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010), volume 8 of Leibniz International Proceedings in Informatics (LIPIcs), pages 1-12, Dagstuhl, Germany, 2010. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. URL:
  7. J. R. Büchi. Weak second-order arithmetic and finite automata. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 6(1-6):66-92, 1960. Google Scholar
  8. J. R. Büchi. On a decision method in restricted second-order arithmetic. In Int. Congr. for Logic Methodology and Philosophy of Science, pages 1-11. Standford University Press, Stanford, 1962. Google Scholar
  9. Olivier Carton and Luc Dartois. Aperiodic two-way transducers and fo-transductions. In 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, pages 160-174, 2015. Google Scholar
  10. B. Courcelle. Monadic second-order definable graph transductions: a survey. Theoretical Computer Science, 126(1):53-75, 1994. Google Scholar
  11. Vrunda Dave, Shankara Narayanan Krishna, and Ashutosh Trivedi. Fo-definable transformations of infinite strings. CoRR, abs/1607.04910, 2016. URL:
  12. V. Diekert and P. Gastin. First-order definable languages. In Logic and Automata: History and Perspectives, pages 261-306. Amsterdam University Press, 2008. Google Scholar
  13. J. Engelfriet and H. J. Hoogeboom. MSO definable string transductions and two-way finite-state transducers. ACM Trans. Comput. Logic, 2:216-254, 2001. Google Scholar
  14. Emmanuel Filiot. Logic and Its Applications: 6th Indian Conference, ICLA 2015, Mumbai, India, January 8-10, 2015. Proceedings, chapter Logic-Automata Connections for Transformations, pages 30-57. Springer Berlin Heidelberg, Berlin, Heidelberg, 2015. Google Scholar
  15. Emmanuel Filiot, Shankara Narayanan Krishna, and Ashutosh Trivedi. First-order definable string transformations. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, December 15-17, 2014, New Delhi, India, pages 147-159, 2014. Google Scholar
  16. Richard E. Ladner. Application of model theoretic games to discrete linear orders and finite automata. Information and Control, 33(4):281-303, 1977. Google Scholar
  17. R. McNaughton. Testing and generating infinite sequences by a finite automaton. Inform. Contr., 9:521-530, 1966. Google Scholar
  18. R. McNaughton and S. Papert. Counter-free automata. M.I.T. Research Monograph, 65, 1971. With an appendix by William Henneman. Google Scholar
  19. Dominique Perrin. Mathematical Foundations of Computer Science 1984: Proceedings, 11th Symposium Praha, Czechoslovakia September 3-7, 1984, chapter Recent results on automata and infinite words, pages 134-148. Springer Berlin Heidelberg, 1984. Google Scholar
  20. M. P. Schuetzenberger. On finite monoids having only trivial subgroups. Information and Control, 8(2):190-194, 1965. Google Scholar
  21. H. Straubing. Finite Automata, Formal Logic, and Circuit Complexity. Birkhäuser, Boston, 1994. Google Scholar
  22. Wolfgang Thomas. Star-free regular sets of ω-sequences. Information and Control, 42(2):148-156, 1979. Google Scholar
  23. Wolfgang Thomas. Languages, automata, and logic. In Handbook of Formal Languages, pages 389-455. Springer, 1996. Google Scholar
  24. Wolfgang Thomas. Ehrenfeucht games, the composition method, and the monadic theory of ordinal words. In Structures in Logic and Computer Science: A Selection of Essays in Honor of A. Ehrenfeucht, Lecture, pages 118-143. Springer-Verlag, 1997. Google Scholar