Model-Checking an Alternating-time Temporal Logic with Knowledge, Imperfect Information, Perfect Recall and Communicating Coalitions

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.

References in corpus (1)

• Algorithms for Omega-Regular Games with Imperfect Information

Cited by in corpus (8)

• Opacity Issues in Games with Imperfect Information
• Fixpoint Approximation of Strategic Abilities under Imperfect Information
• The Complexity of Synthesizing Uniform Strategies
• Model Checking an Epistemic mu-calculus with Synchronous and Perfect Recall Semantics
• Model-checking an Epistemic μ-calculus with Synchronous and Perfect Recall Semantics
• Games on graphs with a public signal monitoring
• Dynamic Connected Cooperative Coverage Problem
• Computationally Feasible Strategies