Skip to Main content Skip to Navigation
Conference papers

The Complexity of One-Agent Refinement Modal Logic

Laura Bozzelli 1 Hans Van Ditmarch 2 Sophie Pinchinat 3
3 S4 - System synthesis and supervision, scenarios
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : We 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).
Complete list of metadata
Contributor : Sophie Pinchinat <>
Submitted on : Monday, December 29, 2014 - 10:30:21 AM
Last modification on : Thursday, January 7, 2021 - 4:30:07 PM

Links full text



Laura Bozzelli, Hans Van Ditmarch, Sophie Pinchinat. The Complexity of One-Agent Refinement Modal Logic. JELIA 2012 - 13th European Conference on Logics in Artificial Intelligence, Sep 2012, Toulouse, France. pp.120-133, ⟨10.1007/978-3-642-33353-8_10⟩. ⟨hal-01098749⟩



Record views