Arbeitsgemeinschaft Logik und Automaten

Vorträge im Sommersemester 2006

Multi-parity Games

Dienstag, 16.5.2006, 12:30 Uhr
Thomas Place, ENS Cachan


We intend to study multi-parity games which are games with an arbitrary number of parity conditions. Using known results we will present the memory needed to win those games and the complexity of deciding the winner.

Undirected Reachability in Logspace (in short: L = SL)

Dienstag, 16.5.2006, 13:30 Uhr
Tobias Ganzow, RWTH Aachen


It was a long-standing open question whether the reachability problem for undirected graphs can be decided deterministically with logarithmic space requirements which was lately answered affirmatively by Omer Reingold. While the corresponding problem for directed graphs is NLogspace-complete, the undirected version was shown to be SLogspace-complete which, together with this new result, implies the collapse of SLogspace to Logspace.

We will present the influences, concepts, and techniques used in the algorithm; particularly the notion and properties of expander graphs and the so-called "zig-zag" graph product.

3rd PROCOPE Meeting Aachen–Rennes




Games with Unboundedness and Regular Conditions

Dienstag, 13.6.2006, 14:00 Uhr
Olivier Serre, LIAFA Paris


We consider infinitary two-player perfect information games defined over graphs of configurations of a pushdown automaton.We show how to solve such games when winning conditions are Boolean combinations of a Parity condition and a stack unboundedness condition. An infinite play satisfies the unboundedness condition if there is no bound on the size of the stack during the play. We show that we can reduce these games to pushdown games with a regular parity condition and deduce that the problem of deciding a winner in such games is EXPTIME-complete.

We discuss possible extensions of this result to more complicated game graphs.

This is a joint work with A.-J. Bouquet and I. Walukiewicz.

Structured strategies for games on finite graphs

Montag, 24.7.2006, 14:00 Uhr
Sunil Simon, Institute of Mathematical Sciences, Chennai, India


We consider infinite plays over finite game graphs where players have possibly overlapping objectives. Instead of considering strategies as functions that map game positions or plays to moves, we look at strategies defined by its properties. We propose a structural definition of strategies built up from atomic decisions of the form "when condition x holds play a" and where a player's strategy may depend on properties of other players' strategies. These strategies can be represented by finite state automata. In this framework, we look at the algorithmic questions of checking whether a strategy achieves a certain objective and synthesising strategies to achieve certain conditions.

We propose a simple logic to describe such structured strategies and reason about how they ensure players' objectives. We show that checking such an assertion on a game graph is decidable.

This is joint work with R. Ramanujam (IMSc).

Game Tree Logic: Reasoning about games with multiple players

Donnerstag, 17.8.2006, 14:00 Uhr
Michael Ummels, RWTH Aachen


The logic ATL^* (Alternating time temporal logic) as proposed by Alur, Henzinger, and Kupferman has become a standard specification logic for game structures. Intuitively, ATL^* is like CTL^* but with the path quantifiers E and A replaced by quantifiers parametrised by a set of players with the meaning that these players have a joint strategy to enforce a computation such that... ATL^* works fine in many situations, but properties like the Nash equilibrium condition seem not to be expressible in it. After reviewing ATL^* and its slightly more expressive companion GL, we define a new temporal logic for specifying properties of games, called GTL, in which properties like the Nash equilibrium condition can be expressed easily. We then show that GL (and with it ATL^*) is not only a fragment of GTL, but a proper one, i.e. there are properties that can be expressed in GTL but not in GL or ATL^*. Finally, we discuss the model checking complexity of GTL. An automaton-based procedure leads to a non-elementary upper bound. This is highly unsatisfactory, because model checking for GL and ATL^* is possible in double exponential time. However, when restricted to formulae of bounded length, our algorithm works in polynomial time.
Counting over Unranked Trees

Donnerstag, 24.8.2006, 13:30 Uhr
Benoit Groz, ENS Cachan


  • Definition of several types of automata counting over unranked trees, and comparizon of their expressive power.
  • Presburger and Parikh countings, global and local conditions...
  • Decidability of the usual problems for those models, emptiness problem especially.
The Tree of Knowledge in Action: Towards a Common Perspective

Dienstag, 12.9.2006, 14:15 Uhr
Eric Pacuit, Universiteit van Amsterdam