Document Open Access Logo

Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability

Author Reijo Jaakkola

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.26.pdf
  • Filesize: 0.76 MB
  • 18 pages

Document Identifiers

Author Details

Reijo Jaakkola
  • Tampere University, Finland

Acknowledgements

I want to thank Antti Kuusisto for suggesting this topic to me and for discussing it with me on numerous occasions. I also want to thank the anonymous reviewers for their detailed comments which greatly improved the presentation of this paper.

Cite As Get BibTex

Reijo Jaakkola. Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CSL.2023.26

Abstract

We study the computational complexity of model checking and satisfiability problems of polyadic modal logics extended with permutations and Boolean operators on accessibility relations. First, we show that the combined complexity of the model checking problem for the resulting logic is PTime-complete. Secondly, we show that the satisfiability problem of polyadic modal logic extended with negation on accessibility relations is ExpTime-complete. Finally, we show that the satisfiability problem of polyadic modal logic with permutations and Boolean operators on accessibility relations is ExpTime-complete, under the assumption that both the number of accessibility relations that can be used and their arities are bounded by a constant. If NExpTime is not contained in ExpTime, then this assumption is necessary, since already the satisfiability problem of modal logic extended with Boolean operators on accessibility relations is NExpTime-hard.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • Polyadic modal logics
  • Boolean modal logics
  • Model checking
  • Satisfiability

Metrics

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

References

  1. Franz Baader, Ian Horrocks, Carsten Lutz, and Ulrike Sattler. An Introduction to Description Logic. Cambridge University Press, 2017. Google Scholar
  2. Bartosz Bednarczyk. Exploiting forwardness: Satisfiability and query-entailment in forward guarded fragment. In Logics in Artificial Intelligence, pages 179-193. Springer, 2021. Google Scholar
  3. Dietmar Berwanger and Erich Grädel. Games and model checking for guarded logics. In Proceedings of the Artificial Intelligence on Logic for Programming, pages 70-84. Springer-Verlag, 2001. Google Scholar
  4. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. URL: https://doi.org/10.1017/CBO9781107050884.
  5. Diego Calvanese, Giuseppe De Giacomo, and Maurizio Lenzerini. On the decidability of query containment under constraints. In Alberto O. Mendelzon and Jan Paredaens, editors, Proceedings of the Seventeenth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 149-158, 1998. URL: https://doi.org/10.1145/275487.275504.
  6. Maarten de Rijke. The modal logic of inequality. Journal of Symbolic Logic, 57(2):566-584, 1992. URL: https://doi.org/10.2307/2275293.
  7. G Gargov, S Passy, and T Tinchev. Modal environment for boolean speculations. In Mathematical logic and its applications, pages 253-263, 1987. Google Scholar
  8. Erich Grädel. On the restraining power of guards. J. Symb. Log., 64(4):1719-1742, 1999. URL: https://doi.org/10.2307/2586808.
  9. Erich Grädel. Why Are Modal Logics so Robustly Decidable?, pages 393-408. World Scientific Publishing Co., Inc., 2001. Google Scholar
  10. Erich Grädel. Finite model theory and descriptive complexity. In Finite Model Theory and Its Applications, pages 125-230. Springer, 2007. Google Scholar
  11. Erich Grädel, Phokion Kolaitis, and Moshe Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53-69, 1997. Google Scholar
  12. Lauri Hella and Antti Kuusisto. One-dimensional fragment of first-order logic. In Proceedings of Advances in Modal Logic, pages 274-293, 2014. Google Scholar
  13. Jonne Iso-Tuisku and Antti Kuusisto. Uniform one-dimensional fragment over ordered structures. arXiv, abs/1812.08732, 2018. URL: http://arxiv.org/abs/1812.08732.
  14. Jonne Iso-Tuisku and Antti Kuusisto. Description logics as polyadic modal logics. arXiv, abs/2108.08838, 2021. URL: http://arxiv.org/abs/2108.08838.
  15. Reijo Jaakkola. Ordered fragments of first-order logic. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS), pages 62:1-62:14, 2021. Google Scholar
  16. Reijo Jaakkola and Antti Kuusisto. Algebraic classifications for fragments of first-order logic and beyond. arXiv, abs/2005.01184, 2020. URL: http://arxiv.org/abs/2005.01184.
  17. Emanuel Kieronski. One-dimensional guarded fragments. In 44th International Symposium on Mathematical Foundations of Computer Science, MFCS, pages 16:1-16:14, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.16.
  18. Emanuel Kieronski and Antti Kuusisto. Complexity and expressivity of uniform one-dimensional fragment with equality. In 39nd International Symposium on Mathematical Foundations of Computer Science (MFCS), pages 365-376, 2014. Google Scholar
  19. Emanuel Kieronski and Antti Kuusisto. One-dimensional fragment over words and trees. Journal of Logic and Computation, February 2022. Google Scholar
  20. Antti Kuusisto. On the uniform one-dimensional fragment. In International Workshop on Description Logics (DL), 2016. Google Scholar
  21. Antti Kuusisto and Carsten Lutz. Weighted model counting beyond two-variable logic. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 619-628, 2018. Google Scholar
  22. Leonid Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-07003-1.
  23. Carsten Lutz and Ulrike Sattler. The complexity of reasoning with boolean modal logics. In Proceedings of Advances in Modal Logic, pages 329-348, 2000. Google Scholar
  24. Carsten Lutz and Ulrike Sattler. The complexity of reasoning with boolean modal logics. In Advances in Modal Logic, 2000. Google Scholar
  25. Carsten Lutz and Ulrike Sattler. Mary likes all cats. In Proceedings of the 2000 International Workshop on Description Logics (DL2000), pages 213-226, 2000. Google Scholar
  26. Carsten Lutz, Ulrike Sattler, and Stephan Tobies. A suggestion for an n-ary description logic. In Patrick Lambrix, Alexander Borgida, Maurizio Lenzerini, Ralf Möller, and Peter F. Patel-Schneider, editors, Proceedings of the 1999 International Workshop on Description Logics (DL'99), 1999. Google Scholar
  27. Carsten Lutz, Ulrike Sattler, and Frank Wolter. Modal logic and the two-variable fragment. In Proceedings of the 15th International Workshop on Computer Science Logic (CSL), pages 247-261, 2001. Google Scholar
  28. Maarten Marx and Yde Venema. Local variations on a loose theme: Modal logic and decidability. In Finite Model Theory and Its Applications, pages 371-429. Springer, 2007. Google Scholar
  29. James G. Schmolze. Terminological knowledge representation systems supporting n-ary terms. In Proceedings of the 1st International Conference on Principles of Knowledge Representation and Reasoning (KR'89), 1989. Google Scholar
  30. Moshe Y. Vardi. Why is modal logic so robustly decidable? In Descriptive Complexity and Finite Models, pages 149-183. American Mathematical Society, 1996. 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