Document Open Access Logo

Modal Logic Is More Succinct Iff Bi-Implication Is Available in Some Form

Authors Christoph Berkholz , Dietrich Kuske, Christian Schwarz

PDF
Thumbnail PDF

File

LIPIcs.STACS.2024.12.pdf
  • Filesize: 0.75 MB
  • 17 pages

Document Identifiers

Author Details

Christoph Berkholz
  • Technische Universität Ilmenau, Germany
Dietrich Kuske
  • Technische Universität Ilmenau, Germany
Christian Schwarz
  • Technische Universität Ilmenau, Germany

Funding

  • Berkholz, Christoph: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 414325841.

Cite AsGet BibTex

Christoph Berkholz, Dietrich Kuske, and Christian Schwarz. Modal Logic Is More Succinct Iff Bi-Implication Is Available in Some Form. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.STACS.2024.12

Abstract

Is it possible to write significantly smaller formulae, when using more Boolean operators in addition to the De Morgan basis (and, or, not)? For propositional logic a negative answer was given by Pratt: every formula with additional operators can be translated to the De Morgan basis with only polynomial increase in size. Surprisingly, for modal logic the picture is different: we show that adding bi-implication allows to write exponentially smaller formulae. Moreover, we provide a complete classification of finite sets of Boolean operators showing they are either of no help (allow polynomial translations to the De Morgan basis) or can express properties as succinct as modal logic with additional bi-implication. More precisely, these results are shown for the modal logic T (and therefore for K). We complement this result showing that the modal logic S5 behaves as propositional logic: no additional Boolean operators make it possible to write significantly smaller formulae.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • succinctness
  • modal logic

Metrics

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

References

  1. M. Adler and N. Immerman. An n! lower bound on formula size. ACM Trans. Comput. Log., 4(3):296-314, 2003. Google Scholar
  2. K. Etessami, M. Vardi, and T. Wilke. First-order logic with two variables and unary temporal logic. Inf. Comput., 179(2):279-295, 2002. Google Scholar
  3. T. French, W. van der Hoek, P. Iliev, and B.P. Kooi. On the succinctness of some modal logics. Artif. Intell., 197:56-85, 2013. Google Scholar
  4. S.B. Gashkov and I.S. Sergeev. О значении работ В. М. Храпченко. Прикладная дискретная математика, 2020(48):109-124, 2020. URL: https://doi.org/10.17223/20710410/48/10.
  5. M. Grohe and N. Schweikardt. The succinctness of first-order logic on linear orders. Log. Methods Comput. Sci., 1(1), 2005. Google Scholar
  6. L. Hella and M. Vilander. Formula size games for modal logic and μ-calculus. J. Log. Comput., 29(8):1311-1344, 2019. Google Scholar
  7. S. Jukna. Boolean Function Complexity - Advances and Frontiers, volume 27 of Algorithms and combinatorics. Springer, 2012. Google Scholar
  8. C Lutz. Complexity and succinctness of public announcement logic. In AAMAS'06, pages 137-143. ACM, 2006. Google Scholar
  9. C. Lutz, U. Sattler, and F. Wolter. Modal logic and the two-variable fragment. In CSL'01, Lecture Notes in Computer Science vol. 2142, pages 247-261. Springer, 2001. Google Scholar
  10. N. Markey. Temporal logic with past is exponentially more succinct. Bull. EATCS, 79:122-128, 2003. Google Scholar
  11. V.R. Pratt. The effect of basis on size of Boolean expressions. In 16th Annual Symposium on Foundations of Computer Science, pages 119-121, 1975. URL: https://doi.org/10.1109/SFCS.1975.29.
  12. J.E. Savage. The Complexity of Computing. Wiley, 1976. Google Scholar
  13. P.M. Spira. On time-hardware tradeoffs for Boolean functions. In Proc. of 4th Hawaii Intern. Symp. on System Sciences, pages 525-527, 1971. Google Scholar
  14. H. van Ditmarsch, Jie Fan, W. van der Hoek, and P. Iliev. Some exponential lower bounds on formula-size in modal logic. In Rajeev Goré, Barteld P. Kooi, and Agi Kurucz, editors, Advances in Modal Logic 2014, pages 139-157. College Publications, 2014. Google Scholar
  15. T. Wilke. Ctl^+ is exponentially more succinct than CTL. In FSTTCS'99, Lecture Notes in Computer Science vol. 1738, pages 110-121. Springer, 1999. Google Scholar
  16. S.V. Yablonskii and V.P. Kozyrev. Математические бопросы кибернетики. Информационные материалы, Академия наук СССР научный совет по комплексной проблеме "кибернетика", 19a:3-15, 1968. 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 Imprint Privacy Contact