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 Abstract Freely available
Right arrow Full Text (PDF)
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.

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



References

  1. Alur R, de Alfaro L, Henzinger TA, Krishnan SC, Mang FYC, Qadeer S, Rajamani SK, Tasiran S. MOCHA user manual. In: University of Berkeley Report (2000).
  2. Alur R, Henzinger T, Kupferman O, Vardi M. Alternating refinement relations. (1998) Springer-Verlag. 163–178. In International Conference on Concurrency Theory, Vol. 1466 of Lecture Notes in Computer Science.
  3. Alur R, Henzinger TA, Kupferman O. Alternating-time temporal logic. Journal of the ACM (2002) 49:672–713.[CrossRef][Web of Science]
  4. Alur R, Henzinger TA, Mang FYC, Qadeer S, Rajamani SK, Tasiran S. Mocha: modularity in model checking. (1998) Springer. 521–525. In CAV 1998: Tenth International Conference on Computeraided Verification, (LNCS Volume 1427).
  5. Apt K. Introduction to logic programming. In: Handbook of Theoretical Computer Science—van Leeuwen J, ed. (1990) Elsevier. 494–574.
  6. Clarke EM, Grumberg O, Peled DA. Model Checking (2000) The MIT Press.
  7. Clocksin WF, Mellish CS. Programming in Prolog (1981) Springer.
  8. Dixit A, Skeath S. Games of Strategy (2004) 2nd edn. W.W. Norton & Co. Inc.
  9. van Drimmelen G. Satisfiability in alternating-time temporal logic. (2003) Canada: Ottawa. 208–217. In Eighteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2003).
  10. Emerson EA. Temporal and modal logic. In: Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics—van Leeuwen J, ed. (1990) Elsevier Science Publishers B.V. 996–1072.
  11. Francez N. Fairness (1986) Springer.
  12. Genereseth M, Love N. General game playing: overview of the AAAI competition. In: Technical report (2005) Stanford: Stanford University.
  13. Goldblatt R. Logics of Time and Computation (CSLI Lecture Notes Number 7) (1987) Ventura Hall: Center for the Study of Language and Information. (Distributed by Chicago University Press).
  14. Goranko V. Coalition games and alternating temporal logics. van Benthem J, ed. (2001) Italy: Siena. 259–272. In Proceeding of the Eighth Conference on Theoretical Aspects of Rationality and Knowledge (TARK VIII).
  15. Goranko V, Jamroga W. Comparing semantics of logics for multi-agent systems. Synthese (2004) 139:241–280.[CrossRef][Web of Science]
  16. Goranko V, Shkatov D. Tableau-based decision procedures for logics of strategic ability in multi-agent systems. In: ACM Transactions on Computational Logic (2009) To appear.
  17. Love N, Hinrichs T, Genesereth M. General game playing: game description language specification. In: Technical report (2006) Stanford: Stanford University.
  18. Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurrent Systems (1992) Springer.
  19. Manna Z, Pnueli A. Temporal Verification of Reactive Systems — Safety (1995) Springer.
  20. McCarthy J, Hayes PJ. Some philosophical problems from the standpoint of artificial intelligence. In: Machine Intelligence 4—Meltzer B, Michie D, eds. (1969) Edinburgh University Press. 463–502.
  21. Pauly M. Logic for Social Software (2001) University of Amsterdam. PhD Thesis, ILLC Dissertation Series 2001–10.
  22. Pauly M, Wooldridge M. Logic for mechanism design — a manifesto. In: Proceedings of the 2003 Workshop on Game Theory and Decision Theory in Agent Systems (GTDT-2003) (2003) Melbourne.
  23. Pell B. Strategy Generation and Evaluation for Meta-Game Playing (1993) Trinity College, University of Cambridge. PhD Thesis.
  24. Ruan J, van der Hoek W, Wooldridge M. Model checking GDL through MOCHA: a case study. In: Technical Report ULCS-09-14 (2009) Department of Computer Science, University of Liverpool.
  25. Stockmeyer LJ, Chandra AK. Provably difficult combinatorial games. SIAM Journal of Computing (1979) 8:151–174.[CrossRef]
  26. van der Hoek W, Lomuscio AR, Wooldridge M. On the complexity of practical ATL model checking. (2006) ACM. 201–208. In Proceedings of the Fifth International Joint Conference on Autonomous Agents & Multiagent Systems (AAMAS 2006).
  27. van der Hoek W, Roberts M, Wooldridge M. Social laws in alternating time: effectiveness, feasibility, and synthesis. Synthese (2007) 156:1–19.[CrossRef][Web of Science]
  28. van der Hoek W, Wooldridge M. Time, knowledge, and cooperation: alternating-time temporal epistemic logic and its applications. Studia Logica (2003) 75:125–157.[CrossRef]
  29. Walther D, Lutz C, Wolter F, Wooldridge M. ATL satisfiability is indeed ExpTimecomplete. Journal of Logic and Computation (2006) 16:765–787.[Abstract/Free Full Text]

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



This Article
Right arrow Abstract Freely available
Right arrow Full Text (PDF)
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?