GDL meets ATL : a logic for game description and strategic reasoning

Guifei Jiang; Dongmo Zhang; Laurent Perrussel

doi:10.1007/978-3-319-13560-1_58

GDL meets ATL : a logic for game description and strategic reasoning

Guifei Jiang, Dongmo Zhang, Laurent Perrussel

Research output: Chapter in Book / Conference Paper › Conference Paper › peer-review

4 Citations (Scopus)

Abstract

This paper presents a logical framework that extends the Game Description Language with coalition operators from Alternatingtime Temporal Logic and prioritised strategy connectives. Our semantics is built upon the standard state transition model. The new framework allows us to formalise van Benthem's game-oriented principles in multiplayer games, and formally deriveWeak Determinacy and Zermelo's Theorem for two-player games. We demonstrate with a real-world game how to use our language to specify a game and design a strategy, and how to use our framework to verify a winning/no-losing strategy. Finally, we show that the model-checking problem of our logic is in 2EXPTIME with respect to the size of game structure and the length of formula, which is no worse than the model-checking problem in ATL*.

Original language	English
Title of host publication	PRICAI 2014: Trends in Artificial Intelligence: 13th Pacific Rim International Conference on Artificial Intelligence, Gold Coast, QLD, Australia, December 1-5, 2014, Proceedings
Publisher	Springer
Pages	733-746
Number of pages	14
ISBN (Print)	9783319135595
DOIs	https://doi.org/10.1007/978-3-319-13560-1_58
Publication status	Published - 2014
Event	Pacific Rim International Conference on Artificial Intelligence - Duration: 13 Sept 2019 → …

Conference

Conference	Pacific Rim International Conference on Artificial Intelligence
Period	13/09/19 → …

Keywords

artificial intelligence
computational linguistics
game theory
intelligent agents (computer software)
reasoning

Access to Document

10.1007/978-3-319-13560-1_58

Cite this

@inproceedings{6c77a3a2b054422c8e60056584759fff,

title = "GDL meets ATL : a logic for game description and strategic reasoning",

abstract = "This paper presents a logical framework that extends the Game Description Language with coalition operators from Alternatingtime Temporal Logic and prioritised strategy connectives. Our semantics is built upon the standard state transition model. The new framework allows us to formalise van Benthem's game-oriented principles in multiplayer games, and formally deriveWeak Determinacy and Zermelo's Theorem for two-player games. We demonstrate with a real-world game how to use our language to specify a game and design a strategy, and how to use our framework to verify a winning/no-losing strategy. Finally, we show that the model-checking problem of our logic is in 2EXPTIME with respect to the size of game structure and the length of formula, which is no worse than the model-checking problem in ATL*.",

keywords = "artificial intelligence, computational linguistics, game theory, intelligent agents (computer software), reasoning",

author = "Guifei Jiang and Dongmo Zhang and Laurent Perrussel",

year = "2014",

doi = "10.1007/978-3-319-13560-1_58",

language = "English",

isbn = "9783319135595",

pages = "733--746",

booktitle = "PRICAI 2014: Trends in Artificial Intelligence: 13th Pacific Rim International Conference on Artificial Intelligence, Gold Coast, QLD, Australia, December 1-5, 2014, Proceedings",

publisher = "Springer",

note = "Pacific Rim International Conference on Artificial Intelligence ; Conference date: 13-09-2019",

}

Jiang, G, Zhang, D & Perrussel, L 2014, GDL meets ATL : a logic for game description and strategic reasoning. in PRICAI 2014: Trends in Artificial Intelligence: 13th Pacific Rim International Conference on Artificial Intelligence, Gold Coast, QLD, Australia, December 1-5, 2014, Proceedings. Springer, pp. 733-746, Pacific Rim International Conference on Artificial Intelligence, 13/09/19. https://doi.org/10.1007/978-3-319-13560-1_58

GDL meets ATL : a logic for game description and strategic reasoning. / Jiang, Guifei; Zhang, Dongmo; Perrussel, Laurent.
PRICAI 2014: Trends in Artificial Intelligence: 13th Pacific Rim International Conference on Artificial Intelligence, Gold Coast, QLD, Australia, December 1-5, 2014, Proceedings. Springer, 2014. p. 733-746.

Research output: Chapter in Book / Conference Paper › Conference Paper › peer-review

TY - GEN

T1 - GDL meets ATL : a logic for game description and strategic reasoning

AU - Jiang, Guifei

AU - Zhang, Dongmo

AU - Perrussel, Laurent

PY - 2014

Y1 - 2014

N2 - This paper presents a logical framework that extends the Game Description Language with coalition operators from Alternatingtime Temporal Logic and prioritised strategy connectives. Our semantics is built upon the standard state transition model. The new framework allows us to formalise van Benthem's game-oriented principles in multiplayer games, and formally deriveWeak Determinacy and Zermelo's Theorem for two-player games. We demonstrate with a real-world game how to use our language to specify a game and design a strategy, and how to use our framework to verify a winning/no-losing strategy. Finally, we show that the model-checking problem of our logic is in 2EXPTIME with respect to the size of game structure and the length of formula, which is no worse than the model-checking problem in ATL*.

AB - This paper presents a logical framework that extends the Game Description Language with coalition operators from Alternatingtime Temporal Logic and prioritised strategy connectives. Our semantics is built upon the standard state transition model. The new framework allows us to formalise van Benthem's game-oriented principles in multiplayer games, and formally deriveWeak Determinacy and Zermelo's Theorem for two-player games. We demonstrate with a real-world game how to use our language to specify a game and design a strategy, and how to use our framework to verify a winning/no-losing strategy. Finally, we show that the model-checking problem of our logic is in 2EXPTIME with respect to the size of game structure and the length of formula, which is no worse than the model-checking problem in ATL*.

KW - artificial intelligence

KW - computational linguistics

KW - game theory

KW - intelligent agents (computer software)

KW - reasoning

UR - http://handle.uws.edu.au:8081/1959.7/uws:28766

U2 - 10.1007/978-3-319-13560-1_58

DO - 10.1007/978-3-319-13560-1_58

M3 - Conference Paper

SN - 9783319135595

SP - 733

EP - 746

BT - PRICAI 2014: Trends in Artificial Intelligence: 13th Pacific Rim International Conference on Artificial Intelligence, Gold Coast, QLD, Australia, December 1-5, 2014, Proceedings

PB - Springer

T2 - Pacific Rim International Conference on Artificial Intelligence

Y2 - 13 September 2019

ER -

GDL meets ATL : a logic for game description and strategic reasoning

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this