Verification of multiagent systems via unbounded model checking.
Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems: AAMAS 2004: New York City, New York, USA: 19-23 July 2004.
(pp. 638 - 645).
ACM Press: New York, US.
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.
|Title:||Verification of multiagent systems via unbounded model checking|
|UCL classification:||UCL > School of BEAMS > Faculty of Engineering Science > Computer Science|
Archive Staff Only