|
Magdalena Kacprzak Alessio Lomuscio
Wojciech Penczek
Unbounded Model Checking for
Knowledge and Time
966
Abstract
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 isshown 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 baseour discussion on interpreted systems semantics, a popular semantics used in multi-agent systems literature. We give details of the technique and show howit can be applied to the well known train, gate and controller problem.
Keywords : model checking, unbounded model checking, multi-agent systems.
|
|
 |
 |
