×

zbMATH — the first resource for mathematics

Symbolic model checking for temporal-epistemic logic. (English) Zbl 1356.68144
Artikis, Alexander (ed.) et al., Logic programs, norms and action. Essays in honor of Marek J. Sergot on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-642-29413-6/pbk). Lecture Notes in Computer Science 7360. Lecture Notes in Artificial Intelligence, 172-195 (2012).
Summary: 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.
For the entire collection see [Zbl 1241.68007].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B42 Logics of knowledge and belief (including belief change)
03B44 Temporal logic
Software:
MCK; NuSMV; CUDD; MCMAS; Verics; SPIN
PDF BibTeX Cite
Full Text: DOI