Document Open Access Logo

Countdown μ-Calculus

Authors Jędrzej Kołodziejski , Bartek Klin

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2022.64.pdf
  • Filesize: 0.7 MB
  • 14 pages

Document Identifiers

Author Details

Jędrzej Kołodziejski
  • University of Warsaw, Poland
Bartek Klin
  • University of Oxford, UK

Funding

  • Kołodziejski, Jędrzej: National Science Center (NCN) grant 2021/41/B/ST6/00535

Acknowledgements

We are grateful to Mikołaj Bojańczyk for numerous helpful suggestions.

Cite AsGet BibTex

Jędrzej Kołodziejski and Bartek Klin. Countdown μ-Calculus. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 64:1-64:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.MFCS.2022.64

Abstract

We introduce the countdown μ-calculus, an extension of the modal μ-calculus with ordinal approximations of fixpoint operators. In addition to properties definable in the classical calculus, it can express (un)boundedness properties such as the existence of arbitrarily long sequences of specific actions. The standard correspondence with parity games and automata extends to suitably defined countdown games and automata. However, unlike in the classical setting, the scalar fragment is provably weaker than the full vectorial calculus and corresponds to automata satisfying a simple syntactic condition. We establish some facts, in particular decidability of the model checking problem and strictness of the hierarchy induced by the maximal allowed nesting of our new operators.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Automata over infinite objects
Keywords
  • countdown μ-calculus
  • games
  • automata

Metrics

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

Related Versions

References

  1. André Arnold and Damian Niwinski. Rudiments of calculus. Elsevier, 2001. Google Scholar
  2. Mikołaj Bojańczyk. Weak mso with the unbounding quantifier. Theory of Computing Systems, 48(3):554-576, 2011. URL: https://doi.org/10.1007/s00224-010-9279-2.
  3. Mikołaj Bojańczyk, Edon Kelmendi, Rafał Stefański, and Georg Zetzsche. Extensions of ω-regular languages. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '20, pages 266-272, 2020. URL: https://doi.org/10.1145/3373718.3394779.
  4. Mikolaj Bojanczyk, Pawel Parys, and Szymon Torunczyk. The MSO+U Theory of (N,<) Is Undecidable. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016), volume 47 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:8, 2016. URL: https://doi.org/10.4230/LIPIcs.STACS.2016.21.
  5. Mikołaj Bojanczyk and Szymon Torunczyk. Weak MSO+U over infinite trees. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012), volume 14 of Leibniz International Proceedings in Informatics (LIPIcs), pages 648-660, 2012. URL: https://doi.org/10.4230/LIPIcs.STACS.2012.648.
  6. Mikołaj Bojańczyk. A bounding quantifier. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, pages 41-55, September 2004. URL: https://doi.org/10.1007/978-3-540-30124-0_7.
  7. Mikołaj Bojańczyk and Thomas Colcombet. Bounds in w-regularity. In Proceedings - Symposium on Logic in Computer Science, pages 285-296, January 2006. URL: https://doi.org/10.1109/LICS.2006.17.
  8. Mikołaj Bojańczyk, Laure Daviaud, Bruno Guillon, Vincent Penelle, and A. V. Sreejith. Undecidability of mso+"ultimately periodic". ArXiv, abs/1807.08506, 2018. Google Scholar
  9. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasi-polynomial time. SIAM Journal on Computing, 0(0), 2017. URL: https://doi.org/10.1137/17M1145288.
  10. Thomas Colcombet. Regular Cost Functions, Part I: Logic and Algebra over Words. Logical Methods in Computer Science, Volume 9, Issue 3, 2013. URL: https://doi.org/10.2168/LMCS-9(3:3)2013.
  11. Lauri Hella, Antti Kuusisto, and Raine Rönnholm. Bounded game-theoretic semantics for modal mu-calculus. In GandALF, 2020. Google Scholar
  12. Szczepan Hummel and Michał Skrzypczak. The topological complexity of mso+u and related automata models. Fundamenta Informaticae, 119:87-111, 2012. Google Scholar
  13. David Janin and Igor Walukiewicz. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In Ugo Montanari and Vladimiro Sassone, editors, CONCUR '96: Concurrency Theory, pages 263-277, 1996. Google Scholar
  14. Dexter Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27(3):333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  15. Michał Skrzypczak. Descriptive Set Theoretic Methods in Automata Theory - Decidability and Topological Complexity, volume 9802 of Lecture Notes in Computer Science. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-52947-8.
  16. Yde Venema. Lectures on the modal μ-calculus, 2020. Google Scholar
  17. Igor Walukiewicz. Pushdown processes: Games and model-checking. Information and Computation, 164(2):234-263, 2001. URL: https://doi.org/10.1006/inco.2000.2894.
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