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

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
titre	Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
Editeur	Association for Computing Machinery
Pages	181-194
Nombre de pages	14
ISBN (Electronique)	9781450371049
Les DOIs	https://doi.org/10.1145/3373718.3394784
état	Publié - 8 juil. 2020
Modification externe	Oui
Evénement	35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 - Saarbrucken, Allemagne Durée: 8 juil. 2020 → 11 juil. 2020

Série de publications

Nom	ACM International Conference Proceeding Series

Une conférence

Une conférence	35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020
Pays/Territoire	Allemagne
La ville	Saarbrucken
période	8/07/20 → 11/07/20

Accès au document

10.1145/3373718.3394784

Contient cette citation

Belardinelli, F., Dima, C., Malvone, V., & Tiplea, F. (2020). A Hennessy-Milner Theorem for ATL with Imperfect Information. Dans Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020 (p. 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. Dans 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, p. 181-194, 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020, Saarbrucken, Allemagne, 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).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

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

Résumé

Série de publications

Une conférence

Accès au document

Empreinte digitale

Contient cette citation