Friday 20th May, 12:15, room 310

posted 16 May 2016, 07:08 by Jakub Michaliszyn   [ updated 16 May 2016, 07:15 ]
Panagiotis Kouvaros Imperial College London
Parameterised Verification for Multi-Agent Systems

In the past ten years several methods have been put forward for the
efficient model checking of multiagent systems  against agent-based
specifications.   Yet, since the number of states is exponential in the
number of agents in the system, the model checking problem remains
intractable for systems of many agents.
This is particularly problematic when wishing to reason about unbounded systems
where the number of components is not known at design time. Systems ranging
from robotic swarms to e-commerce applications constitute typical examples  in
which the number of participants is independent of the design process.

In this talk I will introduce a semantics that captures unbounded
multiagent systems. The semantics extends interpreted systems in a
parameterised setting where the number of agents is the parameter. I will
then present parameterised model checking techniques for the validation of
multiagent systems irrespective of the number of the agents present.
Finally, I will discuss MCMAS-P, a tool realising these techniques; MCMAS-P has
been applied to cache coherence protocols, mutual exclusion protocols,
swarm foraging and aggregation algorithms.