Parameterised verification for multi-agent systems

We study the problem of verifying role-based multi-agent systems, where the number of components cannot be determined at design time. We give a semantics that captures parameterised, generic multi-agent systems and identify three notable classes that represent different ways in which the agents may interact among themselves and with the environment. While the verification problem is undecidable in general we put forward cutoff procedures for the classes identified. The methodology is based on the existence of a notion of simulation between the templates for the agents and the template for the environment in the system. We show that the cutoff identification procedures as well as the general algorithms that we propose are sound; for one class we show the decidability of the verification problem and present a complete cutoff procedure. We report experimental results obtained on MCMAS-P, a novel model checker implementing the parameterised model checking methodologies here devised.