Symbolic model checking for temporal-epistemic logics
Alessio R. Lomuscio, Wojciech Penczek · ACM SIGACT News · 2007
Abstract. We survey some of the recent work in verification via symbolic model checking of temporal-epistemic logic. Specifically, we discuss OBDD-based and SAT-based approaches for epistemic logic built on discrete and real-time branching time temporal logic. The underlying semantical model considered throughout is the one of interpreted system, suitably extended whenever necessary. 1