A Hennessy-Milner Theorem for ATL with Imperfect Information

TL;DR

This paper establishes a Hennessy-Milner theorem for a history-based variant of ATL with imperfect information, linking bisimulation and logic semantics, and discusses the undecidability of bisimulation existence.

Contribution

It introduces a full Hennessy-Milner theorem for a history-based ATL variant with imperfect information and common knowledge semantics, and proves the undecidability of bisimulation between finite structures.

Findings

Hennessy-Milner theorem holds for the proposed ATL variant.

Bisimulation existence between finite structures is undecidable.

The ATL variant requires common knowledge semantics.

Abstract

We show that a history-based variant of alternating bisimulation with imperfect information allows it to be related to a variant of Alternating-time Temporal Logic (ATL) with imperfect information by a full Hennessy-Milner theorem. The variant of ATL we consider has a common knowledge semantics, which requires that the uniform strategy available for a coalition to accomplish some goal must be common knowledge inside the coalition, while other semantic variants of ATL with imperfect information do not accommodate a Hennessy-Milner theorem. We also show that the existence of a history-based alternating bisimulation between two finite Concurrent Game Structures with imperfect information (iCGS) is undecidable.