Seminars

Verification of multi-agent systems PDF slides
Alessio Lomuscio, Department of Computing, Imperial College, London, UK

11/12/2010, 2:00 PM, GHC-6501

Abstract

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 otherintentional states, including their knowledge, intentions, their strategic abilities, etc. This talk will survey recent work carried out on model checking MAS. Specifically, serial and parallel algorithms for symbolic model checking for temporal-epistemic logic as well as bounded-modelchecking procedures will be discussed. MCMAS, an open-source model checker, used at Imperial College, will be briefly demonstrated. Applications of the methodology to the automatic verification of security protocols, web services, and fault-tolerance will be surveyed.

Biography

Dr. Alessio Lomuscio is a Reader at the Department of Computing, Imperial College London, where he leads the group on verification of multi-agent systems. He currently holds an EPSRC Leadership Fellowship. He received a PhD in Computer Science from the University of Birmingham, UK, in 1999 and a Laurea in Electronic Engineering from Politecnico di Milano, Italy, 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. He has published about 100 research papers on the subject. He was invited speaker and invited guest lecturer in a number of international conferences and postgraduate courses and regularly sits on program committees for several international conferences and workshops. He is co-author of MCMAS, an open-source symbolic model checker for multi-agent systems.