The Complexity of One-Agent Refinement Modal Logic

International audienceWe investigate the complexity of satisfiability for one-agent Refinement Modal Logic ( \sffamily RML ), a known extension of basic modal logic ( \sffamily ML ) obtained by adding refinement quantifiers on structures. It is known that \sffamily RML has the same expressiveness as \sffamily ML , but the translation of \sffamily RML into \sffamily ML is of non-elementary complexity, and \sffamily RML is at least doubly exponentially more succinct than \sffamily ML . In this paper, we show that \sffamily RML -satisfiability is ‘only’ singly exponentially harder than \sffamily ML -satisfiability, the latter being a well-known PSPACE-complete problem. More precisely, we establish that \sffamily RML -satisfiability is complete for the complexity class AEXP \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 \sffamily pol ⊆ EXPSPACE)