Symbolic model checking for temporal-epistemic logic

被引：5

作者：

Lomuscio, Alessio ^{[1
]}

Penczek, Wojciech ^{[2
]}

机构：

[1] Department of Computing, Imperial College London, United Kingdom

[2] ICS PAS Warsaw, UPH Siedlce, Poland

来源：

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 2012年 / 7360 LNCS卷

基金：

英国工程与自然科学研究理事会;

关键词：

Temporal logic - Computer circuits;

D O I：

10.1007/978-3-642-29414-3_10

中图分类号：

学科分类号：

摘要：

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. © 2012 Springer-Verlag Berlin Heidelberg.

引用

页码：172 / 195