Reducing Transducer Equivalence to Register Automata Problems Solved by "Hilbert Method"

Authors Adrien Boiret, Radoslaw Piórkowski, Janusz Schmude

Thumbnail PDF


  • Filesize: 0.49 MB
  • 16 pages

Document Identifiers

Author Details

Adrien Boiret
  • University of Warsaw, Poland
Radoslaw Piórkowski
  • University of Warsaw, Poland
Janusz Schmude
  • University of Warsaw, Poland

Cite AsGet BibTex

Adrien Boiret, Radoslaw Piórkowski, and Janusz Schmude. Reducing Transducer Equivalence to Register Automata Problems Solved by "Hilbert Method". In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 48:1-48:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


In the past decades, classical results from algebra, including Hilbert's Basis Theorem, had various applications in formal languages, including a proof of the Ehrenfeucht Conjecture, decidability of HDT0L sequence equivalence, and decidability of the equivalence problem for functional tree-to-string transducers. In this paper, we study the scope of the algebraic methods mentioned above, particularily as applied to the functionality problem for register automata, and equivalence for functional register automata. We provide two results, one positive, one negative. The positive result is that functionality and equivalence are decidable for MSO transformations on unordered forests. The negative result comes from a try to extend this method to decide functionality and equivalence on macro tree transducers. We reduce macro tree transducers equivalence to an equivalence problem for some class of register automata naturally relevant to our method. We then prove this latter problem to be undecidable.

Subject Classification

ACM Subject Classification
  • Theory of computation → Transducers
  • formal language
  • Hilbert's basis theorem
  • transducers
  • register automata
  • equivalence problem
  • unordered trees
  • MSO transformations


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


  1. Michael H. Albert and J. Lawrence. A Proof of Ehrenfeucht’s Conjecture. Theor. Comput. Sci., 41:121-123, 1985. Google Scholar
  2. Rajeev Alur and Pavol Cerný. Expressiveness of streaming string transducers. In FSTTCS, volume 8 of LIPIcs, pages 1-12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010. Google Scholar
  3. Rajeev Alur and Loris D'Antoni. Streaming Tree Transducers. J. ACM, 64(5):31:1-31:55, 2017. URL:
  4. Rajeev Alur, Loris D'Antoni, Jyotirmoy V. Deshmukh, Mukund Raghothaman, and Yifei Yuan. Regular Functions and Cost Register Automata. In LICS, pages 13-22. IEEE Computer Society, 2013. Google Scholar
  5. Michael Benedikt, Timothy Duff, Aditya Sharad, and James Worrell. Polynomial automata: Zeroness and applications. In LICS, pages 1-12. IEEE Computer Society, 2017. Google Scholar
  6. Mikołaj Bojańczyk. Automata toolbox, May 2018. URL:
  7. Mikołaj Bojańczyk and Igor Walukiewicz. Forest algebras. In Logic and Automata, volume 2 of Texts in Logic and Games, pages 107-132. Amsterdam University Press, 2008. Google Scholar
  8. Christian Choffrut. Minimizing subsequential transducers: a survey. Theor. Comput. Sci., 292(1):131-143, 2003. Google Scholar
  9. Bruno Courcelle. Monadic Second-Order Definable Graph Transductions: A Survey. Theor. Comput. Sci., 126(1):53-75, 1994. Google Scholar
  10. Joost Engelfriet and Sebastian Maneth. Macro Tree Translations of Linear Size Increase are MSO Definable. SIAM J. Comput., 32(4):950-1006, 2003. Google Scholar
  11. Joost Engelfriet and Heiko Vogler. Macro Tree Transducers. J. Comput. Syst. Sci., 31(1):71-146, 1985. Google Scholar
  12. Juha Honkala. A short solution for the HDT0L sequence equivalence problem. Theor. Comput. Sci., 244(1-2):267-270, 2000. Google Scholar
  13. Karel Culik II and Juhani Karhumäki. The Equivalence of Finite Valued Transducers (On HDT0L Languages) is Decidable. Theor. Comput. Sci., 47(3):71-84, 1986. Google Scholar
  14. Sebastian Maneth. A Survey on Decidable Equivalence Problems for Tree Transducers. Int. J. Found. Comput. Sci., 26(8):1069-1100, 2015. URL:
  15. William C. Rounds. Mappings and Grammars on Trees. Mathematical Systems Theory, 4(3):257-287, 1970. Google Scholar
  16. Helmut Seidl, Sebastian Maneth, and Gregor Kemper. Equivalence of Deterministic Top-Down Tree-to-String Transducers is Decidable. In FOCS, pages 943-962. IEEE Computer Society, 2015. Google Scholar