English

A Hennessy-Milner Theorem for ATL with Imperfect Information

Logic in Computer Science 2020-06-29 v1 Multiagent Systems

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.

Keywords

Cite

@article{arxiv.2006.15000,
  title  = {A Hennessy-Milner Theorem for ATL with Imperfect Information},
  author = {Francesco Belardinelli and Catalin Dima and Vadim Malvone and Ferucio Tiplea},
  journal= {arXiv preprint arXiv:2006.15000},
  year   = {2020}
}