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

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

[img]
Preview
Text
Download (12MB) | Preview

Abstract

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)
Language: English
Date: 2014
Uncontrolled Keywords: Information storage and retrieval
Subjects: H- INFORMATIQUE
Divisions: Institut de Recherche en Informatique de Toulouse
Site: UT1
Date Deposited: 25 Mar 2019 14:29
Last Modified: 25 Mar 2019 14:29
URI: http://publications.ut-capitole.fr/id/eprint/29976

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year