LIPIcs.FSTTCS.2022.40.pdf
- Filesize: 0.77 MB
- 20 pages
Document
Parikh Automata over Infinite Words
Authors
Shibashis Guha 
,
Ismaël Jecker ,
Karoliina Lehtinen ,
Martin Zimmermann
-
Part of:
Volume:
42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-12-14
File
Document Identifiers
Author Details
Acknowledgements
We want to thank an anonymous reviewer for proposing Lemma 14.
Cite As Get 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)
https://doi.org/10.4230/LIPIcs.FSTTCS.2022.40
Abstract
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
Keywords
- Parikh automata
- ω-automata
- Infinite Games
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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: https://doi.org/10.1016/S0304-3975(00)00399-6.
- 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: https://doi.org/10.4230/LIPIcs.ICALP.2020.114.
-
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 books@ocg.at, pages 103-119. Austrian Computer Society, 2011.
- Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Unambiguous constrained automata. Int. J. Found. Comput. Sci., 24(7):1099-1116, 2013. URL: https://doi.org/10.1142/S0129054113400339.
- Giusi Castiglione and Paolo Massazza. On a class of languages with holonomic generating functions. Theor. Comput. Sci., 658:74-84, 2017. URL: https://doi.org/10.1016/j.tcs.2016.07.022.
- 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: https://doi.org/10.4230/LIPIcs.ICALP.2017.117.
- 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: https://doi.org/10.1016/S0022-0000(77)80004-4.
- 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: https://doi.org/10.1007/978-3-030-17127-8_11.
- Jürgen Dassow and Victor Mitrana. Finite automata over free groups. Int. J. Algebra Comput., 10(6):725-738, 2000. URL: https://doi.org/10.1142/S0218196700000315.
-
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.
- Henning Fernau and Ralf Stiebe. Blind counter automata on omega-words. Fundam. Informaticae, 83(1-2):51-64, 2008. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi83-1-2-06.
- 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: https://doi.org/10.1109/LICS.2015.39.
- 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: https://doi.org/10.4230/LIPIcs.FSTTCS.2019.40.
- 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: https://doi.org/10.1142/S0129054120410038.
-
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.
- Seymour Ginsburg and Edwin H. Spanier. Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics, 16(2):285-296, 1966. URL: https://doi.org/pjm/1102994974.
- Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. Parikh automata over infinite words. arXiv, 2207.07694, 2022. URL: https://doi.org/10.48550/arXiv.2207.07694.
- Oscar H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, 25(1):116-133, 1978. URL: https://doi.org/10.1145/322047.322058.
- 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: https://doi.org/10.1007/3-540-45061-0_54.
-
Marvin L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967.
- Victor Mitrana and Ralf Stiebe. Extended finite automata over groups. Discret. Appl. Math., 108(3):287-300, 2001. URL: https://doi.org/10.1016/S0166-218X(00)00200-6.
- 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: https://doi.org/10.1016/S0049-237X(09)70564-6.
- Karianto Wong. Parikh automata with pushdown stack, 2004. Diploma thesis, RWTH Aachen University. URL: https://old.automata.rwth-aachen.de/download/papers/karianto/ka04.pdf.