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

References

[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).