The Complexity of One-Agent Refinement Modal Logic

We investigate the complexity of satisfiability for one-agent Refinement Modal Logic (

$\text{\sffamily RML}$

), a known extension of basic modal logic (

$\text{\sffamily ML}$

) obtained by adding refinement quantifiers on structures. It is known that

$\text{\sffamily RML}$

has the same expressiveness as

$\text{\sffamily ML}$

, but the translation of

$\text{\sffamily RML}$

into

$\text{\sffamily ML}$

is of non-elementary complexity, and

$\text{\sffamily RML}$

is at least

doubly

exponentially more succinct than

$\text{\sffamily ML}$

. In this paper, we show that

$\text{\sffamily RML}$

-satisfiability is ‘only’

singly

exponentially harder than

$\text{\sffamily ML}$

-satisfiability, the latter being a well-known

PSPACE

-complete problem. More precisely, we establish that

$\text{\sffamily RML}$

-satisfiability is complete for the complexity class

AEXP

$_{\text{\sffamily pol}}$

, 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

⊆

AEXP

$_{\text{\sffamily pol}}$

⊆

EXPSPACE

).