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:
http://www.cs.ucl.ac.uk/staff/f.raimondi/MCMAS/

Alessio Lomuscio

• <link http://www.cs.ucl.ac.uk/staff/a.lomuscio - external-link-new-window "Opens external link in new window">Alessio Lomuscio</link>
• <link http://www.cs.ucl.ac.uk/staff/f.raimondi - 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.