Recent advances in Artificial Intelligence have enabled the development and deployment of autonomous agents and Multi-Agent Systems (MAS) in diverse applications. In particular there is an accelerating trend towards the specification of Unbounded Multi-Agent Systems (UMAS). From multi-party negotiation protocols and auctions to robotic swarms and scenarios in the internet of things, UMAS are MAS composed of an arbitrary number of homogeneous agents.
Crucially specifications pertaining to faulty behaviour may be exchibited only when some conditions on the number of agents are met. So for validation purposes it is not sufficient to verify that a system satisfies a given property of interest for a predetermined number of agents. Instead to provide full guarantees of correctness my research aims to ascertain that the property is satisfied for any number of agents in the system. Specifically my research is concerned with the development of parameterised model checking techniques to verify UMAS specified by agent-based logics.