A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics

TL;DR

This paper analyzes the computational complexity of the satisfiability problem in graded modal logics, which extend propositional modal logic with cardinality constraints, over various classes of frames.

Contribution

It provides tight complexity bounds for satisfiability in graded modal logic across different frame classes, highlighting challenges like the absence of the tree-model property.

Findings

Complexity bounds are established for various frame classes.

Satisfiability is more complex than in ordinary modal logic, especially for transitive frames.

The problem remains challenging due to the lack of the tree-model property in some cases.

Abstract

Graded modal logic is the formal language obtained from ordinary (propositional) modal logic by endowing its modal operators with cardinality constraints. Under the familiar possible-worlds semantics, these augmented modal operators receive interpretations such as "It is true at no fewer than 15 accessible worlds that...", or "It is true at no more than 2 accessible worlds that...". We investigate the complexity of satisfiability for this language over some familiar classes of frames. This problem is more challenging than its ordinary modal logic counterpart--especially in the case of transitive frames, where graded modal logic lacks the tree-model property. We obtain tight complexity bounds for the problem of determining the satisfiability of a given graded modal logic formula over the classes of frames characterized by any combination of reflexivity, seriality, symmetry, transitivity and the Euclidean property.