Document Open Access Logo

Modal Separation of Fixpoint Formulae

Authors Jean Christoph Jung , Jędrzej Kołodziejski

PDF
Thumbnail PDF

File

LIPIcs.STACS.2025.55.pdf
  • Filesize: 0.87 MB
  • 20 pages

Document Identifiers

Author Details

Jean Christoph Jung
  • TU Dortmund University, Germany
Jędrzej Kołodziejski
  • TU Dortmund University, Germany

Cite As Get BibTex

Jean Christoph Jung and Jędrzej Kołodziejski. Modal Separation of Fixpoint Formulae. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 55:1-55:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.STACS.2025.55

Abstract

Modal separability for modal fixpoint formulae is the problem to decide for two given modal fixpoint formulae φ,φ' whether there is a modal formula ψ that separates them, in the sense that φ ⊧ ψ and ψ ⊧ ¬φ'. We study modal separability and its special case modal definability over various classes of models, such as arbitrary models, finite models, trees, and models of bounded outdegree. Our main results are that modal separability is PSpace-complete over words, that is, models of outdegree ≤ 1, ExpTime-complete over unrestricted and over binary models, and 2-ExpTime-complete over models of outdegree bounded by some d ≥ 3. Interestingly, this latter case behaves fundamentally different from the other cases also in that modal logic does not enjoy the Craig interpolation property over this class. Motivated by this we study also the induced interpolant existence problem as a special case of modal separability, and show that it is coNExpTime-complete and thus harder than validity in the logic. Besides deciding separability, we also investigate the problem of efficient construction of separators. Finally, we consider in a case study the extension of modal fixpoint formulae by graded modalities and investigate separability by modal formulae and graded modal formulae.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Modal Logic
  • Fixpoint Logic
  • Separability
  • Interpolation

Metrics

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

