Advances in symbolic model checking for multi-agent systems
Title: Advances in symbolic model checking for multi-agent systems
Speaker: Alessio Lomuscio (Imperial College London, UK)
Time: 10:00, August 5th, 2013
Venue: Lecture Room, 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
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
intensional states, including their knowledge, intentions, their strategic abilities, etc.
In a previous talk at IOS I surveyed some of our work in this area, including serial and parallel algorithms for symbolic model checking
for temporal-epistemic logic and bounded-model checking procedures. In this talk I will summarise these results and present two further,
recent extensions. In the first I will explain how parameters representing sets of agents can automatically be synthesised, thereby
identifying epistemic properties of scenarios. In the second, I will describe how the usual limitations pertaining to the fixed number of
components of a system can be overcome by giving parameterised model checking procedures. In this context I will explain how MAS protocols
with unbounded number of agents can be, in some cases, efficiently verified.
The talk is based on material published at CAV09, AAMAS12 (best paper runner up paper) and IJCAI13.
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 autonomous underwater vehicles,
web-services and security protocols including e-voting.
He has published over 100 research papers in internationally leading conferences on the topics above. He is co-author of MCMAS, an
open-source, BDD-based model checker for multi-agent systems developed at the VAS research group at Imperial. In the past 15 years he has
served in a variety of roles at a number of international conferences on logic, artificial intelligence, and multi-agent systems. He is
Programme co-Chair for AAMAS 2014, the leading conference on multi-agent systems.