@inproceedings{publications29976,
       booktitle = {13th Pacific Rim International Conference on Artificial Intelligence (PRICAI 2014)},
          number = {8862},
           title = {GDL Meets ATL: A Logic for Game Description and Strategic Reasoning},
          author = {Guifei Jiang and Dongmo Zhang and Laurent Perrussel},
       publisher = {Springer-Verlag},
            year = {2014},
           pages = {733--746},
        keywords = {Information storage and retrieval},
             url = {https://publications.ut-capitole.fr/id/eprint/29976/},
        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.}
}