Tech Reports

ULCS-09-014

Model Checking GDL through MOCHA: A Case Study

Ji Ruan, Wiebe van der Hoek and Michael Wooldridge

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 to play a specific game. Software participants in the competition are provided with a game specified in GDL, and then required to play this game, interpreting the GDL specification for themselves in order to determine the rules of the game. However, not all GDL specifications correspond to games, let alone meaningful, non-trivial games. We address the problem of verifying that games specified in GDL satisfy appropriate conditions, defining not just games, but meaningful games; we refer to these as playability conditions. Our approach is based on model checking formulae of Alternating-time Temporal Logic (ATL) over GDL specifications. Following an introduction to GDL and ATL, we present GDL2RML, a tool enabling model checking ATL formulae over GDL specifications using MOCHA - an ATL model checker. We illustrate the approach by a case study with experimental results.

Keywords: Game Description Language, Alternating-time Temporal Logic, Specification, Model checking

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.