Symbolic model checking for multi-agent systems
Alessio Lomuscio ( Imperial College, London )
- 14:00 2nd December 2014 ( week 8, Michaelmas Term 2014 )Lecture Theatre B
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.
Speaker bio
Alessio Lomuscio is Professor in logic for multi-agent systems in the Department of Computing, Imperial College London, where he leads the VAS (verification of autonomous systems) research group. He currently holds an EPSRC Leadership Fellowship. He received a PhD in Computer Science from the University of Birmingham in 1999 and a Laurea in Electronic Engineering from Politecnico di Milano in 1995. Before joining Imperial he was Lecturer at King's College London and Senior Lecturer at University College London. His research interests concern the specification and verification of multi-agent systems by means of techniques based on computational logic. In particular he has made theoretical contributions in the area of logic for multi-agent systems (including studying the completeness, decidability and complexity of several temporal-epistemic formalisms) and has put forward several symbolic model checking techniques for the verification of agent-based systems. he has applied these techniques to the verification of a range of applications including web-services, communication protocols, and security protocols.He has published over 120 research papers on the topics above. He sits on the editorial board of the Journal of Artificial Intelligence Research; in 2014 he served as Programme co-Chair for AAMAS 2014, the leading conference on multi-agent systems.
Share this:
