Title: Verification of multi-agent systems

Speaker: Dr Alessio Lomuscio (Imperial College London, United Kingdom)

ime: 10am, Monday 22 November

Venue: Lecture room, Lab for Computer Science, Level 3 Building #5, Institute of Software, CAS

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 other intensional 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-model checking 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.

Bio sketch:

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 programme committees for several international conferences and workshops. He is co-author of MCMAS, an open-source symbolic model checker for multi-agent systems.