Games Meeting Cambridge 2006
Announcement
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
Programme
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 |
Organisers
- Erich Grädel (Aachen)
- Luke C.-H. Ong (Oxford)
- Colin P. Stirling (Edinburgh)