Verifying Multi-agent Systems via Unbounded Model Checking

   page       BibTeX_logo.png   
M. Kacprzak, A. Lomuscio, T. Lasica, W. Penczek, M. Szreter
Formal Approaches to Agent-Based Systems Third International Workshop, FAABS 2004, Greenbelt, MD, April 26-27, 2004, Revised Selected Papers
Lecture Notes in Computer Science 3228

We present an approach to the problem of verification of epistemic properties in multi-agent systems by means of symbolic model checking. In particular, it is shown how to extend the technique of unbounded model checking from a purely temporal setting to a temporal-epistemic one. In order to achieve this, we base our discussion on interpreted systems semantics, a popular semantics used in multi-agent systems literature. We give details of the technique and show how it can be applied to the well known train, gate and controller problem.

keywordsModel checking - unbounded model checking - multi-agent systems