MODEL-CHECKING ALTERNATING-TIME TEMPORAL LOGIC WITH STRATEGIES BASED ON COMMON KNOWLEDGE IS UNDECIDABLE

被引：4

作者：

Diaconu, Raluca ^{[1
,2
]}

Dima, Catalin ^{[1
]}

机构：

[1] Univ Paris Est Creteil, LACL, F-94010 Creteil, France

[2] Alexandru Ioan Cuza Univ, Dept Comp Sci, Iasi, Romania

来源：

APPLIED ARTIFICIAL INTELLIGENCE | 2012年 / 26卷 / 04期

关键词：

Computer circuits - Model checking - Temporal logic;

D O I：

10.1080/08839514.2012.652905

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We present a semantics for the Alternating-time Temporal Logic (ATL) with imperfect information, in which the participants in a coalition choose their strategies such that each agent's choice is the same in all states that form the common knowledge for the coaltion. We show that ATL with this semantics has an undecidable model-checking problem if the semantics is also synchronous and the agents have perfect recall.

引用

页码：331 / 348

页数：18

共 50 条

[1] Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions
Dima, Catalin
Enea, Constantin
Guelev, Dimitar
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (25): : 103 - 117
[2] Parameterised Model Checking for Alternating-Time Temporal Logic
Kouvaros, Panagiotis
Lomuscio, Alessio
[J]. ECAI 2016: 22ND EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2016, 285 : 1230 - 1238
[3] Model Checking Alternating-time Temporal Logics of Knowledge
Long Shigong
Luo Wenjun
[J]. 2008 4TH INTERNATIONAL CONFERENCE ON WIRELESS COMMUNICATIONS, NETWORKING AND MOBILE COMPUTING, VOLS 1-31, 2008, : 5424 - 5426
[4] Probabilistic alternating-time temporal logic and model checking algorithm
Chen, Taolue
Lu, Jian
[J]. FOURTH INTERNATIONAL CONFERENCE ON FUZZY SYSTEMS AND KNOWLEDGE DISCOVERY, VOL 2, PROCEEDINGS, 2007, : 35 - +
[5] Fully symbolic unbounded model checking for Alternating-time Temporal Logic
Kacprzak, M
Penczek, W
[J]. AUTONOMOUS AGENTS AND MULTI-AGENT SYSTEMS, 2005, 11 (01) : 69 - 89
[6] Action and knowledge in alternating-time temporal logic
Ågotnes, T
[J]. SYNTHESE, 2006, 149 (02) : 121 - 153
[7] Action and Knowledge in Alternating-Time Temporal Logic
Thomas Ågotnes
[J]. Synthese, 2006, 149 : 375 - 407
[8] A SAT-based approach to unbounded model checking for Alternating-time Temporal Epistemic Logic
Kacprzak, M
Penczek, W
[J]. SYNTHESE, 2004, 142 (02) : 203 - 227
[9] A Sat-Based Approach to Unbounded Model Checking for Alternating-Time Temporal Epistemic Logic
M. Kacprzak
W. Penczek
[J]. Synthese, 2004, 142 : 203 - 227
[10] On the Complexity of Model-Checking Branching and Alternating-Time Temporal Logics in One-Counter Systems
Vester, Steen
[J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015, 2015, 9364 : 361 - 377

← 1 2 3 4 5 →