Verification of multiagent systems via model checking by Alessio Lomuscio and Wojciech Penczek

Course description:

The course introduces model checking algorithms and tools for the verification of MAS. In particular, attention is given to ordered-binary decision diagrams and bounded-model checking algorithms for the verification of MAS specified by means of epistemic, deontic and temporal logic. Tools are presented and concrete examples discussed in detail.

Tutor bio:

Dr A Lomuscio is Senior Lecturer at UCL Adastral Park, UK. He has worked in the area of logic-based specifications and verification for MAS since 1995. In particular he is currently involved in the study of logics for MAS specifications (epistemic, doxastic, deontic and temporal modal logics) and of model checking algorithms and their implementation for the verification of MAS specified by means of such logics.
Further details at: www.cs.ucl.ac.uk/staff/A.Lomuscio/

Dr. Wojciech Penczek is the head of the Theory of Distributed Systems group at ICS-PAS. He was awarded a PhD in 1989 and habilitation in 1996 from ICS-PAS. He was a research fellow in the Department of Computer Science, Technical University of Eindhoven, 1989, 1993-1995, and Manchester University, 1990-1991. In 1996 he worked as a consultant at AT&T for two months. His research now is focused on verification methods for (timed) distributed and multi-agent systems. He is the author
of more than 80 conference and journal articles on temporal logic, verification methods, model checking, and formal theories of multi-agent systems.

Further details at: http://www.ipipan.waw.pl/~penczek