Title: Verification of Games in the Game Description Language
Authors: 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 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.
Link to an online version: http://portal.acm.org/citation.cfm?id=1666968.1666995&coll=&dl=
Bibtex:
@article{RuanHW:2009JLC,
author = {Ruan, Ji and van der Hoek, Wiebe and Wooldridge, Michael},
title = {Verification of Games in the Game Description Language},
journal = {J. Log. and Comput.},
volume = {19},
number = {6},
year = {2009},
issn = {0955-792X},
pages = {1127–1156},
doi = {http://dx.doi.org/10.1093/logcom/exp039},
publisher = {Oxford University Press},
address = {Oxford, UK},
}
On 5th July 2009, a tragic event happened in Urumqi, the capital of Xinjiang Province, China. As of 9th July, it has been reported that 156 people died, and more than 1000 people injured. I was saddened by the news. So what happened? What are the causes of this tragic? What is still going on? Here is a list of information sources I collected. I will keep updating it until I know enough to answer these questions.
- July 2009 Urumqi riots (Wikipedia)
- Search for Han Chinese sister whose family were butchered by Uighurs (The Times, 10 July)
- Roit Video 1 (*containing very disturbing images, Youtube)
- Photos on 8th July (Boston.com)
- The Urumqi Mass Incident (A compilation of news from many sources. *Containing very disturbing images)
- Migrants Describe Grief From China’s Strife (New York Times)
- The riots in Xinjiang: Is China fraying? (Economist.com)
My joint paper with Wiebe and Mike with title “Verification of Games in the Game Description Language”, has been accepted by the Journal of Logic and Computation. This is my second journal paper.
Here is the preview version (final draft). The first version was submitted on 8th August, 2008.
I have only a Chinese version yet: #lvba #greendam
当GFW遭遇微博客（1）
In this first article, I try to analysis the huge impact of the uprising of micro-blogging services towards the Great Firewall (GFW), which is created by the Chinese government to censor the Chinese Internet. My website was blocked by the GFW from August 2008 to May 2009, so during that period, the users from China mainland could not directly access my website. Whenever they tried to connect to any page in jiruan.net, their web browsers would get a “The Connection Has Been Reset” error message.
I will argue that the micro-blogging services are making the GFW more difficult to stop the information flow to Chinese people. I believe that this is the very reason that recently Chinese government requested all the pc vendors in China install a censorship software called “Green Dam + Youth Escourt” by 1st July.
Title: Model Checking Knowledge Dynamics of Multi-Agent Systems
- Time: 3PM, 29 May 2009
- Location: Seminar room in the Centre for Logic and Information at StFX.
- Talk Slides: available upon request.
Abstract:
In this talk, I will first briefly introduce Model Checking and Multi-Agent Systems (MAS), then focus on two frameworks on modelling knowledge dynamics of MAS. The first is Dynamic Epistemic Logic, which is reasoning about knowledge and actions, and the second is Temporal Epistemic Logic, which is reasoning about knowledge and time. Then I will give a comparison of three state-of-the-art model checkers for MAS (DEMO, MCK and MCMAS) by verifying a communication protocol for Russian Cards Problem. Finally I will discuss with the audience about the possible ways of modelling the interactions in Health Care Services & Work-flows.
(Some work was jointly done with H.P van Ditmarsch, W. van der Hoek, and R. van der Meyden)
References:
- Chapter 6 of my PhD Thesis.
This Russian Cards Problem originated at the Moscow Math Olympiad 2000. Maybe you could try to solve it before the talk.
From a pack of seven known cards two players each draw three cards and a third player gets the remaining card. How can the players with three cards openly inform each other about their cards, without the third player learning from any of their cards who holds it?
