Verification of Multiagent Systems via Unbounded Model Checking

We present an approach to the problem of verification of epistemic properties of 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.

• Type: Conference
• Year: 2004
• Where: ATAL
• Authors: Magdalena Kacprzak, Alessio Lomuscio, Wojciech Penczek
• Keywords: ATAL 2004, Intelligent Agents, Model Checking, Multi-agent Systems, Symbolic Model Checking