Refinement modal logic - Université de Rennes Accéder directement au contenu
Article Dans Une Revue Information and Computation Année : 2014

Refinement modal logic

Résumé

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.

Dates et versions

hal-01098737 , version 1 (29-12-2014)

Identifiants

Citer

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

Altmetric

Partager

Gmail Facebook X LinkedIn More