Bounded versus Unbounded Model Checking for Interpreted Systems

This paper addresses the problem of verification of multiagent systems by means of symbolic model checking. It is shown how to adapt the techniques of bounded and unbounded model checking to verify temporal epistemic properties of multi-agent systems. We give details of these two techniques for the logic that extends CTLK by past modalities, and show how it can be applied to the well known train, gate and controller problem