The Complexity of One-Agent Refinement Modal Logic

International audienceWe investigate the complexity of satisfiability forone-agent refinement modal logic (RML), an extension of basic modal logic (ML) obtained by addingrefinement quantifiers on structures. RML is knownto have the same expressiveness as ML, but thetranslation of RML into ML is of non-elementarycomplexity, and RML is at least doubly exponentially more succinct than ML. In this paper weshow that RML-satisfiability is ‘only’ singly exponentially harder than ML-satisfiability, the latter being a well-known PSPACE-complete problem