Skip to content

Workshop Programme

for period 3 - 7 July 2006

Games and Verification

3 - 7 July 2006


Monday 3 July
08:30-09:00 Registration
09:00-10:25 van Benthem, J (Stanford and Amsterdam)
  Dynamic-epistemic 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:30-10:45 Kaiser, L (RWTH Aachen)
  Game quantification on automatic structures and hierarchical games Sem 1

11:00-11:30 Coffee
11:30-12:00 Duparc, J (Universite de Lausanne)
  Towards the Wadge hierarchy of weak alternating tree automata Sem 1

12:00-12:30 Obdrzalek, J (Masaryk University, Brno)
  Are parity games spineless? Sem 1

12:30-13:30 Lunch at Wolfson Court
14:00-14:30 Colcombet, T (IRISA)
  Ramseyan factorisation for trees Sem 1

14:30-14:45 Samuelides, M (Universite Denis Diderot)
  Pebble tree-walking automata Sem 1

14:45-15:00 Barany, V (RWTH Aachen)
  A hierachy of automatically presentable omega-words having a decidable MSO theory Sem 1

15:00-15:30 Tea
15:30-16:00 Janin, D (Universite Bordeaux-1)
  On distributed synthesis of discrete systems Sem 1

16:00-16:30 Esparza, J (Universitaet Stuttgart)
  Solving fixpoint equations in omega-continuous semirings: Some ideas and many questions Sem 1

16:30-17:00 Immerman, N (Massachusetts)
  On size versus number of variables Sem 1

17:00-18:00 Wine reception
Tuesday 4 July
09:00-10: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:30-11:00 Apt, K (CWI)
  Stable partitions in coalition games Sem 1

11:00-11:30 Coffee
11:30-12:00 Zielonka, W (LIAFA - Universite Paris 7)
  From discounting to parity games Sem 1

12:00-12:30 Gimbert, H (Warsaw)
  Positional stochastic games Sem 1

12:30-13:30 Lunch at Wolfson Court
14:00-14:30 Etessami, K (Edinburgh)
  Recursive concurrent stochastic games Sem 1

14:30-15:00 Berwanger, D (Universite Bordeaux-1)
  Backwards induction for games of infinite horizon Sem 1

15:00-15:30 Tea
15:30-16:55 Gottlob, G (Oxford)
  Hypertree decompositions Sem 1

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

17:00-18:00 GAMES Steering Commitee Meeting
Wednesday 5 July
09:00-10: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 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

10:30-11:00 Venema, Y (Amsterdam)
  Coalgebra automata Sem 1

11:00-11:30 Coffee
11:30-12:00 Froschle, S (Warsaw)
  When is secrecy decidable? Sem 1

12:00-12:15 Horn, F (Laboratoire d'Informatique Algorithmique)
  Finitary parity and streett games Sem 1

12:15-12:30 Lasota, S (Warsaw)
  Faster algorithm for bisimulation equivalence of normed context-free processes Sem 1

12:30-13:30 Lunch at Wolfson Court
14:00-17:00 Excursion
Thursday 6 July
09:00-10: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 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.

10:30-11:00 Murawski, A (Oxford)
  Game semantics and automata Sem 1

11:00-11:30 Coffee
11:30-12:00 Touili, T (LIAFA - Universite Paris 7)
  Verifying concurrent message-passing C programs with recursive calls Sem 1

12:00-12:15 Rozier, K (Rice)
  Algorithms for automata-theoretic linear temporal logic model checking Sem 1

12:15-12:30 Tabakov, D (Rice)
  Experimental evaluation of complementation of non-deterministic Buechi automata Sem 1

12:30-13:30 Lunch at Wolfson Court
14:00-14:30 Jurdzinski, M (Warwick)
  Optimality equations and strategy improvement for average payoff games Sem 1

14:30-14:45 Trivedi, A (Warwick)
  A strategy improvement algorithm for optimal time reachability games Sem 1

14:45-15:00 Krcal, P (Uppsala)
  Communicating timed automata Sem 1

15:00-15:30 Tea
15:30-16:00 Jonsson, B (Uppsala)
  Proving liveness by backwards reachability Sem 1

16:00-16:30 Lange, M (Munich)
  Model checking games for fixpoint logic with Chop Sem 1

16:30-17:00 GAMES Coordinator's Report
17:00-18:00 Panel discusssion: The future of GAMES
Session: Games and Verification
19:30-23:00 Conference Dinner, Emmanuel College (Old Library)
Friday 7 July
09:00-10: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 (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.

10:30-11:00 Lazic, R (Warwick)
  On LTL with the freeze quantifier and register automata Sem 1

Session: Games and Verification
11:00-11:30 Coffee
11:30-12:00 Vorobyov, S (Uppsala)
  Are one-player games always simple? Sem 1

12:00-12:30 Walukiewicz, I (Universite Bordeaux-1)
  Tree algebras Sem 1

12:30-13:30 Lunch at Wolfson Court

Back to top ∧