The complexity of one-agent refinement modal logic

We investigate the complexity of satisfiability for one-agent refinement modal logic (RML), a known extension of basic modal logic (ML) obtained by adding refinement quantifiers on structures. It is known that RML has the same expressiveness as ML, but the translation of RML into ML is of non-elementary complexity, and RML is at least doubly exponentially more succinct than ML. In this paper, we show that RML-satisfiability is ‘only’ singly exponentially harder than ML-satisfiability, the latter being a well-known PSPACE-complete problem. More precisely, we establish that RML-satisfiability is complete for the complexity class AEXPpolAEXPpol, i.e., the class of problems solvable by alternating Turing machines running in single exponential time but only with a polynomial number of alternations (note that NEXPTIME⊆AEXPpol⊆EXPSPACENEXPTIME⊆AEXPpol⊆EXPSPACE).1