The Complexity of One-Agent Refinement Modal Logic

摘要: We investigate the complexity of satisfiability for one-agent Refinement Modal Logic ($\text{\sffamily RML}$), a known extension basic modal logic ML}$) obtained by adding refinement quantifiers on structures. It is that $\text{\sffamily RML}$ has same expressiveness as ML}$, but translation into ML}$ non-elementary complexity, and at least doubly exponentially more succinct than ML}$. In this paper, we show RML}$-satisfiability 'only' singly harder ML}$-satisfiability, latter being well-known PSPACE-complete problem. More precisely, establish complete class AEXP$_{\text{\sffamily pol}}$, i.e., problems solvable alternating Turing machines running in single exponential time only with polynomial number alternations (note NEXPTIME⊆ pol}}$⊆ EXPSPACE).