Symbolic model checking for multi-agent systems

Alessio Lomuscio

Multi-agent systems (MAS) are distributed autonomous systems in which the components, or agents, act autonomously or collectively in order to reach private or common goals. Logic-based specifications for MAS typically do not only involve their temporal evolution, but also other agent attitudes, including their knowledge, intentions, their strategic abilities, etc.

This talk will survey some of our work on model checking MAS against agent-based specifications. Serial and parallel algorithms for symbolic model checking against temporal-epistemic specifications as well as bounded-model checking procedures will be discussed. MCMAS, an open-source model checker, developed in the VAS group at Imperial College London, will be briefly demonstrated. A case study concerning the verification of diagnosability and fault-tolerance of an autonomous underwater vehicles will be discussed.

I will conclude by considering the case of open MAS where the number of agents is unbounded. In this context I will report recent results that enable us to establish a cut-off of a MAS, i.e., the maximal number of agents that need to be verified for conclusions to be drawn on any system of any number of components.