Closing a Gap in the Complexity of Refinement Modal Logic

TL;DR

This paper establishes the precise computational complexity of satisfiability and model checking in Refinement Modal Logic, showing PSPACE-completeness and providing a tableau system for the existential fragment.

Contribution

It introduces a tableau system to prove a tight PSPACE upper bound for RML satisfiability and characterizes the complexity for any fixed number of quantifier alternations.

Findings

PSPACE-complete model checking for RML with a single quantifier

Tight PSPACE upper bound for satisfiability of the existential fragment

Complexity characterization for fixed quantifier alternations in RML

Abstract

Refinement Modal Logic (RML), which was recently introduced by Bozzelli et al., is an extension of classical modal logic which allows one to reason about a changing model. In this paper we study computational complexity questions related to this logic, settling a number of open problems. Specifically, we study the complexity of satisfiability for the existential fragment of RML, a problem posed by Bozzelli, van Ditmarsch and Pinchinat. Our main result is a tight PSPACE upper bound for this problem, which we achieve by introducing a new tableau system. As a direct consequence, we obtain a tight characterization of the complexity of RML satisfiability for any fixed number of alternations of refinement quantifiers. Additionally, through a simple reduction we establish that the model checking problem for RML is PSPACE-complete, even for formulas with a single quantifier.