Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics

2007/09/04 by Alessio Lomuscio, Lomuscio, Alessio, Wojciech Penczek +1
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Logic, Reasoning, and Knowledge

paper · pdf · doi:10.48550/arxiv.0709.0446

Abstract

This article surveys some of the recent work in verification of temporal epistemic logic via symbolic model checking, focusing on OBDD-based and SAT-based approaches for epistemic logics built on discrete and real-time branching time temporal logics.

Citations

• Alternating-time temporal logic
• Graph-Based Algorithms for Boolean Function Manipulation

Related

• Model checking: the interval way
• Unifying Hyper and Epistemic Temporal Logic
• Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic
• SCTL: Towards Combining Model Checking and Proof Checking
• Learning Branching-Time Properties in CTL and ATL via Constraint Solving