Model Checking Multiagent Systems

Fausto Giunchiglia
Istituto per la Ricerca Scientifica e Tecnologica (IRST)
Istituto Trentino di Cultura (ITC)
Trento, ITALY.
Dipartimento di Informatica e Studi Aziendali (DISA)
Universita` di Trento
Trento, ITALY.


Model checking is a very successful technique which has been applied in the design and verification of finite state concurrent reactive processes. In this talk I will show how this technique can be lifted to be applicable to multi-agent systems. Our approach allows us to reuse the technology and tools developed in model checking, to design and verify multi-agent systems in a modular and incremental way, and also to have a very efficient model checking algorithm.
Eyal Amir
Last modified: Tue May 5 13:04:40 PDT 1998