PSPACE Reasoning for Graded Modal Logics

TL;DR

This paper introduces a PSPACE algorithm for deciding satisfiability in graded modal logic, matching the problem's known complexity and refuting previous conjectures of higher complexity.

Contribution

It presents the first optimal PSPACE algorithm for graded modal logic and extends results to more complex logics, setting a theoretical benchmark.

Findings

The algorithm operates within PSPACE, matching the lower bound.

It refutes the conjecture that the problem is ExpTime-hard.

Extends results to logics with inverse relations and intersection.

Abstract

We present a PSPACE algorithm that decides satisfiability of the graded modal logic Gr(K_R)---a natural extension of propositional modal logic K_R by counting expressions---which plays an important role in the area of knowledge representation. The algorithm employs a tableaux approach and is the first known algorithm which meets the lower bound for the complexity of the problem. Thus, we exactly fix the complexity of the problem and refute an ExpTime-hardness conjecture. We extend the results to the logic Gr(K_(R \cap I)), which augments Gr(K_R) with inverse relations and intersection of accessibility relations. This establishes a kind of ``theoretical benchmark'' that all algorithmic approaches can be measured against.