An Isaac Newton Institute Workshop

Games and Verification

Annual Workshop of the Research Training Network

Games and Automata for Synthesis and Validation

3 - 7 July 2006

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

Programme | Participants | Photograph

Theme of Conference:

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 Abstract
  • Johan van Bentham (U. of Amsterdam) - Dynamic-Epistemic Logic of Games Abstract
  • Didier Caucal (IRISA-CNRS) - Deterministic grammars Abstract
  • Georg Gottlob (U. of Oxford) - Hypertree decompositions Abstract
  • Dov Monderer (Technion) - Mechanism design Abstract
  • Moshe Vardi (Rice U) - Games as an algorithmic construct Abstract

Location and Cost:

The workshop will take place at the Newton Institute where limited accommodation is available. Three packages are available:

  • £340 (single study bedroom with shared bathroom at Wolfson Court, lunch on the days that lectures take place, formal dinner and refreshments from Sunday 2 July to Friday 7 July 2006)

  • £180 (lunches on days that lectures take place, formal dinner and refreshments)

  • £55 (registration fee, no meals)

Please indicate on the application form which package you require.

A list of local Guest Houses are available here

Application Forms:

Are available here. Invited participants to the semester long programme whose dates coincide with those of the workshop need not apply or pay any registration fee.

Closing Date:

The closing date for the receipt of applications is 31 March 2006

Local Information

Local Information


Logic and Algorithms | Workshops | Newton Institute Home Page