Riccardo Pucella
Abstract
In this issue, Lomuscio and Penczek survey some of the recent work in verification of temporal-epistemic logic via symbolic model checking, focussing on OBDD-based and SAT-based approaches for epistemic logics built on discrete and real-time branching time temporal logics.
- H. P. van Ditmarsch, W. van der Hoek, R. van der Meyden, and J. Ruan. Model checking Russian Cards. Electronic Notes in Theoretical Computer Science, 149(2):105--123, 2006. Google Scholar
Digital Library
- H. P. van Ditmarsch. The Russian Cards problem. Studia Logica, 75:31--62, 2003.Google ScholarCross Ref
Index Terms
- Introduction
Recommendations
A tutorial introduction to symbolic model checking
Logic for concurrency and synchronisationSymbolic model checking is a powerful formal verification technique that, contrarily to theorem proving, requires no user assistance. It is able to verify that an implementation, modelled as a labelled finite-state transition graph, satisfies its ...
Introduction to generalized symbolic trajectory evaluation
Special section on the 2001 international conference on computer design (ICCD)Symbolic trajectory evaluation (STE) is a lattice-based model checking technology that uses a form of symbolic simulation. It offers an alternative to 'classical' symbolic model checking that, within its domain of applicability, often is much easier to ...
Comments