2013/09/20 by Antonis Achilleos, Michael Lampis, Achilleos, Antonis +1 · 1 citation
Computer Science · #Advanced Algebra and Logic #Logic, Reasoning, and Knowledge #Semantic Web and Ontologies #cs.CC #cs.LO
paper · pdf · doi:10.48550/arxiv.1309.5184
arxiv created 2013/09/20 · arxiv updated 2013/09/23
Refinement Modal Logic (RML), which was recently introduced by Bozzelli et al., is an extension of classical modal logic which allows one to reason about a changing model. In this paper we study computational complexity questions related to this logic, settling a number of open problems. Specifically, we study the complexity of satisfiability for the existential fragment of RML, a problem posed by Bozzelli, van Ditmarsch and Pinchinat. Our main result is a tight PSPACE upper bound for this problem, which we achieve by introducing a new tableau system. As a direct consequence, we obtain a tight characterization of the complexity of RML satisfiability for any fixed number of alternations of refinement quantifiers. Additionally, through a simple reduction we establish that the model checking problem for RML is PSPACE-complete, even for formulas with a single quantifier.