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.