Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking

Issue title: Concurrency Specification and Programming (CS&P'2002), Part 2

Article type: Research Article

Authors: Penczek, Wojciech^; | Lomuscio, Alessio

Affiliations: Institute of Computer Science, PAS, 01-237 Warsaw, ul. Ordona 21, Poland | Podlasie Academy, Institute of Informatics, Siedlce, Poland | Department of Computer Science, King's College London, London WC2R 2LS, UK

Abstract: We present a framework for verifying temporal and epistemic properties of multi-agent systems by means of bounded model checking. We use interpreted systems as underlying semantics. We give details of the proposed technique, and show how it can be applied to the "attacking generals problem", a typical example of coordination in multi-agent systems.

Journal: Fundamenta Informaticae, vol. 55, no. 2, pp. 167-185, 2003