Games Meeting Cambridge 2006


This conference, organised as an Isaac Newton Institute Workshop on Games and Verification, was the final meeting of the previous GAMES research training network.

Games are pervasive in the theory of computation. Traditionally, they have been used as tools for understanding definability in logic. For example, in the case of finite model theory they provide a mechanism for showing that certain properties are not definable in enrichments of first-order logic that are computationally interesting. A second role is that important algorithmic questions can be couched in terms of games. For instance, model checking properties expressible in modal logic with fixed points is equivalent to deciding which player has a winning strategy in a simple two-player game, the parity game. The exact complexity of this model checking problem is a long standing open problem, and games may help to solve it. In fact more generally, games are useful, as alternating automata, for solving a variety of algorithmic questions about finite and infinite state systems (such as reachability and liveness properties). A third, and much more recent, use of games is the semantics of programming languages. The idea is that the meaning of a program is defined in terms of winning strategies. What is particularly exciting about this approach is that such a semantics is exact in the sense that it is fully abstract.

The aim of the conference is to bring together researchers who work in these different areas. In one direction, there is strong interest amongst the semanticists in understanding algorithmic properties of games in the semantics of programming languages. Researchers have examined fragments of Idealized Algol and shown that program equivalence is decidable by reducing it to equivalent decidable automata theoretic problems. In the opposite direciton, there is also strong interest amongst the model checking community to be able to cope with more realistic models of programs than classical automata. The meeting will begin with a number of invited tutorials covering the relevant areas before the more specialist contributed talks.

Invited Tutorials

  • Rajeev Alur Pushdown games
  • Johan van Bentham Dynamic-Epistemic Logic of Games
  • Didier Caucal Deterministic grammars
  • Georg Gottlob Hypertree decompositions
  • Dov Monderer Mechanism design
  • Moshe Vardi Games as an algorithmic construct


Monday, 3 July
8:30 9:00 Registration
9:00 10:25 Johan van Benthem Dynamic-epistemic logic of games
10:30 10:45 Lukasz Kaiser Game quantification on automatic structures and hierarchical games
11:00 11:30   Coffee
11:30 12:00 Jacques Duparc Towards the Wadge hierarchy of weak alternating tree automata
12:00 12:30 Jan Obdrzalek Are parity games spineless?
12:30 13:30   Lunch at Wolfson Court
14:00 14:30 Thomas Colcombet Ramseyan factorisation for trees
14:30 14:45 Mathias Samuelides Pebble tree-walking automata
14:45 15:00 Vince Barany A hierachy of automatically presentable omega-words having a decidable MSO theory
15:00 15:30   Tea
15:30 16:00 David Janin On distributed synthesis of discrete systems
16:00 16:30 Javier Esparza Solving fixpoint equations in omega-continuous semirings: Some ideas and many questions
16:30 17:00 Neil Immerman On size versus number of variables
17:00 18:00   Wine reception
Tuesday, 4 July
9:00 10:25 Dov Monderer Mechanism design
10:30 11:00 Krzysztof Apt Stable partitions in coalition games
11:00 11:30   Coffee
11:30 12:00 Wieslaw Zielonka From discounting to parity games
12:00 12:30 Hugo Gimbert Positional stochastic games
12:30 13:30   Lunch at Wolfson Court
14:00 14:30 Kousha Etessami Recursive concurrent stochastic games
14:30 15:00 Dietmar Berwanger Backwards induction for games of infinite horizon
15:00 15:30   Tea
15:30 16:55 Georg Gottlob Hypertree decompositions
17:00 18:00 GAMES Steering Commitee Meeting
Wednesday, 5 July
09:00 10:25 Moshe Vardi Games as an algorithmic construct
10:30 11:00 Yde Venema Coalgebra automata
11:00 11:30   Coffee
11:30 12:00 Sibylle Fröschle When is secrecy decidable?
12:00 12:15 Florian Horn Finitary parity and streett games
12:15 12:30 Slawomir Lasota Faster algorithm for bisimulation equivalence of normed context-free processes
12:30 13:30   Lunch at Wolfson Court
14:00 17:00   Excursion
Thursday, 6 July
09:00 10:25 Rajeev Alur Nested words and trees
10:30 11:00 Andrzej Murawski Game semantics and automata
11:00 11:30   Coffee
11:30 12:00 Tayssir Touili Verifying concurrent message-passing C programs with recursive calls
12:00 12:15 Kristin Rozier Algorithms for automata-theoretic linear temporal logic model checking
12:15 12:30 Deian Tabakov Experimental evaluation of complementation of non-deterministic Buechi automata
12:30 13:30   Lunch at Wolfson Court
14:00 14:30 Marcin Jurdzinski Optimality equations and strategy improvement for average payoff games
14:30 14:45 Ashutosh Trivedi A strategy improvement algorithm for optimal time reachability games
14:45 15:00 Pavel Krcal Communicating timed automata
15:00 15:30   Tea
15:30 16:00 Bengt Jonsson Proving liveness by backwards reachability
16:00 16:30 Martin Lange Model checking games for fixpoint logic with Chop
16:30 17:00 GAMES Coordinator's Report
17:00 18:00 Panel discusssion: The future of GAMES
19:30 23:00   Conference Dinner, Emmanuel College (Old Library)
Friday, 7 July
09:00 10:25 Didier Caucal Deterministic grammars
10:30 11:00 Ranko Lazic On LTL with the freeze quantifier and register automata
11:00 11:30   Coffee
11:30 12:00 Sergei Vorobyov Are one-player games always simple?
12:00 12:30 Igor Walukiewicz Tree algebras


  • Erich Grädel (Aachen)
  • Luke C.-H. Ong (Oxford)
  • Colin P. Stirling (Edinburgh)