Skip to Main content Skip to Navigation
Journal articles

Refinement modal logic

Abstract : In this paper we present 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 ∀ in addition to the standard box modalities for each agent. The operator ∀ 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 ∀ 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 μ-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.
Document type :
Journal articles
Complete list of metadata
Contributor : Sophie Pinchinat <>
Submitted on : Monday, December 29, 2014 - 9:21:09 AM
Last modification on : Thursday, January 7, 2021 - 4:36:03 PM

Links full text



Laura Bozzelli, Hans P. Van Ditmarsch, Tim French, James Hales, Sophie Pinchinat. Refinement modal logic. Information and Computation, Elsevier, 2014, 239, pp.37. ⟨10.1016/j.ic.2014.07.013⟩. ⟨hal-01098737⟩



Record views