A Hennessy-Milner Theorem for ATL with Imperfect Information

We show that a history-based variant of alternating bisimulation under imperfect information is related to a variant of ATL with imperfect information by a 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. The proof utilizes a bisimulation game between two coalitions, each composed of two agents, for which we provide a Gale-Stewart determinacy theorem. We notice that other semantic variants of ATL with imperfect information do not accomodate a reverse 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.