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
关键词
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 条