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.
Originalsprog | Engelsk |
---|---|
Titel | 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022 |
Redaktører | Anuj Dawar, Venkatesan Guruswami |
Antal sider | 20 |
Forlag | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
Publikationsdato | 1 dec. 2022 |
Artikelnummer | 40 |
ISBN (Elektronisk) | 9783959772617 |
DOI | |
Status | Udgivet - 1 dec. 2022 |
Begivenhed | 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022 - Chennai, Indien Varighed: 18 dec. 2022 → 20 dec. 2022 |
Konference
Konference | 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022 |
---|---|
Land/Område | Indien |
By | Chennai |
Periode | 18/12/2022 → 20/12/2022 |
Navn | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|
Vol/bind | 250 |
ISSN | 1868-8969 |
Bibliografisk note
Publisher Copyright:© Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann; licensed under Creative Commons License CC-BY 4.0.