Document Open Access Logo

Finite Convergence of μ-Calculus Fixpoints on Genuinely Infinite Structures

Authors Florian Bruse, Marco Sälzer, Martin Lange

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2021.24.pdf
  • Filesize: 0.67 MB
  • 19 pages

Document Identifiers

Author Details

Florian Bruse
  • School of Electrical Engineering and Computer Science, University of Kassel, Germany
Marco Sälzer
  • School of Electrical Engineering and Computer Science, University of Kassel, Germany
Martin Lange
  • School of Electrical Engineering and Computer Science, University of Kassel, Germany

Cite As Get BibTex

Florian Bruse, Marco Sälzer, and Martin Lange. Finite Convergence of μ-Calculus Fixpoints on Genuinely Infinite Structures. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.MFCS.2021.24

Abstract

The modal μ-calculus can only express bisimulation-invariant properties. It is a simple consequence of Kleene’s Fixpoint Theorem that on structures with finite bisimulation quotients, the fixpoint iteration of any formula converges after finitely many steps. We show that the converse does not hold: we construct a word with an infinite bisimulation quotient that is locally regular so that the iteration for any fixpoint formula of the modal μ-calculus on it converges after finitely many steps. This entails decidability of μ-calculus model-checking over this word. We also show that the reason for the discrepancy between infinite bisimulation quotients and trans-finite fixpoint convergence lies in the fact that the μ-calculus can only express regular properties.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Higher order logic
  • Theory of computation → Logic and verification
  • Theory of computation → Automata over infinite objects
Keywords
  • temporal logic
  • fixpoint iteration
  • bisimulation

Metrics

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

References

  1. B. Afshari and G. E. Leigh. On closure ordinals for the modal mu-calculus. In Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 30-44. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.30.
  2. J.-P. Allouche and J. O. Shallit. Automatic Sequences - Theory, Applications, Generalizations. Cambridge University Press, 2003. Google Scholar
  3. R. Axelsson, M. Lange, and R. Somla. The complexity of model checking higher-order fixpoint logic. Logical Methods in Computer Science, 3:1-33, 2007. URL: https://doi.org/10.2168/LMCS-3(2:7)2007.
  4. J. Barwise and Y. N. Moschovakis. Global inductive definability. J. Symb. Log., 43(3):521-534, 1978. URL: https://doi.org/10.2307/2273529.
  5. J. C. Bradfield. The modal μ-calculus alternation hierarchy is strict. In Proc. 7th Conf. on Concurrency Theory, CONCUR'96, volume 1119 of LNCS, pages 233-246. Springer, 1996. URL: https://doi.org/10.1007/3-540-61604-7_58.
  6. F. Bruse. Extremal Fixpoints for Higher-Order Modal Logic. PhD thesis, University of Kassel, Germany, 2020. URL: https://doi.org/doi:10.17170/kobra-202008091547.
  7. F. Bruse, O. Friedmann, and M. Lange. On guarded transformation in the modal μ-calculus. Log. J. IGPL, 23(2):194-216, 2015. URL: https://doi.org/10.1093/jigpal/jzu030.
  8. F. Bruse, M. Lange, and É. Lozes. Collapses of fixpoint alternation hierarchies in low type-levels of higher-order fixpoint logic. Proc. Workshop on Programming and Reasoning on Infinite Structures, PARIS'14, 2018. Google Scholar
  9. M. Czarnecki. How fast can the fixpoints in modal mu-calculus be reached? In 7th Workshop on Fixed Points in Computer Science, FICS 2010, Brno, Czech Republic, August 21-22, 2010, pages 35-39. Laboratoire d'Informatique Fondamentale de Marseille, 2010. URL: https://hal.archives-ouvertes.fr/hal-00512377/document#page=36.
  10. Mads Dam. Ctl* and ectl* as fragments of the modal mu-calculus. Theor. Comput. Sci., 126(1):77-96, 1994. URL: https://doi.org/10.1016/0304-3975(94)90269-0.
  11. S. Ghilardi, M. J. Gouveia, and L. Santocanale. Fixed-point elimination in the intuitionistic propositional calculus. ACM Trans. Comput. Log., 21(1):4:1-4:37, 2020. URL: https://doi.org/10.1145/3359669.
  12. M. J. Gouveia and L. Santocanale. ℵ_1 and the modal μ-calculus. Log. Methods Comput. Sci., 15(4), 2019. URL: https://doi.org/10.23638/LMCS-15(4:1)2019.
  13. D. Janin and I. Walukiewicz. On the expressive completeness of the propositional μ-calculus with respect to monadic second order logic. In Proc. 7th Conf. on Concurrency Theory, CONCUR'96, volume 1119 of LNCS, pages 263-277. Springer, 1996. URL: https://doi.org/10.1007/3-540-61604-7_60.
  14. J.Gutierrez, F.Klaedtke, and M. Lange. The μ-calculus alternation hierarchy collapses over structures with restricted connectivity. Theor. Comput. Sci., 560:292-306, 2014. URL: https://doi.org/10.1016/j.tcs.2014.03.027.
  15. R. Kaivola. Axiomatising linear time mu-calculus. In CONCUR '95: Concurrency Theory, 6th International Conference, Philadelphia, PA, USA, August 21-24, 1995, Proceedings, volume 962 of Lecture Notes in Computer Science, pages 423-437. Springer, 1995. URL: https://doi.org/10.1007/3-540-60218-6_32.
  16. S. C. Kleene. On a notation for ordinal numbers. Journal of Symbolic Logic, 3:150-155, 1938. Google Scholar
  17. D. Kozen. Results on the propositional μ-calculus. TCS, 27:333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  18. E. Lozes. A type-directed negation elimination. In Proceedings Tenth International Workshop on Fixed Points in Computer Science, FICS 2015, Berlin, Germany, September 11-12, 2015, volume 191 of EPTCS, pages 132-142, 2015. URL: https://doi.org/10.4204/EPTCS.191.12.
  19. G. C. Milanese and Y. Venema. Closure ordinals of the two-way modal μ-calculus. In Logic, Language, Information, and Computation - 26th International Workshop, WoLLIC 2019, Utrecht, The Netherlands, July 2-5, 2019, Proceedings, volume 11541 of Lecture Notes in Computer Science, pages 498-515. Springer, 2019. URL: https://doi.org/10.1007/978-3-662-59533-6_30.
  20. M. Otto. Eliminating recursion in the μ-calculus. In STACS 99, 16th Annual Symposium on Theoretical Aspects of Computer Science, Trier, Germany, March 4-6, 1999, Proceedings, volume 1563 of Lecture Notes in Computer Science, pages 531-540. Springer, 1999. URL: https://doi.org/10.1007/3-540-49116-3_50.
  21. R. S. Streett and E. A. Emerson. The propositional mu-calculus is elementary. In Automata, Languages and Programming, 11th Colloquium, Antwerp, Belgium, July 16-20, 1984, Proceedings, volume 172 of Lecture Notes in Computer Science, pages 465-472. Springer, 1984. URL: https://doi.org/10.1007/3-540-13345-3_43.
  22. M. Viswanathan and R. Viswanathan. A higher order modal fixed point logic. In Proc. 15th Int. Conf. on Concurrency Theory, CONCUR'04, volume 3170 of LNCS, pages 512-528. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-28644-8_33.
  23. T. Wilke. Alternating tree automata, parity games, and modal μ-calculus. Bull. Belgian Math. Soc., 8(2):359-391, 2001. URL: https://doi.org/10.36045/bbms/1102714178.
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 About DROPS Imprint Privacy Contact