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

共 50 条

[41] A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic
M. Kacprzak
W. Penczek
Synthese, 2004, 142 : 203 - 227
[42] Model Checking Probabilistic Epistemic Logic for Probabilistic Multiagent Systems
Fu, Chen
Turrini, Andrea
Huang, Xiaowei
Song, Lei
Feng, Yuan
Zhang, Lijun
PROCEEDINGS OF THE TWENTY-SEVENTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2018, : 4757 - 4763
[43] Bounded model checking distributed temporal logic
Peres, Augusto
Ramos, Jaime
Dionisio, Francisco
JOURNAL OF LOGIC AND COMPUTATION, 2023, 33 (05) : 1022 - 1059
[44] RESOLUTION AND MODEL CHECKING FOR TEMPORAL LOGIC - A COMPARISON
CAVALLI, AR
JOURNAL OF SYMBOLIC LOGIC, 1987, 52 (04) : 1063 - 1063
[45] Exploiting symmetry in temporal logic model checking
Clarke, EM
Enders, R
Filkorn, T
Jha, S
FORMAL METHODS IN SYSTEM DESIGN, 1996, 9 (1-2) : 77 - 104
[46] Coverage metrics for temporal logic model checking*
Hana Chockler
Orna Kupferman
Moshe Y. Vardi
Formal Methods in System Design, 2006, 28 : 189 - 212
[47] Model Checking General Linear Temporal Logic
French, Tim
McCabe-Dansted, John
Reynolds, Mark
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS (TABLEAUX 2013), 2013, 8123 : 119 - 133
[48] Operator precedence temporal logic and model checking
Chiari, Michele
Mandrioli, Dino
Pradella, Matteo
THEORETICAL COMPUTER SCIENCE, 2020, 848 : 47 - 81
[49] Decidability of model checking with the temporal logic EF
Mayr, R
THEORETICAL COMPUTER SCIENCE, 2001, 256 (1-2) : 31 - 62
[50] Model Checking over Paraconsistent Temporal Logic
陈冬火
王林章
崔家林
JournalofDonghuaUniversity(EnglishEdition), 2008, 25 (05) : 571 - 580

← 1 2 3 4 5 →