TY - GEN
T1 - Complexity of Polyadic Boolean Modal Logics
T2 - Annual Conference on Computer Science Logic
AU - Jaakkola, Reijo
N1 - Publisher Copyright:
© Reijo Jaakkola; licensed under Creative Commons License CC-BY 4.0.
PY - 2023/2/1
Y1 - 2023/2/1
N2 - 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.
AB - 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.
KW - Boolean modal logics
KW - Model checking
KW - Polyadic modal logics
KW - Satisfiability
U2 - 10.4230/LIPIcs.CSL.2023.26
DO - 10.4230/LIPIcs.CSL.2023.26
M3 - Conference contribution
AN - SCOPUS:85148331215
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 31st EACSL Annual Conference on Computer Science Logic, CSL 2023
A2 - Klin, Bartek
A2 - Pimentel, Elaine
Y2 - 13 February 2023 through 16 February 2023
ER -