HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Monday, December 29, 2014 - 9:21:09 AM
Last modification on : Friday, February 4, 2022 - 3:25:34 AM

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