Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions
Logic in Computer Science
2010-08-11 v1 Multiagent Systems
Abstract
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.
Cite
@article{arxiv.1006.1414,
title = {Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions},
author = {Cătălin Dima and Constantin Enea and Dimitar Guelev},
journal= {arXiv preprint arXiv:1006.1414},
year = {2010}
}