From Bounded to Unbounded Model Checking for Temporal Epistemic Logic
Magdalena Kacprzak, Alessio R. Lomuscio, Wojciech Penczek · Fundamenta Informaticae · 2004
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.