Two-Way Parikh Automata

Authors Emmanuel Filiot, Shibashis Guha, Nicolas Mazzocchi

Thumbnail PDF


  • Filesize: 0.57 MB
  • 14 pages

Document Identifiers

Author Details

Emmanuel Filiot
  • Université libre de Bruxelles, Belgium
Shibashis Guha
  • Université libre de Bruxelles, Belgium
Nicolas Mazzocchi
  • Université libre de Bruxelles, Belgium

Cite AsGet BibTex

Emmanuel Filiot, Shibashis Guha, and Nicolas Mazzocchi. Two-Way Parikh Automata. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 40:1-40:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Parikh automata extend automata with counters whose values can only be tested at the end of the computation, with respect to membership into a semi-linear set. Parikh automata have found several applications, for instance in transducer theory, as they enjoy a decidable emptiness problem. In this paper, we study two-way Parikh automata. We show that emptiness becomes undecidable in the non-deterministic case. However, it is PSpace-C when the number of visits to any input position is bounded and the semi-linear set is given as an existential Presburger formula. We also give tight complexity bounds for the inclusion, equivalence and universality problems. Finally, we characterise precisely the complexity of those problems when the semi-linear constraint is given by an arbitrary Presburger formula.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Parikh automata
  • two-way automata
  • Presburger arithmetic


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


  1. Alfred V. Aho, John E. Hopcroft, and Jeffrey D. Ullman. A general theory of translation. Mathematical Systems Theory, 3(3):193-221, 1969. Google Scholar
  2. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. On the Expressiveness of Parikh Automata and Related Models. In NCMA'11 Proceedings, pages 103-119, 2011. Google Scholar
  3. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Unambiguous Constrained Automata. Int. J. Found. Comput. Sci., 24(7):1099-1116, 2013. Google Scholar
  4. Vincent Carnino and Sylvain Lombardy. On Determinism and Unambiguity of Weighted Two-Way Automata. IJFCS, 26(8):1127-1146, 2015. Google Scholar
  5. David C. Cooper. Theorem proving in arithmetic without multiplication. Machine Intelligence, 7(1):91-–99, 1972. Google Scholar
  6. Luc Dartois, Emmanuel Filiot, and Jean-Marc Talbot. Two-Way Parikh Automata with a Visibly Pushdown Stack. In FoSSaCS'19 Proceedings, pages 189-206, 2019. Google Scholar
  7. Luc Dartois, Paulin Fournier, Ismaël Jecker, and Nathan Lhote. On Reversible Transducers. In ICALP'18 Proceedings, pages 113:1-113:12, 2017. Google Scholar
  8. Rodrigo de Souza. Uniformisation of Two-Way Transducers. In LATA'13 Proceedings, pages 547-558, 2013. Google Scholar
  9. Diego Figueira and Leonid Libkin. Path Logics for Querying Graphs: Combining Expressiveness and Efficiency. In LICS'15 Proceedings, pages 329-340, 2015. Google Scholar
  10. Emmanuel Filiot, Nicolas Mazzocchi, and Jean-François Raskin. A Pattern Logic for Automata with Outputs. In DLT'18 Proceedings, pages 304-317, 2018. Google Scholar
  11. Viliam Geffert, Carlo Mereghetti, and Giovanni Pighizzini. Complementing two-way finite automata. Information and Computation, 205(8):1173-1187, 2007. Google Scholar
  12. Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics, 16(2):285-296, 1966. Google Scholar
  13. Christoph Haase. Subclasses of presburger arithmetic and the weak Exp hierarchy. In LICS'14 Proceedings, pages 47:1-47:10, 2014. Google Scholar
  14. Lane A. Hemachandra. The strong exponential hierarchy collapses. Journal of Computer and System Sciences, 39:299-322, 1987. Google Scholar
  15. John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979. Google Scholar
  16. Oscar H. Ibarra. Reversal-Bounded Multicounter Machines and Their Decision Problems. Journal ACM, 25(1):116-133, 1978. Google Scholar
  17. Wong Karianto. Parikh Automata with Pushdown Stack, 2004. Google Scholar
  18. Felix Klaedtke and Harald Rueß. Monadic Second-order Logics with Cardinalities. In ICALP'03 Proceedings, pages 681-696, 2003. Google Scholar
  19. Dexter Kozen. Lower bounds for natural proof systems. Foundations of Computer Science, pages 254-266, 1977. Google Scholar
  20. Anthony Widjaja Lin. Model checking infinite-state systems: generic and specific approaches. PhD thesis, University of Edinburg, 2010. Google Scholar
  21. Michal P. Chytil and Vojtech Jákl. Serial Composition of 2-Way Finite-State Transducers and Simple Programs on Strings. In ICALP'77 Proceedings, pages 135-147, 1977. Google Scholar
  22. Bruno Scarpellini. Complexity of subcases of presburger arithmetic. American Mathematical Society, 284(1):203-218, 1984. Google Scholar