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

TL;DR

This paper surveys recent symbolic model checking techniques, including OBDD and SAT-based methods, for verifying temporal epistemic logics in discrete and real-time systems.

Contribution

It provides a comprehensive overview of recent advances in symbolic model checking for temporal epistemic logics, highlighting OBDD and SAT-based approaches.

Findings

OBDD-based methods effectively verify temporal epistemic properties.

SAT-based approaches offer scalable solutions for real-time systems.

The survey identifies key challenges and future directions in the field.

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.