Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability

TL;DR

This paper analyzes the computational complexity of model checking and satisfiability in polyadic Boolean modal logics with permutations and Boolean operators, establishing PTime and ExpTime completeness results.

Contribution

It provides the first detailed complexity classifications for model checking and satisfiability in these extended polyadic modal logics.

Findings

Model checking is PTime-complete.

Satisfiability with negation is ExpTime-complete.

Satisfiability with permutations and Boolean operators is ExpTime-complete under bounded relations.

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 necessary assumption that the number of accessibility relations that can be used is bounded by a constant.