License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2023.26
URN: urn:nbn:de:0030-drops-174875
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17487/
Go to the corresponding LIPIcs Volume Portal

Jaakkola, Reijo

Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability

pdf-format:
LIPIcs-CSL-2023-26.pdf (0.8 MB)

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.

BibTeX - Entry

@InProceedings{jaakkola:LIPIcs.CSL.2023.26,
  author =	{Jaakkola, Reijo},
  title =	{{Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/17487},
  URN =		{urn:nbn:de:0030-drops-174875},
  doi =		{10.4230/LIPIcs.CSL.2023.26},
  annote =	{Keywords: Polyadic modal logics, Boolean modal logics, Model checking, Satisfiability}
}

Keywords: Polyadic modal logics, Boolean modal logics, Model checking, Satisfiability
Collection: 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)
Issue Date: 2023
Date of publication: 01.02.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI