Document Open Access Logo

Parikh One-Counter Automata

Authors Michaël Cadilhac , Arka Ghosh, Guillermo A. Pérez , Ritam Raha

Thumbnail PDF


  • Filesize: 0.78 MB
  • 15 pages

Document Identifiers

Author Details

Michaël Cadilhac
  • DePaul University, Chicago, IL, USA
Arka Ghosh
  • University of Warsaw, Poland
Guillermo A. Pérez
  • University of Antwerp - Flanders Make, Belgium
Ritam Raha
  • University of Antwerp - Flanders Make, Belgium
  • LaBRI, University of Bordeaux, France

Cite AsGet BibTex

Michaël Cadilhac, Arka Ghosh, Guillermo A. Pérez, and Ritam Raha. Parikh One-Counter Automata. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 30:1-30:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Counting abilities in finite automata are traditionally provided by two orthogonal extensions: adding a single counter that can be tested for zeroness at any point, or adding ℤ-valued counters that are tested for equality only at the end of runs. In this paper, finite automata extended with both types of counters are introduced. They are called Parikh One-Counter Automata (POCA): the "Parikh" part referring to the evaluation of counters at the end of runs, and the "One-Counter" part to the single counter that can be tested during runs. Their expressiveness, in the deterministic and nondeterministic variants, is investigated; it is shown in particular that there are deterministic POCA languages that cannot be expressed without nondeterminism in the original models. The natural decision problems are also studied; strikingly, most of them are no harder than in the original models. A parametric version of nonemptiness is also considered.

Subject Classification

ACM Subject Classification
  • Theory of computation → Grammars and context-free languages
  • Parikh automata
  • Context-free languages
  • One-counter automata


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


  1. Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In S. Rao Kosaraju, David S. Johnson, and Alok Aggarwal, editors, Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, May 16-18, 1993, San Diego, CA, USA, pages 592-601. ACM, 1993. URL:
  2. Stanislav Böhm, Stefan Göller, and Petr Jancar. Equivalence of deterministic one-counter automata is NL-complete. In Dan Boneh, Tim Roughgarden, and Joan Feigenbaum, editors, Symposium on Theory of Computing Conference, STOC'13, Palo Alto, CA, USA, June 1-4, 2013, pages 131-140. ACM, 2013. URL:
  3. Daniel Bundala and Joël Ouaknine. On parametric timed automata and one-counter machines. Inf. Comput., 253:272-303, 2017. URL:
  4. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Affine Parikh automata. RAIRO - Theoretical Informatics and Applications, 46(04):511-545, 2012. URL:
  5. Michaël Cadilhac, Andreas Krebs, and Pierre McKenzie. The algebraic theory of parikh automata. Theory of Computing Systems, 62(5):1241-1268, 2017. URL:
  6. Ehsan Chiniforooshan, Mark Daley, Oscar H. Ibarra, Lila Kari, and Shinnosuke Seki. One-reversal counter machines and multihead automata: Revisited. In Current Trends in Theory and Practice of Computer Science, volume 6543 of LNCS, pages 166-177. Springer, 2011. Google Scholar
  7. Diego Figueira and Leonid Libkin. Path logics for querying graphs: Combining expressiveness and efficiency. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 329-340. IEEE Computer Society, 2015. URL:
  8. Stefan Göller, Christoph Haase, Joël Ouaknine, and James Worrell. Model checking succinct and parametric one-counter automata. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 575-586. Springer, 2010. URL:
  9. Christoph Haase. Subclasses of presburger arithmetic and the weak EXP hierarchy. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 47:1-47:10. ACM, 2014. URL:
  10. Christoph Haase. A survival guide to Presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. URL:
  11. Christoph Haase, Stephan Kreutzer, Joël Ouaknine, and James Worrell. Reachability in succinct and parametric one-counter automata. In Mario Bravetti and Gianluigi Zavattaro, editors, CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009. Proceedings, volume 5710 of Lecture Notes in Computer Science, pages 369-383. Springer, 2009. URL:
  12. Matthew Hague and Anthony Widjaja Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 260-276. Springer, 2012. URL:
  13. John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979. Google Scholar
  14. Oscar H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, 25(1):116-133, 1978. URL:
  15. Petr Jancar and Jiří Šíma. The simplest non-regular deterministic context-free language. In Filippo Bonchi and Simon J. Puglisi, editors, 46th International Symposium on Mathematical Foundations of Computer Science, MFCS 2021, August 23-27, 2021, Tallinn, Estonia, volume 202 of LIPIcs, pages 63:1-63:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL:
  16. Felix Klaedtke and Harald Rueß. Monadic second-order logics with cardinalities. In International Colloquium on Automata, Languages and Programming, volume 2719 of LNCS, pages 681-696. Springer-Verlag, 2003. URL:
  17. Pascal Lafourcade, Denis Lugiez, and Ralf Treinen. Intruder deduction for AC-like equational theories with homomorphisms. In Jürgen Giesl, editor, Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings, volume 3467 of Lecture Notes in Computer Science, pages 308-322. Springer, 2005. URL:
  18. Michel Latteux and Grzegorz Rozenberg. Commutative one-counter languages are regular. J. Comput. Syst. Sci., 29(1):54-57, 1984. URL:
  19. Guillermo A. Pérez and Ritam Raha. Revisiting parameter synthesis for one-counter automata. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, Göttingen, Germany (Virtual Conference), volume 216 of LIPIcs, pages 33:1-33:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL:
  20. Yann-Joachim Ringard. Mustard watches: An integrated approach to time and food. Technical report, Équipe de Logique Mathématique, Paris 7, 1990. URL:
  21. Leslie G. Valiant and Michael S. Paterson. Deterministic one-counter automata. Journal of Computer and System Sciences, 10(3):340-350, 1975. URL:
  22. Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. On the complexity of equational horn clauses. In Robert Nieuwenhuis, editor, Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, volume 3632 of Lecture Notes in Computer Science, pages 337-352. Springer, 2005. URL:
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