Document Open Access Logo

Aleph1 and the Modal mu-Calculus

Authors Maria João Gouveia, Luigi Santocanale

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2017.38.pdf
  • Filesize: 0.65 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • Modal mu-calculus
  • regular cardinal
  • continuous function
  • aleph1
  • omega1
  • closure ordinal
  • ordinal sum

Metrics

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

Abstract

For a regular cardinal kappa, a formula of the modal mu-calculus is kappa-continuous in a variable x if, on every model, its interpretation as a unary function of x is monotone and preserves unions of kappa-directed sets. We define the fragment C1 (x) of the modal mu-calculus and prove that all the formulas in this fragment are aleph_1-continuous. For each formula phi(x) of the modal mu-calculus, we construct a formula psi(x) in C1 (x) such that phi(x) is kappa-continuous, for some kappa, if and only if psi(x) is equivalent to phi(x). Consequently, we prove that (i) the problem whether a formula is kappa-continuous for some kappa is decidable, (ii) up to equivalence, there are only two fragments determined by continuity at some regular cardinal: the fragment C0(x) studied by Fontaine and the fragment C1 (x). We apply our considerations to the problem of characterizing closure ordinals of formulas of the modal mu-calculus. An ordinal alpha is the closure ordinal of a formula phi(x) if its interpretation on every model converges to its least fixed-point in at most alpha steps and if there is a model where the convergence occurs exactly in alpha steps. We prove that omega_1, the least uncountable ordinal, is such a closure ordinal. Moreover we prove that closure ordinals are closed under ordinal sum. Thus, any formal expression built from 0, 1, omega, omega_1 by using the binary operator symbol + gives rise to a closure ordinal.

Cite As Get BibTex

Maria João Gouveia and Luigi Santocanale. Aleph1 and the Modal mu-Calculus. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 38:1-38:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CSL.2017.38

Author Details

Maria João Gouveia
Luigi Santocanale

