A Lazy Approach to Temporal Epistemic Logic Model Checking

Temporal Epistemic Logic is used to reason about the evolution of knowledge over time. A notable example is the temporal epistemic logic KL1, which is used to model what a reasoner can infer about the state of a dynamic system by using available observations. Applications of KL1 span from security (verification of cryptography protocols and information flow) to diagnostic systems (fault detection and diagnosability). In this paper, we tackle the verification of KL1 properties under observational semantics, by proposing an effective approach that is able to deal with both finite and infinite state systems. The denotation of the epistemic atoms is computed in a lazy way, driven by the counterexamples obtained from model checking an abstraction of the property. We analyze the approach on a comprehensive set of finite-and infinite-state benchmarks from the literature, evaluate the effectiveness of various optimizations, and demonstrate that our approach outperforms existing approaches.