References

  1. Alessandro Artale, Jean Christoph Jung, Andrea Mazzullo, Ana Ozaki, and Frank Wolter. Living without Beth and Craig: Definitions and interpolants in description and modal logics with nominals and role inclusions. ACM Trans. Comput. Log., 24(4):34:1-34:51, 2023. URL: https://doi.org/10.1145/3597301.
  2. Franz Baader, Ian Horrocks, Carsten Lutz, and Ulrike Sattler. An Introduction to Description Logic. Cambridge University Press, 2017. URL: http://www.cambridge.org/de/academic/subjects/computer-science/knowledge-management-databases-and-data-mining/introduction-description-logic?format=PB#17zVGeWD2TZUeu6s.97.
  3. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  4. Fabio Bellissima. On the lattice of extensions of the modal logics KAlt_n. Arch. Math. Log., 27(2):107-114, 1988. URL: https://doi.org/10.1007/BF01620760.
  5. Michael Benedikt, Balder ten Cate, Thomas Colcombet, and Michael Vanden Boom. The complexity of boundedness for guarded logics. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS, pages 293-304. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/LICS.2015.36.
  6. Achim Blumensath, Martin Otto, and Mark Weyer. Decidability results for the boundedness problem. Log. Methods Comput. Sci., 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:2)2014.
  7. Mikołaj Bojańczyk and Wojciech Czerwiński. Automata Toolbox. University of Warsaw, 2018. URL: https://www.mimuw.edu.pl/~bojan/papers/toolbox.pdf.
  8. Ashok K. Chandra, Dexter Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. URL: https://doi.org/10.1145/322234.322243.
  9. Sang Cho and Dung T. Huynh. Finite-automaton aperiodicity is PSpace-complete. Theor. Comput. Sci., 88(1):99-116, 1991. URL: https://doi.org/10.1016/0304-3975(91)90075-D.
  10. Maarten de Rijke. A note on graded modal logic. Stud Logica, 64(2):271-283, 2000. URL: https://doi.org/10.1023/A:1005245900406.
  11. Kit Fine. In so many possible worlds. Notre Dame J. Formal Log., 13(4):516-520, 1972. URL: https://doi.org/10.1305/NDJFL/1093890715.
  12. Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci., 18(2):194-211, 1979. URL: https://doi.org/10.1016/0022-0000(79)90046-1.
  13. Tim French, Wiebe van der Hoek, Petar Iliev, and Barteld P. Kooi. On the succinctness of some modal logics. Artif. Intell., 197:56-85, 2013. URL: https://doi.org/10.1016/j.artint.2013.02.003.
  14. Martin Fürer. The computational complexity of the unconstrained limited domino problem (with implications for logical decision problems). In Logic and Machines: Decision Problems and Complexity, Proceedings of the Symposium "Rekursive Kombinatorik", volume 171 of Lecture Notes in Computer Science, pages 312-319. Springer, 1983. URL: https://doi.org/10.1007/3-540-13331-3_48.
  15. Dov M. Gabbay. Craig’s interpolation theorem for modal logics. In Conference in Mathematical Logic - London '70, pages 111-127, Berlin, Heidelberg, 1972. Springer Berlin Heidelberg. Google Scholar
  16. Gerd G. Hillebrand, Paris C. Kanellakis, Harry G. Mairson, and Moshe Y. Vardi. Undecidable boundedness problems for datalog programs. J. Log. Program., 25(2):163-190, 1995. URL: https://doi.org/10.1016/0743-1066(95)00051-K.
  17. Jean Christoph Jung and Jędrzej Kołodziejski. Modal separability of fixpoint formulae. In Proceedings of the 37th International Workshop on Description Logics (DL 2024), volume 3739 of CEUR Workshop Proceedings. CEUR-WS.org, 2024. URL: https://ceur-ws.org/Vol-3739/paper-5.pdf.
  18. Jean Christoph Jung and Frank Wolter. Living without Beth and Craig: Definitions and interpolants in the guarded and two-variable fragments. In Proceedings of Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470585.
  19. Eryk Kopczynski. Invisible pushdown languages. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 867-872. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933579.
  20. Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  21. Louwe Kuijer, Tony Tan, Frank Wolter, and Michael Zakharyaschev. Separating counting from non-counting in fragments of two-variable first-order logic (extended abstract). In Proc. of DL 2024, 2024. Google Scholar
  22. Karoliina Lehtinen and Sandra Quickert. Deciding the first levels of the modal mu alternation hierarchy by formula construction. In Proceedings of Annual Conference on Computer Science Logic CSL, volume 41 of LIPIcs, pages 457-471. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPICS.CSL.2015.457.
  23. Christof Löding and Christopher Spinrath. Decision problems for subclasses of rational relations over finite and infinite words. Discrete Mathematics & Theoretical Computer Science, Vol. 21 no. 3, January 2019. URL: https://doi.org/10.23638/DMTCS-21-3-4.
  24. Martin Otto. Eliminating recursion in the μ-calculus. In Proceedings of 16th Annual Symposium on Theoretical Aspects of Computer Science (STACS), volume 1563 of Lecture Notes in Computer Science, pages 531-540. Springer, 1999. URL: https://doi.org/10.1007/3-540-49116-3_50.
  25. Martin Otto. Graded modal logic and counting bisimulation. CoRR, abs/1910.00039, 2019. URL: https://arxiv.org/abs/1910.00039.
  26. Thomas Place and Marc Zeitoun. Separating regular languages with first-order logic. Log. Methods Comput. Sci., 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:5)2016.
  27. Vaughan R. Pratt. A decidable mu-calculus: Preliminary report. In Proceedings of 22nd Annual Symposium on Foundations of Computer Science (FOCS), pages 421-427. IEEE Computer Society, 1981. URL: https://doi.org/10.1109/SFCS.1981.4.
  28. Abraham Robinson. A result on consistency and its application to the theory of definition. Journal of Symbolic Logic, 25(2):174-174, 1960. URL: https://doi.org/10.2307/2964240.
  29. Marcel Paul Schützenberger. On finite monoids having only trivial subgroups. Inf. Control., 8(2):190-194, 1965. URL: https://doi.org/10.1016/S0019-9958(65)90108-7.
  30. A. Prasad Sistla and Edmund M. Clarke. The complexity of propositional linear temporal logics. J. ACM, 32(3):733-749, 1985. URL: https://doi.org/10.1145/3828.3837.
  31. Moshe Y. Vardi. Reasoning about the past with two-way automata. In Proceedings of International Colloquium Automata, Languages and Programming (ICALP), volume 1443 of Lecture Notes in Computer Science, pages 628-641. Springer, 1998. URL: https://doi.org/10.1007/BFB0055090.
  32. Yde Venema. Lectures on the modal μ-calculus, 2020. 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 About DROPS Imprint Privacy Contact