Document Open Access Logo

Boolean Basis and Succinctness of Modal Logic via Hella-Vilander Games

Author Sebastian Pfau

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.35.pdf
  • Filesize: 0.79 MB
  • 22 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • succinctness
  • modal logic
  • model comparison games

Metrics

Abstract

The Hella-Vilander game for modal logic is a model comparison game that captures the formula size necessary to separate sets of pointed Kripke structures. We introduce the ℳ-ON game as a modification of this game. Our game captures the necessary number of modal operators, i.e., ◇ and □ instead of formula size. We use our game to show that the bi-implication ↔, sometimes also called equivalence, enables us to write modal logic formula with significantly fewer modal operators. With this we show, that with bi-implications we can also write significantly shorter modal logic formulas. This result holds even if only special classes of Kripke structures are considered. To be more precise we show that there is an exponential succinctness gap between modal logic and its extension with bi-implication on the class of structures with a transitive and reflexive accessibility relation, as well as on the class of structures with a symmetrical and reflexive accessibility relation. Lastly we show that for the class of structures with a transitive and symmetrical accessibility relation this succinctness gap disappears.

Cite As Get BibTex

Sebastian Pfau. Boolean Basis and Succinctness of Modal Logic via Hella-Vilander Games. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 35:1-35:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.35

Author Details

Sebastian Pfau
  • Technische Universität Ilmenau, Germany

References

  1. Micah Adler and Neil Immerman. An n! lower bound on formula size. ACM Transactions on Computational Logic, 4(3):296-314, 2003. URL: https://doi.org/10.1145/772062.772064.
  2. Christoph Berkholz, Dietrich Kuske, and Christian Schwarz. Boolean basis, formula size, and number of modal operators. Logical Methods in Computer Science, Volume 21, Issue 3, July 2025. URL: https://doi.org/10.46298/lmcs-21(3:10)2025.
  3. Marco Carmosino, Ronald Fagin, Neil Immerman, Phokion Kolaitis, Jonathan Lenchner, and Rik Sengupta. Multi-structural games and beyond. Logical Methods in Computer Scienc, 20:27:1-27:40, 2024. URL: https://doi.org/10.48550/arXiv.2301.13329.
  4. Andrzej Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae, 49:129-141, 1960. URL: https://eudml.org/doc/213582.
  5. Ronald Fagin, Jonathan Lenchner, Kenneth W. Regan, and Nikhil Vyas. Multi-structural games and number of quantifiers. Logical Methods in Computer Science, 21(1), 2025. URL: https://doi.org/10.46298/lmcs-21(1:10)2025.
  6. Roland Fraïssé. On some classifications of relationship systems. Publications scientifiques de l'Université d'Alger, Série A, Sciences mathématiques, 1954. Google Scholar
  7. Tim French, Wiebe van der Hoek, Petar Iliev, and Barteld Kooi. Succinctness of epistemic languages. In Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence (IJCAI-11), pages 881-886, 2011. URL: https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-153.
  8. Martin Grohe and Nicole Schweikardt. The succinctness of first-order logic on linear orders. Logical Methods in Computer Science, 1(1), 2005. URL: https://doi.org/10.2168/LMCS-1(1:6)2005.
  9. Lauri T. Hella and Miikka S. Vilander. Formula size games for modal logic and μ-calculus. Journal of Logic and Computation, 29(8):1311-1344, 2019. URL: https://doi.org/10.1093/logcom/exz025.
  10. Vaughan R. Pratt. The effect of basis on size of boolean expressions. In Proceedings - Annual IEEE Symposium on Foundations of Computer Science, FOCS, pages 119-121, October 1975. URL: https://doi.org/10.1109/SFCS.1975.29.
  11. Philip Spira. On time-hardware complexity tradeoffs for boolean functions. In Proceedings of the 4th Hawaii Symposium on System Sciences, 1971, pages 525-527, 1971. Google Scholar
  12. Wiebe van der Hoek, Petar Iliev, and Barteld Kooi. On the relative succinctness of two extensions by definitions of multimodal logic. Lecture Notes in Computer Science, 7318 LNCS:323-333, 2012. URL: https://doi.org/10.1007/978-3-642-30870-3_33.
  13. Hans van Ditmarsch, Jie Fan, Wiebe van der Hoek, and Petar Iliev. Some exponential lower bounds on formula-size in modal logic. In Advances in Modal Logic, volume 10, pages 139-157, August 2014. URL: https://www.scopus.com/inward/record.uri?eid=2-s2.0-84924671231&partnerID=40&md5=3f43caf649380733487e57e7338bd34d.
  14. Harry Vinall-Smeeth. From quantifier depth to quantifier number: Separating structures with k variables. In Proceedings - Symposium on Logic in Computer Science, 2024. URL: https://doi.org/10.1145/3661814.3662125.
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