Workshop Programme
for period 3  7 July 2006
Games and Verification
3  7 July 2006
Timetable
Monday 3 July  
08:3009:00  Registration  
09:0010:25  van Benthem, J (Stanford and Amsterdam)  
Dynamicepistemic logic of games  Sem 1  
Games involve actions, knowledge, beliefs, strategies, preferences, and all of these can change interactively as moves are being played. We will show how such phenomena can be modeled in current dynamic logics of information update, belief change, and preference upgrade. This perspective sits at the interface of philosophical logic, computational logic, and game theory. We give some illustrations to communication, and solution procedures for games, and we mention a number of open problems in the area, both conceptual and technical. Related Links


10:3010:45  Kaiser, L (RWTH Aachen)  
Game quantification on automatic structures and hierarchical games  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

11:0011:30  Coffee  
11:3012:00  Duparc, J (Universite de Lausanne)  
Towards the Wadge hierarchy of weak alternating tree automata  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

12:0012:30  Obdrzalek, J (Masaryk University, Brno)  
Are parity games spineless?  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

12:3013:30  Lunch at Wolfson Court  
14:0014:30  Colcombet, T (IRISA)  
Ramseyan factorisation for trees  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

14:3014:45  Samuelides, M (Universite Denis Diderot)  
Pebble treewalking automata  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

14:4515:00  Barany, V (RWTH Aachen)  
A hierachy of automatically presentable omegawords having a decidable MSO theory  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

15:0015:30  Tea  
15:3016:00  Janin, D (Universite Bordeaux1)  
On distributed synthesis of discrete systems  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

16:0016:30  Esparza, J (Universitaet Stuttgart)  
Solving fixpoint equations in omegacontinuous semirings: Some ideas and many questions  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

16:3017:00  Immerman, N (Massachusetts)  
On size versus number of variables  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

17:0018:00  Wine reception 
Tuesday 4 July  
09:0010:25  Monderer, D (Technion)  
Mechanism design  Sem 1  
The field of economic mechanism design has been an active area of research in economics for many years. Recently many researchers in computer Science and Artificial Intelligence have been contributed to this area. This field uses tools of game theory to design rules of interaction for economic transactions that will yield some desired outcome such as maximizing social welfare or maximizing revenue. In this short tutorial I provide an overview of this subject for an audience with a limited knowledge of game theory. 

10:3011:00  Apt, K (CWI)  
Stable partitions in coalition games  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

11:0011:30  Coffee  
11:3012:00  Zielonka, W (LIAFA  Universite Paris 7)  
From discounting to parity games  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

12:0012:30  Gimbert, H (Warsaw)  
Positional stochastic games  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

12:3013:30  Lunch at Wolfson Court  
14:0014:30  Etessami, K (Edinburgh)  
Recursive concurrent stochastic games  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

14:3015:00  Berwanger, D (Universite Bordeaux1)  
Backwards induction for games of infinite horizon  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

15:0015:30  Tea  
15:3016:55  Gottlob, G (Oxford)  
Hypertree decompositions  Sem 1  
One of the bestknown methods for decomposing graphs is the method of treedecompositions introduced by Robertson and Seymour. Many NPhard problems become polynomially soblvable if restricted to instances whose underlying graph structure has bounded treewidth. The notion of treewidth can be straightforwardly extended to hypergraphs by simply considering the treewidth of their primal graphs or, alteratively, of their incidence graphs. However, doing so comes along with a loss of information on the structure of a hypergraph with the effect that many polynomially solvable problems cannot be recognized as such because the treewidth of the underlying hypergraphs is unbounded. In particular, the treewidth of the class of acyclic hypergraphs is unbounded. In this talk, I will describe more appropriate measures for hypergraph acyclicity, and, in particular, the method of hypertree decompositions and the associated concept of hypertree width. After giving general results on hypertree decompositions, I will report on gametheoretic characterizations of hypergraph decomposition methods, and give a survey on recent results. Related Links


17:0018:00  GAMES Steering Commitee Meeting 
Wednesday 5 July  
09:0010:25  Vardi, M (Rice)  
Games as an algorithmic construct  Sem 1  
Games were introduced into complexity theory by Chandra, Kozen, and Stockmeyer (JACM, 198), through the concept of alternation, which generalizes nondeterminism. The standard use of alternation is in complexitytheoretic settings. The focus of this talk is on presenting games and alternation as a powerful algorithmic construct. The driving examples are various automatedverification tasks, where games yield elegant and optimal algorithms. Related Links


10:3011:00  Venema, Y (Amsterdam)  
Coalgebra automata  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

11:0011:30  Coffee  
11:3012:00  Froschle, S (Warsaw)  
When is secrecy decidable?  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

12:0012:15  Horn, F (Laboratoire d'Informatique Algorithmique)  
Finitary parity and streett games  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

12:1512:30  Lasota, S (Warsaw)  
Faster algorithm for bisimulation equivalence of normed contextfree processes  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

12:3013:30  Lunch at Wolfson Court  
14:0017:00  Excursion 
Thursday 6 July  
09:0010:25  Alur, R (Pennsylvania)  
Nested words and trees  Sem 1  
This talk is centered around our recent model of nested words as a representation of data with both a linear ordering and a hierarchically nested matching of items. Such dual structure occurs in diverse corners of computer science ranging from executions of structured programs where there is a natural wellnested matching of entries to and exits from functions and procedures, to XML documents with the wellnested structure given by starttags matched with endtags. Finitestate acceptors for nested words define the class of regular languages of nested words that has all the appealing theoretical properties that the class of classical regular word languages enjoys: deterministic nested word automata are as expressive as their nondeterministic counterparts; the class is closed under union, intersection, complementation, concatenation, and Kleene*; membership, emptiness, language inclusion, and language equivalence are all decidable; and definability in monadic second order logic corresponds exactly to finitestate recognizability. We argue that for algorithmic lineartime verification of pushdown systems, instead of viewing the program as a contextfree language over words, one should view it as a regular language of nested words, and this would allow model checking of many properties (such as stack inspection, prepost conditions) that are not expressible in existing specification logics. We also discuss nested trees that are obtained adding nesting edges along paths of trees, and finitestate acceptors over nested trees. This leads to a very expressive fixpoint logic (equivalently, alteranting parity nested tree automata) with a decidable model checking problem for pushdown systems. 

10:3011:00  Murawski, A (Oxford)  
Game semantics and automata  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

11:0011:30  Coffee  
11:3012:00  Touili, T (LIAFA  Universite Paris 7)  
Verifying concurrent messagepassing C programs with recursive calls  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

12:0012:15  Rozier, K (Rice)  
Algorithms for automatatheoretic linear temporal logic model checking  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

12:1512:30  Tabakov, D (Rice)  
Experimental evaluation of complementation of nondeterministic Buechi automata  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

12:3013:30  Lunch at Wolfson Court  
14:0014:30  Jurdzinski, M (Warwick)  
Optimality equations and strategy improvement for average payoff games  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

14:3014:45  Trivedi, A (Warwick)  
A strategy improvement algorithm for optimal time reachability games  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

14:4515:00  Krcal, P (Uppsala)  
Communicating timed automata  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

15:0015:30  Tea  
15:3016:00  Jonsson, B (Uppsala)  
Proving liveness by backwards reachability  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

16:0016:30  Lange, M (Munich)  
Model checking games for fixpoint logic with Chop  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

16:3017:00  GAMES Coordinator's Report  
17:0018:00  Panel discusssion: The future of GAMES  
Session: Games and Verification  
19:3023:00  Conference Dinner, Emmanuel College (Old Library)  
Friday 7 July  
09:0010:25  Caucal, D (IRISA  CNRS)  
Deterministic grammars  Sem 1  
We purpose a survey on various deterministic grammars (alphabetic systems) used to define infinite words, terms, trees and graphs. The deterministic grammars over words are the morphisms which are used to generate the morphic words. The labelled deterministic grammars over words coincide with the simple (contextfree) grammars or the monadic recursive schemes, and can be used to produce simple infinite trees and graphs. The deterministic grammars over terms are the recursive program schemes, and define the algebraic terms. The deterministic grammars over typed terms are used to generate a hierarchy of infinite terms and can be used to generate a hierarchy of higher order morphic words. The deterministic grammars over (finite) graphs generate the transition graphs of pushdown automata. We will present these grammars with general known results. Then we will give new results with open questions and possible extensions. 

10:3011:00  Lazic, R (Warwick)  
On LTL with the freeze quantifier and register automata  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

Session: Games and Verification  
11:0011:30  Coffee  
11:3012:00  Vorobyov, S (Uppsala)  
Are oneplayer games always simple?  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

12:0012:30  Walukiewicz, I (Universite Bordeaux1)  
Tree algebras  Sem 1  
http://www.games.rwthaachen.de/History/PastEvents/cambridge06.html 

12:3013:30  Lunch at Wolfson Court 