APICe » Publications » UnboundedVerification05

Verifying Multi-agent Systems via Unbounded Model Checking

M. Kacprzak, A. Lomuscio, T. Lasica, W. Penczek, M. Szreter
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.
Keywords: Model checking - unbounded model checking - multi-agent systems
Lecture Notes in Computer Science 3228, 2005, Springer
 Author = {Kacprzak, M. and Lomuscio, A. and Lasica, T. and Penczek, W. and Szreter, M.},
 Journal = {Lecture Notes in Computer Science},
 Title = {Verifying Multi-agent Systems via Unbounded Model Checking},
 Volume = {3228},
 Year = {2005},
 Publisher = {Springer},
 DOI = {10.1007/978-3-540-30960-4_13}