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

TL;DR

This paper introduces a variant of ATL with distributed knowledge operators under perfect recall, enabling model-checking for systems with imperfect information and coalition cooperation, using game-theoretic techniques.

Contribution

It presents a decidable model-checking procedure for a new ATL variant incorporating knowledge, imperfect information, and perfect recall, with a novel game-based approach.

Findings

Model-checking is decidable for the proposed logic.

Uses game variants with imperfect information for verification.

Employs subset construction to identify indistinguishable states.

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.