Vous êtes ici : Accueil > Université > Composantes > Faculté d’Informatique > Séminaires IRIT UT Capitole
- Recherche,
"A logic for game description and strategic reasoning", par Guifei Jiang, séminaire de l'IRIT
le 4 novembre 2014
12h30 - 13h30
Manufacture des Tabacs
ME303
ME303
Guifei Jiang, de l'Université Western Sydney et de l'UT1 (doctorante) parlera de "GDL meets ATL : a logic for game description and strategic reasoning"
Ce séminaire sera présenté entièrement en anglais
Résumé :
Références
[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).
Résumé :
"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*."
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*."
Références
[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).
Mis à jour le 31 octobre 2014