2026-08-11T03:07:09Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17487 2024-03-06T11:00:06Z ddc:004 open_access

Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability Jaakkola, Reijo Polyadic modal logics Boolean modal logics Model checking Satisfiability 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Reijo Jaakkola 2023 Is Part Of LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2023.26 urn:nbn:de:0030-drops-174875 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.26 eng https://creativecommons.org/licenses/by/4.0/legalcode