This project is concerned with the verification of properties of multiagent systems. In particular the proposed methodology allows for the verification of a temporal language enriched by modalities for epistemic states, for strategies, and for correct behaviour defined for individual agents or for groups of agents. It extends existing obdd-based techniques for reactive systems by adding an epistemic, ATL, and a "deontic" dimension to the language to be checked, and by providing an input language that allows for the description of a system in terms of interpreted systems (in the spirit of Fagin et al "Reasoning about Knowledge", MIT95, and Lomuscio and Sergot "Deontic Interpreted Systems", Studia Logica - Special Issue on The Dynamics of Knowledge, W. van der Hoek and M. Wooldridge eds. Kluwer Academic Publishers. Volume 75.).

A prototype model checker has been developed, and it is available under the terms of the GPL license from:

Principal Investigator

Alessio Lomuscio


  • <link - external-link-new-window "Opens external link in new window">Alessio Lomuscio</link>
  • <link - external-link-new-window "Opens external link in new window">Franco Raimondi</link>


The studentship for this project has been partially granted by EPSRC grant CNA 04/04.

This page was last modified on 18 Oct 2013.