Document Open Access Logo

Remarks on Parikh-Recognizable Omega-languages

Authors Mario Grobler , Leif Sabellek , Sebastian Siebertz

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.31.pdf
  • Filesize: 0.76 MB
  • 21 pages

Document Identifiers

Author Details

Mario Grobler
  • University of Bremen, Germany
Leif Sabellek
  • University of Bremen, Germany
Sebastian Siebertz
  • University of Bremen, Germany

Acknowledgements

We thank Georg Zetzsche for his valuable remarks.

Cite AsGet BibTex

Mario Grobler, Leif Sabellek, and Sebastian Siebertz. Remarks on Parikh-Recognizable Omega-languages. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CSL.2024.31

Abstract

Several variants of Parikh automata on infinite words were recently introduced by Guha et al. [FSTTCS, 2022]. We show that one of these variants coincides with blind counter machine as introduced by Fernau and Stiebe [Fundamenta Informaticae, 2008]. Fernau and Stiebe showed that every ω-language recognized by a blind counter machine is of the form ⋃_iU_iV_i^ω for Parikh recognizable languages U_i, V_i, but blind counter machines fall short of characterizing this class of ω-languages. They posed as an open problem to find a suitable automata-based characterization. We introduce several additional variants of Parikh automata on infinite words that yield automata characterizations of classes of ω-language of the form ⋃_iU_iV_i^ω for all combinations of languages U_i, V_i being regular or Parikh-recognizable. When both U_i and V_i are regular, this coincides with Büchi’s classical theorem. We study the effect of ε-transitions in all variants of Parikh automata and show that almost all of them admit ε-elimination. Finally we study the classical decision problems with applications to model checking.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
Keywords
  • Parikh automata
  • blind counter machines
  • infinite words
  • Büchi’s theorem

Metrics

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

Related Versions

References

  1. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008. Google Scholar
  2. Brenda S. Baker and Ronald V. Book. Reversal-bounded multipushdown machines. Journal of Computer and System Sciences, 8(3):315-332, 1974. Google Scholar
  3. Pascal Baumann, Flavio D'Alessandro, Moses Ganardi, Oscar Ibarra, Ian McQuillan, Lia Schütze, and Georg Zetzsche. Unboundedness problems for machines with reversal-bounded counters. In Foundations of Software Science and Computation Structures, pages 240-264, Cham, 2023. Springer Nature Switzerland. Google Scholar
  4. J. Richard Büchi. Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly, 6(1‐6):66-92, 1960. Google Scholar
  5. Michaël Cadilhac. Automates à contraintes semilinéaires= Automata with a semilinear constraint. PhD thesis, University of Montréal, 2013. Google Scholar
  6. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. On the expressiveness of Parikh automata and related models. In Third Workshop on Non-Classical Models for Automata and Applications - NCMA 2011, volume 282 of books@ocg.at, pages 103-119. Austrian Computer Society, 2011. Google Scholar
  7. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Affine Parikh automata. RAIRO Theor. Informatics Appl., 46(4):511-545, 2012. Google Scholar
  8. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. Bounded Parikh automata. Int. J. Found. Comput. Sci., 23(8):1691-1710, 2012. Google Scholar
  9. Edmund M Clarke, Orna Grumberg, and Doron A. Peled. Model checking. The MIT Press, London, Cambridge, 1999. Google Scholar
  10. Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. Handbook of Model Checking. Springer Publishing Company, Incorporated, 1st edition, 2018. Google Scholar
  11. Luc Dartois, Emmanuel Filiot, and Jean-Marc Talbot. Two-way Parikh automata with a visibly pushdown stack. In Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, volume 11425 of Lecture Notes in Computer Science, pages 189-206. Springer, 2019. Google Scholar
  12. Enzo Erlich, Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. History-deterministic Parikh automata. arXiv preprint, 2022. URL: https://arxiv.org/abs/2209.07745.
  13. Henning Fernau and Ralf Stiebe. Sequential grammars and automata with valences. Theoretical Computer Science, 276(1):377-405, 2002. Google Scholar
  14. Henning Fernau and Ralf Stiebe. Blind counter automata on omega-words. Fundam. Inform., 83:51-64, 2008. Google Scholar
  15. Diego Figueira and Leonid Libkin. Path logics for querying graphs: Combining expressiveness and efficiency. In Proceedings of the 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), LICS ’15, pages 329-340. IEEE, 2015. Google Scholar
  16. 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, volume 150 of LIPIcs, pages 40:1-40:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  17. Dimitra Giannakopoulou and Flavio Lerda. From states to transitions: Improving translation of LTL formulae to Büchi automata. In Formal Techniques for (Networked and) Distributed Systems, 2002. Google Scholar
  18. Sheila A. Greibach. Remarks on blind and partially blind one-way multicounter machines. Theoretical Computer Science, 7(3):311-324, 1978. Google Scholar
  19. Mario Grobler, Leif Sabellek, and Sebastian Siebertz. Parikh automata on infinite words. arXiv preprint, 2023. URL: https://arxiv.org/abs/2301.08969.
  20. Mario Grobler, Leif Sabellek, and Sebastian Siebertz. Remarks on Parikh-recognizable omega-languages. arXiv preprint, 2023. URL: https://arxiv.org/abs/2307.07238.
  21. Mario Grobler and Sebastian Siebertz. Büchi-like characterizations for Parikh-recognizable omega-languages. arXiv preprint, 2023. URL: https://arxiv.org/abs/2302.04087.
  22. 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), volume 250 of Leibniz International Proceedings in Informatics (LIPIcs), pages 40:1-40:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  23. Hendrik Jan Hoogeboom. Context-free valence grammars - revisited. In Developments in Language Theory, pages 293-303, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. Google Scholar
  24. Oscar H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, 25(1):116-133, 1978. Google Scholar
  25. Wong Karianto. Parikh automata with pushdown stack. Diplomarbeit, RWTH Aachen, 2004. Google Scholar
  26. Felix Klaedtke and Harald Rueß. Monadic second-order logics with cardinalities. In Automata, Languages and Programming, pages 681-696, Berlin, Heidelberg, 2003. Springer. Google Scholar
  27. Michel Latteux. Cônes rationnels commutatifs. Journal of Computer and System Sciences, 18(3):307-333, 1979. Google Scholar
  28. Victor Mitrana and Ralf Stiebe. Extended finite automata over groups. Discrete Applied Mathematics, 108(3):287-300, 2001. Google Scholar
  29. Wolfgang Thomas. Automata on Infinite Objects, pages 133-191. MIT Press, Cambridge, MA, USA, 1991. Google Scholar
  30. Georg Zetzsche. Silent transitions in automata with storage. In Automata, Languages, and Programming, pages 434-445, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact