skip to content

Games and Verification

3rd July 2006 to 7th July 2006

Organisers: E Graedel (Aachen), C-H L Ong (Oxford) and CP Stirling (Edinburgh)

Annual Workshop of the Research Training Network Games and Automata for Synthesis and Validation

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.

The conference is also the final annual meeting of GAMES, a research training network funded by the European Community under the Fifth Framework Programme.

Invited Tutorials:

  • Rajeev Alur (U. of Pennsylvania) - Pushdown games
  • Johan van Bentham (U. of Amsterdam) - Dynamic-Epistemic Logic of Games
  • Didier Caucal (IRISA-CNRS) - Deterministic grammars
  • Georg Gottlob (U. of Oxford) - Hypertree decompositions
  • Dov Monderer (Technion) - Mechanism design
  • Moshe Vardi (Rice U) - Games as an algorithmic construct
University of Cambridge Research Councils UK
    Clay Mathematics Institute The Leverhulme Trust London Mathematical Society Microsoft Research NM Rothschild and Sons