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.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2014, 239, pp.37. 〈10.1016/j.ic.2014.07.013〉
Liste complète des métadonnées
Contributeur : Sophie Pinchinat <>
Soumis le : lundi 29 décembre 2014 - 09:21:09
Dernière modification le : jeudi 11 janvier 2018 - 06:25:24



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〉



Consultations de la notice