Arbeitsgemeinschaft Logik und Automaten

Vorträge im Sommersemester 2005

Rational Behaviour and Strategy Construction in Infinite Multiplayer Games

Di, 19.7.2005, 14:00 Uhr
Michael Ummels, RWTH Aachen


We study infinite games played by arbitrarily many players on a directed graph. Equilibrium states capture rational behaviour in these games. Besides the well-known notion of a Nash equilibrium, we deal with the less well-known notion of a subgame perfect equilibrium. We argue that the latter is more appropriate for our scenario. Our most general result is the existence of a subgame perfect equilibrium in any game where each player has a winning condition of Borel type, a generalisation of Martin's Theorem on the determinacy of two-player zero-sum Borel games. We then turn to games where the winning condition for each player is a parity condition. For parity games with a finite arena, we show the existence of a subgame perfect equilibrium in finite-state strategies. By a suitable notion of game reduction, we extend this result to games with MSO-definable winning conditions. In the last part of the talk, we turn to algorithmical questions. For games with MSO-definable winning conditions played on a finite graph, we present an algorithm for computing a subgame perfect equilibrium of a given payoff and analyse the complexity of the problem of deciding whether a game has a subgame perfect equilibrium with a payoff between two given thresholds.

Beyond parity games

Di, 28.6.2005, 14:00 Uhr
Wieslaw Zielonka, Université Paris 7


Are there games with non binary payoff pertinent to program verification? We propose one such class of games: priority mean-payoff games. This class contains as special cases mean-payoff games and parity games. We show that the priority mean-payoff games on finite arenas admit optimal positional (memoryless) strategies for both players. To this end we develop a general technique for games with arbitrary real valued payoffs allowing us a quick verification of the existence of optimal positional strategies.

As it is well-known mean-payoff games are the limit of discounted games if the discount factor tends to 1. We extend this result to priority mean-payoff games showing that they are a limit of discounted games with a non-uniform discount factor. For discount factor close to 1 the optimal strategies in this form of discounted games are also optimal for priority mean-payoff games.

Nested Pebbles Capture Transitive Closure

Do, 23.6.2005, 14:00 Uhr
Hendrik Jan Hoogeboom, Universiteit Leiden


String languages recognizable in (deterministic) log-space are characterized either by two-way (deterministic) multi-head automata, or following Immerman, by first-order logic with (deterministic) transitive closure. Here we elaborate this result, and match the number of heads to the arity of the transitive closure. More precisely, first-order logic with k-ary deterministic transitive closure has the same power as deterministic automata walking on their input with k heads, additionally using a finite set of nested pebbles. This result is valid for strings, ordered trees, and in general for families of graphs having a fixed automaton that can be used to traverse the nodes of each of the graphs in the family. Examples of such families are grids, toruses, and rectangular mazes.

The special case of k=1 for trees, shows that single-head deterministic tree-walking automata with nested pebbles are characterized by first-order logic with unary deterministic transitive closure. This refines our earlier result that placed these automata between first-order and second-order logic on trees.

Some Remarks About Active XML and Context-free Games

Di, 21.6.2005, 14:00 Uhr
Thierry Cachat, Université Paris 7


An active XML (AXML) document is a tree where some leafs are labeled by URL-names and represent calls to web services. If a web service is called, the corresponding leaf is replaced by a sub-tree, which can contain new URL-names... This can be modelled by a context-free grammar (the tree is here represented by a word).

In certain circumstances, we want the AXML document to belong to a given regular language, representing the desired format. One has to call some web services to conform the document to the requirements. This can be modeled by a two-player game between a controller and an environment. In each round, the controller selects a letter of the word, and the environment chooses a context-free rule of the grammar to rewrite the letter. The controller wins if after a finite number of round the word belong to the target language. The problem is to decide whether the controller has a winning strategy.

The aim of the talk is to consider restrictions on the strategy and the resources of the controller. This is joint work with Anca Muscholl, and this is work in progress