PSPACE Bounds for Rank-1 Modal Logics

TL;DR

This paper establishes that all rank-1 modal logics have a PSPACE complexity bound by demonstrating a shallow model property, providing a unified framework for analyzing various modal logics.

Contribution

It introduces a coalgebraic semantics approach to prove PSPACE bounds for all rank-1 modal logics, unifying and extending prior results.

Findings

All rank-1 logics have a shallow model property.

The generic algorithm finds tableau proofs with subformula properties.

Unified PSPACE bounds for multiple modal logics like K, KD, and probabilistic logic.

Abstract

For lack of general algorithmic methods that apply to wide classes of logics, establishing a complexity bound for a given modal logic is often a laborious task. The present work is a step towards a general theory of the complexity of modal logics. Our main result is that all rank-1 logics enjoy a shallow model property and thus are, under mild assumptions on the format of their axiomatisation, in PSPACE. This leads to a unified derivation of tight PSPACE-bounds for a number of logics including K, KD, coalition logic, graded modal logic, majority logic, and probabilistic modal logic. Our generic algorithm moreover finds tableau proofs that witness pleasant proof-theoretic properties including a weak subformula property. This generality is made possible by a coalgebraic semantics, which conveniently abstracts from the details of a given model class and thus allows covering a broad range of logics in a uniform way.