Talk by Senior Researcher Hans van Ditmarsch, Department of Logic, University of Sevilla, Spain

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

Abstract: 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 additional 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. We also present an extension of the logic to the modal mu-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.

Host: Associate professor Thomas Bolander, Algorithms and Logic, DTU Informatics.

All are welcome!