Minor changes are by default collapsed in the page history.
No changes
The page does not exist yet.
Failed to load changes
Version by on
Leave Collaboration
Are you sure you want to leave the realtime collaboration and continue editing alone? The changes you save while editing alone will lead to merge conflicts with the changes auto-saved by the realtime editing session.
Verifying Multi-agent Systems via Unbounded Model Checking
M. Kacprzak, A. Lomuscio, T. Lasica, W. Penczek, M. Szreter
Formal Approaches to Agent-Based Systems 3rd International Workshop, FAABS 2004, Greenbelt, MD, April 26-27, 2004, Revised Selected Papers
Lecture Notes in Computer Science 3228
Springer
2005
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
