OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

GDL Meets ATL: A Logic for Game Description and Strategic Reasoning

Jiang, Guifei and Zhang, Dongmo and Perrussel, Laurent GDL Meets ATL: A Logic for Game Description and Strategic Reasoning. (2014) In: 13th Pacific Rim International Conference on Artificial Intelligence (PRICAI 2014), 1 December 2014 - 5 December 2014 (Gold Coast, QLD, Australia).

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: http://dx.doi.org/10.1007/978-3-319-13560-1_58


This paper presents a logical framework that extends the Game Description Language with coalition operators from Alternating-time 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 multi-player games, and formally derive Weak 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.

Item Type:Conference or Workshop Item (Paper)
Additional Information:Thanks to Springer editor. This papers appears in Volume 8862 Lecture Notes in Computer Science ISSN : 0302-9743. ISBN: 978-3-319-13559-5. The original PDF is available at : http://link.springer.com/chapter/10.1007%2F978-3-319-13560-1_58
HAL Id:hal-01316838
Audience (conference):National conference proceedings
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > University of Western Sydney - UWS (AUSTRALIA)
Laboratory name:
Deposited On:20 Apr 2016 12:39

Repository Staff Only: item control page