Skip Navigation



Journal of Logic and Computation Advance Access published online on August 5, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp039
This Article
Right arrow Full Text (PDF)
Right arrow References
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Ruan, J.
Right arrow Articles by Wooldridge, M.
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

Verification of Games in the Game Description Language

Ji Ruan, Wiebe Van Der Hoek and Michael Wooldridge

Department of Computer Science, University of Liverpool, Liverpool L69 3BX, UK.
E-mail: j.ruan{at}csc.liv.ac.uk; wiebe{at}csc.liv.ac.uk; mjw{at}csc.liv.ac.uk

Received 8 August 2008.


  Abstract

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 the following 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.

Keywords: Verification; general game playing; game description language; alternating-time temporal logic; model checking


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer: Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.