First-order Definable String Transformations

Authors Emmanuel Filiot, Shankara Narayanan Krishna, Ashutosh Trivedi

Thumbnail PDF


  • Filesize: 0.54 MB
  • 13 pages

Document Identifiers

Author Details

Emmanuel Filiot
Shankara Narayanan Krishna
Ashutosh Trivedi

Cite AsGet BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 147-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


The connection between languages defined by computational models and logic for languages is well-studied. Monadic second-order logic and finite automata are shown to closely correspond to each-other for the languages of strings, trees, and partial-orders. Similar connections are shown for first-order logic and finite automata with certain aperiodicity restriction. Courcelle in 1994 proposed a way to use logic to define functions over structures where the output structure is defined using logical formulas interpreted over the input structure. Engelfriet and Hoogeboom discovered the corresponding "automata connection" by showing that two-way generalised sequential machines capture the class of monadic-second order definable transformations. Alur and Cerny further refined the result by proposing a one-way deterministic transducer model with string variables - called the streaming string transducers - to capture the same class of transformations. In this paper we establish a transducer-logic correspondence for Courcelle's first-order definable string transformations. We propose a new notion of transition monoid for streaming string transducers that involves structural properties of both underlying input automata and variable dependencies. By putting an aperiodicity restriction on the transition monoids, we define a class of streaming string transducers that captures exactly the class of first-order definable transformations.
  • First-order logic
  • streaming string transducers


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


  1. R. Alur and P. Černý. Expressiveness of streaming string transducers. In Proc. FSTTCS 2010, pages 1-12, 2010. Google Scholar
  2. R. Alur and P. Černý. Streaming transducers for algorithmic verification of single-pass list-processing programs. In Proc. POPL 2011, pages 599-610, 2011. Google Scholar
  3. R. Alur and L. D'Antoni. Streaming tree transducers. In Proc. ICALP 2012, pages 42-53, 2012. Google Scholar
  4. R. Alur, L. D'Antoni, J. V. Deshmukh, M. Raghothaman, and Y. Yuan. Regular functions and cost register automata. In Proc. LICS 2013, pages 13-22, 2013. Google Scholar
  5. R. Alur, A. Durand-Gasselin, and A. Trivedi. From monadic second-order definable string transformations to transducers. In Proc. LICS 2013, pages 458-467, 2013. Google Scholar
  6. R. Alur, E. Filiot, and A. Trivedi. Regular transformations of infinite strings. In Proc. LICS 2012, pages 65-74, 2012. Google Scholar
  7. M. Bojanczyk. Transducers with origin information. In Proc. ICALP 2014, pages 26-37, 2014. Google Scholar
  8. 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
  9. O. Carton and L. Dartois. Aperiodic two-way transducers. In Highlights of Logic, Automata and Games, 2013. Slides available at URL:
  10. B. Courcelle. Monadic second-order definable graph transductions: a survey. Theoretical Computer Science, 126(1):53-75, 1994. Google Scholar
  11. 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
  12. 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
  13. J. Engelfriet and S. Maneth. Macro tree translations of linear size increase are MSO definable. SIAM Journal on Computing, 32:950-1006, 2003. Google Scholar
  14. E. Filiot, S. N. Krishna, and A. Trivedi. First-order definable string transformations. Google Scholar
  15. P. McKenzie, T. Schwentick, D. Therien, and H. Vollmer. The many faces of a translation. JCSS, 72, 2006. Google Scholar
  16. J. Stern. Complexity of some problems from the theory of automata. Information and Control, 66:163-176, 1985. Google Scholar
  17. H. Straubing. Finite Automata, Formal Logic, and Circuit Complexity. Birkhäuser, 1994. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail