skip to content
 

Timetable (LAAW06)

Games and Verification

Monday 3rd July 2006 to Friday 7th July 2006

Monday 3rd July 2006
08:30 to 09:00 Registration
09:00 to 10:25 Dynamic-epistemic logic of games

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

INI 1
10:30 to 10:45 Game quantification on automatic structures and hierarchical games
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
11:00 to 11:30 Coffee
11:30 to 12:00 Towards the Wadge hierarchy of weak alternating tree automata
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
12:00 to 12:30 Are parity games spineless?
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
12:30 to 13:30 Lunch at Wolfson Court
14:00 to 14:30 T Colcombet ([IRISA])
Ramseyan factorisation for trees
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
14:30 to 14:45 M Samuelides (Université Denis Diderot)
Pebble tree-walking automata
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
14:45 to 15:00 A hierachy of automatically presentable omega-words having a decidable MSO theory
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
15:00 to 15:30 Tea
15:30 to 16:00 On distributed synthesis of discrete systems
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
16:00 to 16:30 Solving fixpoint equations in omega-continuous semirings: Some ideas and many questions
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
16:30 to 17:00 On size versus number of variables
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
17:00 to 18:00 Wine reception
Tuesday 4th July 2006
09:00 to 10:25 Mechanism design
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.
INI 1
10:30 to 11:00 Stable partitions in coalition games
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
11:00 to 11:30 Coffee
11:30 to 12:00 From discounting to parity games
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
12:00 to 12:30 H Gimbert ([Warsaw])
Positional stochastic games
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
12:30 to 13:30 Lunch at Wolfson Court
14:00 to 14:30 Recursive concurrent stochastic games
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
14:30 to 15:00 Backwards induction for games of infinite horizon
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
15:00 to 15:30 Tea
15:30 to 16:55 Hypertree decompositions

One of the best-known methods for decomposing graphs is the method of tree-decompositions introduced by Robertson and Seymour. Many NP-hard 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 game-theoretic characterizations of hypergraph decomposition methods, and give a survey on recent results.

Related Links

INI 1
17:00 to 18:00 GAMES Steering Commitee Meeting INI 1
Wednesday 5th July 2006
09:00 to 10:25 Games as an algorithmic construct

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 complexity-theoretic settings. The focus of this talk is on presenting games and alternation as a powerful algorithmic construct. The driving examples are various automated-verification tasks, where games yield elegant and optimal algorithms.

Related Links

INI 1
10:30 to 11:00 Y Venema ([Amsterdam])
Coalgebra automata
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
11:00 to 11:30 Coffee
11:30 to 12:00 S Froschle ([Warsaw])
When is secrecy decidable?
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
12:00 to 12:15 Finitary parity and streett games
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
12:15 to 12:30 S Lasota ([Warsaw])
Faster algorithm for bisimulation equivalence of normed context-free processes
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
12:30 to 13:30 Lunch at Wolfson Court
14:00 to 17:00 Excursion
Thursday 6th July 2006
09:00 to 10:25 Nested words and trees

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 well-nested matching of entries to and exits from functions and procedures, to XML documents with the well-nested structure given by start-tags matched with end-tags. Finite-state 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 finite-state recognizability. We argue that for algorithmic linear-time verification of pushdown systems, instead of viewing the program as a context-free 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, pre-post 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 finite-state 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.

INI 1
10:30 to 11:00 Game semantics and automata
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
11:00 to 11:30 Coffee
11:30 to 12:00 Verifying concurrent message-passing C programs with recursive calls
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
12:00 to 12:15 K Rozier ([Rice])
Algorithms for automata-theoretic linear temporal logic model checking
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
12:15 to 12:30 Experimental evaluation of complementation of non-deterministic Buechi automata
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
12:30 to 13:30 Lunch at Wolfson Court
14:00 to 14:30 Optimality equations and strategy improvement for average payoff games
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
14:30 to 14:45 A Trivedi ([Warwick])
A strategy improvement algorithm for optimal time reachability games
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
14:45 to 15:00 Communicating timed automata
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
15:00 to 15:30 Tea INI 1
15:30 to 16:00 Proving liveness by backwards reachability
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
16:00 to 16:30 Model checking games for fixpoint logic with Chop
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
16:30 to 17:00 GAMES Coordinator's Report INI 1
17:00 to 18:00 Panel discusssion: The future of GAMES INI 1
19:30 to 23:00 Conference Dinner, Emmanuel College (Old Library)
Session: Games and Verification
Friday 7th July 2006
09:00 to 10:25 Deterministic grammars

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 (context-free) 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.

INI 1
10:30 to 11:00 R Lazic ([Warwick])
On LTL with the freeze quantifier and register automata
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
11:00 to 11:30 Coffee
Session: Games and Verification
11:30 to 12:00 Are one-player games always simple?
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
12:00 to 12:30 Tree algebras
http://www.games.rwth-aachen.de/History/PastEvents/cambridge06.html
INI 1
12:30 to 13:30 Lunch at Wolfson Court
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons