Parikh Automata over Infinite Words

Authors Shibashis Guha , Ismaël Jecker , Karoliina Lehtinen , Martin Zimmermann

Thumbnail PDF


  • Filesize: 0.77 MB
  • 20 pages

Document Identifiers

Author Details

Shibashis Guha
  • Tata Institute of Fundamental Research, Mumbai, India
Ismaël Jecker
  • University of Warsaw, Poland
Karoliina Lehtinen
  • CNRS, Aix-Marseille University, LIS, Marseille, France
Martin Zimmermann
  • Aalborg University, Denmark


We want to thank an anonymous reviewer for proposing Lemma 14.

Cite AsGet BibTex

Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. Parikh Automata over Infinite Words. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 40:1-40:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata. Here, we study the extension of the classical framework onto infinite inputs: We introduce reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words and study expressiveness, closure properties, and the complexity of verification problems. We show that almost all classes of automata have pairwise incomparable expressiveness, both in the deterministic and the nondeterministic case; a result that sharply contrasts with the well-known hierarchy in the ω-regular setting. Furthermore, emptiness is shown decidable for Parikh automata with reachability or Büchi acceptance, but undecidable for safety and co-Büchi acceptance. Most importantly, we show decidability of model checking with specifications given by deterministic Parikh automata with safety or co-Büchi acceptance, but also undecidability for all other types of automata. Finally, solving games is undecidable for all types.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Parikh automata
  • ω-automata
  • Infinite Games


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


  1. Vincent D. Blondel, Olivier Bournez, Pascal Koiran, Christos H. Papadimitriou, and John N. Tsitsiklis. Deciding stability and mortality of piecewise affine dynamical systems. Theor. Comput. Sci., 255(1-2):687-696, 2001. URL:
  2. Alin Bostan, Arnaud Carayol, Florent Koechlin, and Cyril Nicaud. Weakly-unambiguous Parikh automata and their link to holonomic series. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, ICALP 2020, volume 168 of LIPIcs, pages 114:1-114:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL:
  3. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. On the expressiveness of Parikh automata and related models. In Rudolf Freund, Markus Holzer, Carlo Mereghetti, Friedrich Otto, and Beatrice Palano, editors, NCMA 2011, volume 282 of, pages 103-119. Austrian Computer Society, 2011. Google Scholar
  4. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Unambiguous constrained automata. Int. J. Found. Comput. Sci., 24(7):1099-1116, 2013. URL:
  5. Giusi Castiglione and Paolo Massazza. On a class of languages with holonomic generating functions. Theor. Comput. Sci., 658:74-84, 2017. URL:
  6. Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Regular Separability of Parikh Automata. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, ICALP 2017, volume 80 of LIPIcs, pages 117:1-117:13. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2017. URL:
  7. Rina S. Cohen and Arie Y. Gold. Theory of omega-languages. I. Characterizations of omega-context-free languages. J. Comput. Syst. Sci., 15(2):169-184, 1977. URL:
  8. Luc Dartois, Emmanuel Filiot, and Jean-Marc Talbot. Two-way Parikh automata with a visibly pushdown stack. In Mikolaj Bojanczyk and Alex Simpson, editors, FOSSACS 2019, volume 11425 of LNCS, pages 189-206. Springer, 2019. URL:
  9. Jürgen Dassow and Victor Mitrana. Finite automata over free groups. Int. J. Algebra Comput., 10(6):725-738, 2000. URL:
  10. Leonard E. Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. Amer. Journal Math., 35(4):413-422, 1913. Google Scholar
  11. Henning Fernau and Ralf Stiebe. Blind counter automata on omega-words. Fundam. Informaticae, 83(1-2):51-64, 2008. URL:
  12. Diego Figueira and Leonid Libkin. Path logics for querying graphs: Combining expressiveness and efficiency. In LICS 2015, pages 329-340. IEEE Computer Society, 2015. URL:
  13. Emmanuel Filiot, Shibashis Guha, and Nicolas Mazzocchi. Two-way Parikh automata. In Arkadev Chattopadhyay and Paul Gastin, editors, FSTTCS 2019, volume 150 of LIPIcs, pages 40:1-40:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL:
  14. Emmanuel Filiot, Nicolas Mazzocchi, and Jean-François Raskin. A pattern logic for automata with outputs. Int. J. Found. Comput. Sci., 31(6):711-748, 2020. URL:
  15. David Gale and F. M. Stewart. Infinite games with perfect information. In Harold William Kuhn and Albert William Tucker, editors, Contributions to the Theory of Games (AM-28), Volume II, chapter 13, pages 245-266. Princeton University Press, 1953. Google Scholar
  16. Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics, 16(2):285-296, 1966. URL:
  17. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. Parikh automata over infinite words. arXiv, 2207.07694, 2022. URL:
  18. Oscar H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, 25(1):116-133, 1978. URL:
  19. Felix Klaedtke and Harald Rueß. Monadic second-order logics with cardinalities. In Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow, and Gerhard J. Woeginger, editors, ICALP 2003, volume 2719 of LNCS, pages 681-696. Springer, 2003. URL:
  20. Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967. Google Scholar
  21. Victor Mitrana and Ralf Stiebe. Extended finite automata over groups. Discret. Appl. Math., 108(3):287-300, 2001. URL:
  22. J. Richard Büchi. Symposium on decision problems: On a decision method in restricted second order arithmetic. In Ernest Nagel, Patrick Suppes, and Alfred Tarski, editors, Logic, Methodology and Philosophy of Science, volume 44 of Studies in Logic and the Foundations of Mathematics, pages 1-11. Elsevier, 1966. URL:
  23. Karianto Wong. Parikh automata with pushdown stack, 2004. Diploma thesis, RWTH Aachen University. URL: