Games and verification

Workshop theme

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

Applications for this workshop are now closed

Timetable

Monday 3rd July 2006
08:30 to 09:00	Registration	No Room Required
09:00 to 10:25	Johan van Benthem University of Helsinki Dynamic-epistemic logic of games	Room 1
10:30 to 10:45	Lukasz Kaiser RWTH Aachen University Game quantification on automatic structures and hierarchical games	Room 1
11:00 to 11:30	Coffee	No Room Required
11:30 to 12:00	Jacques Duparc Université de Lausanne Towards the Wadge hierarchy of weak alternating tree automata	Room 1
12:00 to 12:30	Jan Obdrzalek Are parity games spineless?	Room 1
12:30 to 13:30	Lunch at Wolfson Court	No Room Required
14:00 to 14:30	Thomas Colcombet Ramseyan factorisation for trees	Room 1
14:30 to 14:45	Mathias Samuelides Université Denis Diderot Pebble tree-walking automata	Room 1
14:45 to 15:00	Vince Barany RWTH Aachen University A hierachy of automatically presentable omega-words having a decidable MSO theory	Room 1
15:00 to 15:30	Tea	No Room Required
15:30 to 16:00	David Janin On distributed synthesis of discrete systems	Room 1
16:00 to 16:30	Javier Esparza Universität Stuttgart Solving fixpoint equations in omega-continuous semirings: Some ideas and many questions	Room 1
16:30 to 17:00	Neil Immerman University of Massachusetts On size versus number of variables	Room 1
17:00 to 18:00	Wine reception	No Room Required

Tuesday 4th July 2006
09:00 to 10:25	Dov Monderer Technion - Israel Institute of Technology Mechanism design	Room 1
10:30 to 11:00	Krzysztof Apt Centrum voor Wiskunde en Informatica (CWI) Stable partitions in coalition games	Room 1
11:00 to 11:30	Coffee	No Room Required
11:30 to 12:00	Wieslaw Zielonka From discounting to parity games	Room 1
12:00 to 12:30	Hugo Gimbert Positional stochastic games	Room 1
12:30 to 13:30	Lunch at Wolfson Court	No Room Required
14:00 to 14:30	Kousha Etessami University of Edinburgh Recursive concurrent stochastic games	Room 1
14:30 to 15:00	Dietmar Berwanger Université Bordeaux 1 Backwards induction for games of infinite horizon	Room 1
15:00 to 15:30	Tea	No Room Required
15:30 to 16:55	Georg Gottlob University of Oxford Hypertree decompositions	Room 1
17:00 to 18:00	GAMES Steering Commitee Meeting	Room 1

Wednesday 5th July 2006
09:00 to 10:25	Moshe Vardi Rice University Games as an algorithmic construct	Room 1
10:30 to 11:00	Yde Venema University of Helsinki Coalgebra automata	Room 1
11:00 to 11:30	Coffee	No Room Required
11:30 to 12:00	Sibylle Fröschle When is secrecy decidable?	Room 1
12:00 to 12:15	Florian Horn Finitary parity and streett games	Room 1
12:15 to 12:30	Slawomir Lasota Faster algorithm for bisimulation equivalence of normed context-free processes	Room 1
12:30 to 13:30	Lunch at Wolfson Court	No Room Required
14:00 to 17:00	Excursion	No Room Required

Thursday 6th July 2006
09:00 to 10:25	Rajeev Alur University of Pennsylvania Nested words and trees	Room 1
10:30 to 11:00	Andrzej Murawski University of Oxford Game semantics and automata	Room 1
11:00 to 11:30	Coffee	No Room Required
11:30 to 12:00	Tayssir Touili Verifying concurrent message-passing C programs with recursive calls	Room 1
12:00 to 12:15	Kristin Rozier Rice University Algorithms for automata-theoretic linear temporal logic model checking	Room 1
12:15 to 12:30	Deian Tabakov Rice University Experimental evaluation of complementation of non-deterministic Buechi automata	Room 1
12:30 to 13:30	Lunch at Wolfson Court	No Room Required
14:00 to 14:30	Marcin Jurdzinski University of Warwick Optimality equations and strategy improvement for average payoff games	Room 1
14:30 to 14:45	Ashutosh Trivedi University of Warwick A strategy improvement algorithm for optimal time reachability games	Room 1
14:45 to 15:00	Pavel Krcal Communicating timed automata	Room 1
15:00 to 15:30	Tea	Room 1
15:30 to 16:00	Bengt Jonsson Proving liveness by backwards reachability	Room 1
16:00 to 16:30	Martin Lange Model checking games for fixpoint logic with Chop	Room 1
16:30 to 17:00	GAMES Coordinator's Report	Room 1
17:00 to 18:00	Panel discusssion: The future of GAMES	Room 1
19:30 to 23:00	Conference Dinner, Emmanuel College (Old Library)	No Room Required

Friday 7th July 2006
09:00 to 10:25	Didier Caucal Deterministic grammars	Room 1
10:30 to 11:00	Ranko Lazic University of Warwick On LTL with the freeze quantifier and register automata	Room 1
11:00 to 11:30	Coffee	No Room Required
11:30 to 12:00	Sergei Vorobyov Are one-player games always simple?	Room 1
12:00 to 12:30	Igor Walukiewicz Tree algebras	Room 1
12:30 to 13:30	Lunch at Wolfson Court	No Room Required

Speakers

Rajeev Alur University of Pennsylvania
Krzysztof Apt Centrum voor Wiskunde en Informatica (CWI)
Vince Barany RWTH Aachen University
Dietmar Berwanger Université Bordeaux 1
Didier Caucal
Thomas Colcombet
Jacques Duparc Université de Lausanne
Javier Esparza Universität Stuttgart
Kousha Etessami University of Edinburgh
Sibylle Fröschle
Hugo Gimbert
Georg Gottlob University of Oxford
Florian Horn
Neil Immerman University of Massachusetts
David Janin
Bengt Jonsson
Marcin Jurdzinski University of Warwick
Lukasz Kaiser RWTH Aachen University
Pavel Krcal
Martin Lange
Slawomir Lasota
Ranko Lazic University of Warwick
Dov Monderer Technion - Israel Institute of Technology
Andrzej Murawski University of Oxford
Jan Obdrzalek
Kristin Rozier Rice University
Mathias Samuelides Université Denis Diderot
Deian Tabakov Rice University
Tayssir Touili
Ashutosh Trivedi University of Warwick
Johan van Benthem University of Helsinki
Moshe Vardi Rice University
Yde Venema University of Helsinki
Sergei Vorobyov
Igor Walukiewicz
Wieslaw Zielonka

Show All

Workshop theme

Invited Tutorials:

Applications for this workshop are now closed

Timetable

Speakers

Supported By

Register for updates