References

  1. J. Adamek and J. Rosicky. Locally Presentable and Accessible Categories:. Cambridge University Press, Cambridge, 1994. Google Scholar
  2. B. Afshari and G. E. Leigh. On closure ordinals for the modal mu-calculus. In Ronchi Della Rocca [23], pages 30-44. URL: http://www.dagstuhl.de/dagpub/978-3-939897-60-6, URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2013.30.
  3. L. Alberucci and A. Facchini. The Modal μ-Calculus Hierarchy on Restricted Classes of Transition Systems. The Journal of Symbolic Logic, 74(4):1367-1400, December 2009. URL: https://hal.archives-ouvertes.fr/hal-00396431.
  4. D. Berwanger, E. Grädel, and G. Lenzi. On the variable hierarchy of the modal μ-calculus. In J. Bradfield, editor, CSL 2002, Proceedings, pages 352-366, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/3-540-45793-3_24.
  5. M. Bojanczyk, C. Dittmann, and S. Kreutzer. Decomposition theorems and model-checking for the modal μ-calculus. In CSL-LICS'14, pages 17:1-17:10, New York, NY, USA, 2014. ACM. URL: http://dx.doi.org/10.1145/2603088.2603144.
  6. J. Bradfield and I. Walukiewicz. The mu-calculus and model-checking. In E. Clarke, T. Henzinger, and H. Veith, editors, Handbook of Model Checking. Springer-Verlag, 2015. Google Scholar
  7. J. C. Bradfield. The modal mu-calculus alternation hierarchy is strict. Theoretical Computer Science, 195(2):133-153, 1998. URL: http://dx.doi.org/10.1016/S0304-3975(97)00217-X.
  8. R. Cousot and P. Cousot. Constructive versions of Tarski’s fixed point theorems. Pacific Journal of Mathematics, 82(1):43-57, 1979. Google Scholar
  9. M. Czarnecki. How fast can the fixpoints in modal μ-calculus be reached? In L. Santocanale, editor, 7th Workshop on Fixed Points in Computer Science, FICS 2010, page 89, Brno, Czech Republic, August 2010. Available from Hal: URL: https://hal.archives-ouvertes.fr/hal-00512377.
  10. G. Fontaine. Continuous fragment of the mu-calculus. In M. Kaminski and S. Martini, editors, CSL 2008. Proceedings, volume 5213 of Lecture Notes in Computer Science, pages 139-153. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-87531-4_12.
  11. J. Fortier and L. Santocanale. Cuts for circular proofs: semantics and cut-elimination. In Ronchi Della Rocca [23], pages 248-262. URL: http://www.dagstuhl.de/dagpub/978-3-939897-60-6, URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2013.248.
  12. V. Vaccaro G. Sambin. A new proof of Sahlqvist’s theorem on modal definability and completeness. Journal of Symbolic Logic, 54:992-999, 1989. Google Scholar
  13. M. J. Gouveia and L. Santocanale. ℵ₁ and the modal μ-calculus. Preprint, available from Hal: https://hal.archives-ouvertes.fr/hal-01503091, March 2017.
  14. D. Janin and I. Walukiewicz. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In U. Montanari and V. Sassone, editors, CONCUR'96, Proceedings, pages 263-277, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/3-540-61604-7_60.
  15. M. Jurdziński. Deciding the winner in parity games is in UP ∩ co-UP. Information Processing Letters, 68(3):119-124, 1998. URL: http://dx.doi.org/10.1016/S0020-0190(98)00150-1.
  16. B. Jónsson. On the canonicity of sahlqvist identities. Studia Logica, 53(4):473-491, 1994. URL: http://www.jstor.org/stable/20015747.
  17. D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333-354, 1983. URL: http://dx.doi.org/10.1016/0304-3975(82)90125-6.
  18. M. Kracht and F. Wolter. Simulation and transfer results in modal logic - A survey. Studia Logica, 59(1):149-177, 1997. URL: http://dx.doi.org/10.1023/A:1004900300438.
  19. J.-L. Lassez, V. L. Nguyen, and L. Sonenberg. Fixed point theorems and semantics: A folk tale. Inf. Process. Lett., 14(3):112-116, 1982. URL: http://dx.doi.org/10.1016/0020-0190(82)90065-5.
  20. G. Lenzi. The modal μ-calculus: a survey. Task Quarterly, 9(3):29-316, 2005. Google Scholar
  21. D. Niwiński and I. Walukiewicz. Games for the μ-calculus. Theoretical Computer Science, 163(1):99-116, 1996. URL: http://dx.doi.org/10.1016/0304-3975(95)00136-0.
  22. J. Obdržálek. Fast mu-calculus model checking when tree-width is bounded. In W. A. Hunt and F. Somenzi, editors, CAV 2003, Proceedings, pages 80-92, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. URL: http://dx.doi.org/10.1007/978-3-540-45069-6_7.
  23. S. Ronchi Della Rocca, editor. Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. URL: http://www.dagstuhl.de/dagpub/978-3-939897-60-6.
  24. H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logic*. In S. Kanger, editor, Proceedings of the Third Scandinavian Logic Symposium, volume 82 of Studies in Logic and the Foundations of Mathematics, pages 110-143. Elsevier, 1975. URL: http://dx.doi.org/10.1016/S0049-237X(08)70728-6.
  25. L. Santocanale. μ-Bicomplete Categories and Parity Games. ITA, 36(2):195-227, 2002. Extended version appeared as LaBRI report RR-1281-02 is available from Hal: https://hal.archives-ouvertes.fr/hal-01376731. URL: http://dx.doi.org/10.1051/ita:2002010.
  26. L. Santocanale. Completions of μ-algebras. Ann. Pure Appl. Logic, 154(1):27-50, 2008. URL: http://dx.doi.org/10.1016/j.apal.2007.11.001.
  27. T. Studer. On the proof theory of the modal mu-calculus. Studia Logica, 89(3):343-363, 2008. Google Scholar
  28. A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955. Google Scholar
  29. S. K. Thomason. Independent propositional modal logics. Studia Logica, 39(2):143-144, 1980. URL: http://dx.doi.org/10.1007/BF00370317.
  30. I. Walukiewicz. Completeness of Kozen’s axiomatisation of the propositional μ-calculus. Information and Computation, 157(1):142-182, 2000. URL: http://dx.doi.org/10.1006/inco.1999.2836.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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