A Hennessy-Milner Theorem for ATL with Imperfect Information

Francesco Belardinelli; Catalin Dima; Vadim Malvone; Ferucio Tiplea

doi:10.1145/3373718.3394784

A Hennessy-Milner Theorem for ATL with Imperfect Information

Francesco Belardinelli
, Catalin Dima
, Vadim Malvone
, Ferucio Tiplea

Imperial College London
Université de PARIS XII
Université d'Evry Val d'Essonne
Alexandru Ioan Cuza University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Citation (Scopus)

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 accomodate 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.

Original language	English
Title of host publication	Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
Publisher	Association for Computing Machinery
Pages	181-194
Number of pages	14
ISBN (Electronic)	9781450371049
DOIs	https://doi.org/10.1145/3373718.3394784
Publication status	Published - 8 Jul 2020
Externally published	Yes
Event	35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 - Saarbrucken, Germany Duration: 8 Jul 2020 → 11 Jul 2020

Publication series

Name	ACM International Conference Proceeding Series

Conference

Conference	35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
Country/Territory	Germany
City	Saarbrucken
Period	8/07/20 → 11/07/20

Keywords

ATL
Bisimulation
Concurrent Game Structures with Imperfect Information
Gale-Stewart determinacy

Access to Document

10.1145/3373718.3394784

Cite this

Belardinelli, F., Dima, C., Malvone, V., & Tiplea, F. (2020). A Hennessy-Milner Theorem for ATL with Imperfect Information. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 (pp. 181-194). Article 3394784 (ACM International Conference Proceeding Series). Association for Computing Machinery. https://doi.org/10.1145/3373718.3394784

@inproceedings{68093e5c53684c1ba9bd7814e713b1b7,

title = "A Hennessy-Milner Theorem for ATL with Imperfect Information",

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 accomodate 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 = "ATL, Bisimulation, Concurrent Game Structures with Imperfect Information, Gale-Stewart determinacy",

author = "Francesco Belardinelli and Catalin Dima and Vadim Malvone and Ferucio Tiplea",

note = "Publisher Copyright: {\textcopyright} 2020 ACM.; 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 ; Conference date: 08-07-2020 Through 11-07-2020",

year = "2020",

month = jul,

day = "8",

doi = "10.1145/3373718.3394784",

language = "English",

series = "ACM International Conference Proceeding Series",

publisher = "Association for Computing Machinery",

pages = "181--194",

booktitle = "Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020",

}

Belardinelli, F, Dima, C, Malvone, V & Tiplea, F 2020, A Hennessy-Milner Theorem for ATL with Imperfect Information. in Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020., 3394784, ACM International Conference Proceeding Series, Association for Computing Machinery, pp. 181-194, 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020, Saarbrucken, Germany, 8/07/20. https://doi.org/10.1145/3373718.3394784

A Hennessy-Milner Theorem for ATL with Imperfect Information. / Belardinelli, Francesco; Dima, Catalin; Malvone, Vadim et al.
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020. Association for Computing Machinery, 2020. p. 181-194 3394784 (ACM International Conference Proceeding Series).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - A Hennessy-Milner Theorem for ATL with Imperfect Information

AU - Belardinelli, Francesco

AU - Dima, Catalin

AU - Malvone, Vadim

AU - Tiplea, Ferucio

PY - 2020/7/8

Y1 - 2020/7/8

N2 - 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 accomodate 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.

AB - 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 accomodate 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.

KW - ATL

KW - Bisimulation

KW - Concurrent Game Structures with Imperfect Information

KW - Gale-Stewart determinacy

U2 - 10.1145/3373718.3394784

DO - 10.1145/3373718.3394784

M3 - Conference contribution

AN - SCOPUS:85085951602

T3 - ACM International Conference Proceeding Series

SP - 181

EP - 194

BT - Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020

PB - Association for Computing Machinery

T2 - 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020

Y2 - 8 July 2020 through 11 July 2020

ER -

A Hennessy-Milner Theorem for ATL with Imperfect Information

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this