Refinement modal logic

25^th October 2012, 16:00 Ashton Lecture Theatre
Prof. Hans van Ditmarsch
Dept. of Logic
University of Sevilla
Spain

Abstract

This is joint work with Laura Bozzelli, Tim French, James Hales, and Sophie Pinchinat.

In this talk I will 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 'forall' in addition to the standard modalities box for each agent. The operator 'forall' acts as a quantifier over the set of all refinements of a given model. We call it the refinement operator. As a variation on a bisimulation quantifier, it can be seen as a refinement quantifier over a variable not occurring in the formula bound by the operator. 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 multiagent refinement modal logic. There is an extension to the modal mu-calculus. It can be applied to dynamic epistemic logic: it is a form of quantifying over action models. There are results on the complexity of satisfiability, and on succinctness.