Verification of Games in the Game Description Language

August 2009 Update: Final version is available here.

July 2009 Update: This paper has been accepted by the JLC.

March 2009 Update: The Journal of Logic and Computation (JLC) has sent us back the reviews, and we need a revision before it gets accepted.

This is a joint work with my PhD supervisors Wiebe van der Hoek and Michael Wooldridge.

It is submitted to the Journal of Logic and Computation. Comments are very welcomed and please contact ji@jiruan.net ( or j.ruan@csc.liv.ac.uk as listed in the paper).


The Game Description Language (GDL) is a special purpose declarative language for defining games. GDL is used in the AAAI General Game Playing Competition, which tests the ability of computer programs to play games in general, rather than just the ability to play a specific game. Participants in the competition are provided with a previously unknown game specified in GDL, and are required to dynamically and autonomously determine how best to play this game. Recently, there has been much interest in the use of strategic cooperation logics for reasoning about game-like scenarios — the Alternating-time Temporal Logic (ATL) of Alur, Henzinger, and Kupferman is perhaps the best known example. Such logics are specifically intended to support reasoning about game-theoretic properties of multi-agent systems. In short, the aim of this article is to make a concrete link between ATL and GDL, with the ultimate goal of using ATL to reason about GDL-specified games.  We make three main contributions. First, we demonstrate that GDL can be understood as a specification language for ATL models, and prove that the problem of interpreting ATL formulae over propositional GDL descriptions is EXPTIME-complete. Second, we use ATL to characterize a class of “fair playability” conditions, which might or might not hold of various games. Third, we describe an automated tool that transforms a GDL description into RML, the model description language for the Mocha model checker, thereby permitting the use of Mocha for verifying playability properties on the RML description. We also present some experimental results on the use of this tool.

Short URL: http://goo.gl/zhwa4

No related posts.

Related posts brought to you by Yet Another Related Posts Plugin.

1 Comment

You must be logged in to post a comment.

    RSS Subscribe



    Locations of visitors to this page