文章基本信息

标题：Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions
本地全文：下载
作者：Cătălin Dima ; Constantin Enea ; Dimitar Guelev 等
期刊名称：Electronic Proceedings in Theoretical Computer Science
电子版ISSN：2075-2180
出版年度：2010
卷号：25
页码：103-117
DOI：10.4204/EPTCS.25.12
出版社：Open Publishing Association
摘要：We present a variant of ATL with distributed knowledge operators based on a synchronous and perfect recall semantics. The coalition modalities in this logic are based on partial observation of the full history, and incorporate a form of cooperation between members of the coalition in which agents issue their actions based on the distributed knowledge, for that coalition, of the system history. We show that model-checking is decidable for this logic. The technique utilizes two variants of games with imperfect information and partially observable objectives, as well as a subset construction for identifying states whose histories are indistinguishable to the considered coalition.