• Research,

Guifei Jiang - GDL Meets ATL: A logic for game description and strategic reasoning

on the November 4, 2014

 12:30 - 13:30
Unknown label

Guifei Jiang from University of Western Sydney and University of Toulouse 1 (Joint PhD student) will talk about "GDL Meets ATL: A logic for game description and strategic reasoning"

Logical analysis of games has been an important topic across the study of game theory, mathematics, philosophy and computer science. It deals with the problems of how to specify a game situation, how to represent a game strategy and, more importantly, how to model strategic reasoning of game players.

In this report, I will present a logical framework we have proposed for game description and strategic reasoning. The language of this framework extends Game Description Language (GDL) [1] with coalition operators from Alternating-time Temporal Logic (ATL) [2] and prioritised strategy connectives from Zhang and Thielscher's framework [3]. The 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. I will demonstrate with a real-world game how to use our language to specify a game and represent a winning/no-losing strategy. The model-checking problem of our logic is proved in 2EXPTIME with respect to the size of game structure and the length of a formula, which is no worse than the model-checking problem in ATL*.


[1] Love, N., Hinrichs, T., Genesereth, M.: General game playing: Game description language specification. Tech. rep., Computer Scinece Department, Stanford University (2006).

[2] Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic.Journal of the ACM  49(5),  672--713 (2002).

[3] Zhang, D., Thielscher, M.: Representing and reasoning about game strategies. To appear in J. Philosophical Logic (2014).

Updated on October 23, 2014