  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.
