From Bounded to Unbounded Model Checking for Temporal Epistemic Logic

Issue title: Multiagent Systems (FAMAS'03)

Article type: Research Article

Authors: Kacprzak, M. | Lomuscio, A. | Penczek, W.^;

Affiliations: Białystok University of Technology, Institute of Mathematics and Physics, 15-351 Białystok, ul. Wiejska 45A, Poland | Department of Computer Science, King's College London, London WC2R 2LS, United Kingdom | Institute of Computer Science, PAS, 01-237 Warsaw, ul. Ordona 21, Poland | Podlasie Academy, Institute of Informatics, Siedlce, Poland

Abstract: This paper addresses the problem of verification of temporal epistemic properties of multi-agent systems by means of symbolic model checking. An overview of the technique of bounded model checking for temporal epistemic logic, and an analysis of some limitations of the method are provided. An extension of this technique called unbounded model checking to solve these limitations is explored. Similarities and differences of the two methods are explicitly exemplified by the analysis of a scenario in the two formalisms.

Journal: Fundamenta Informaticae, vol. 63, no. 2-3, pp. 221-240, 2004