Refinement Modal Logic
This work addresses the need for more expressive modal logics in formal verification and epistemic reasoning, though it appears to be an incremental extension of existing bisimulation-based approaches.
The paper introduces refinement modal logic, which extends standard modal logic with a refinement quantifier operator that quantifies over all refinements of a given model, and provides a sound and complete axiomatization for it. It also extends this logic to the modal mu-calculus, analyzes its complexity and succinctness, and discusses applications in software verification and dynamic epistemic logic.
In this paper we present {\em refinement modal logic}. A refinement is like a bisimulation, except that from the three relational requirements only `atoms' and `back' need to be satisfied. Our logic contains a new operator 'all' in addition to the standard modalities 'box' for each agent. The operator 'all' acts as a quantifier over the set of all refinements of a given model. As a variation on a bisimulation quantifier, this refinement operator or refinement quantifier 'all' can be seen as quantifying over a variable not occurring in the formula bound by it. The logic combines the simplicity of multi-agent modal logic with some powers of monadic second-order quantification. We present a sound and complete axiomatization of multi-agent refinement modal logic. We also present an extension of the logic to the modal mu-calculus, and an axiomatization for the single-agent version of this logic. Examples and applications are also discussed: to software verification and design (the set of agents can also be seen as a set of actions), and to dynamic epistemic logic. We further give detailed results on the complexity of satisfiability, and on succinctness.