Games on Pushdown Graphs and Extensions
I have done my PhD Thesis under supervision of
Prof. Dr. Wolfgang Thomas
at the University of Aachen (RWTH Aachen).
You can download here the complete
PDF-file (1 Mb) or
PS-file (2 Mb) or
PS.GZ-file (0.5 Mb).
BiBTeX file with ABSTRACTS
official page.
Abstract:
Two player games are a standard model of reactive computation, where e.g. one
player is the controller and the other is the environment. A game is won by a
player if she has a winning strategy, i.e., if she can win every play. Given a
finite description of the game, our aim is to compute the winner and a winning
strategy. For finite graphs these problems have been solved for a long time,
although some complexity questions remain open.
We consider several classes of infinite graphs, from transition graphs of
pushdown automata up to graphs of the Caucal hierarchy, and we investigate
different winning conditions: reachability, recurrence (Büchi), parity, and
a Sigma_3-condition.
Two kinds of techniques are developed: a symbolic approach based on finite
automata recognizing infinite sets of configurations and a game simulation
which reduces a given game into a simpler one and solves it. Different kinds
of strategies are also constructed: either positional or based on pushdown
stack memories.
Zusammenfassung:
Reaktive Systeme werden oft durch Spiele mit zwei Personen modelliert, wo
typischerweise ein Spieler der Steuerungsprogramm ist, und der andere die
Umgebung. Ein Spieler gewinnt ein Spiel, wenn er eine Gewinnstrategie hat, so
dass er alle Partien gewinnt. Gegeben die endliche Spezifikation eines Spiels
ist es das Ziel, den Gewinner und eine Gewinnstrategie zu berechnen. Für
endliche Spielgraphen sind diese Probleme seit langem gelöst, obwohl einige
Komplexitätsfragen offen bleiben.
Wir betrachten verschiedene Klassen von unendlichen Graphen, von
Kellerautomaten-Transitionsgraphen bis Graphen der Caucal-Hierarchie, und wir
studieren verschiedene Gewinnbedingungen: Erreichbarkeits-, Rekurrenz- (Büchi-),
Paritäts- und eine sogenannte Sigma_3-Bedingung.
Zwei Arten von Methoden werden entwickelt: die symbolische Methode benutzt
endliche Automaten, um unendliche Mengen von Konfigurationen zu erkennen;
die Spielreduktion wandelt ein gegebenes Spiel in einem vereinfachten um, und
löst es. Verschiedene Arten von Strategien werden auch konstruiert: entweder
positionell oder mit Kellerspeicher.
Résumé :
On considère des jeux à deux joueurs sur des familles de graphes
infinis avec différentes conditions de gain. Notre but est de déterminer le
gagnant et de calculer une stratégie gagnante.
Dans le cas des graphes de
transition des automates à pile, on donne une méthode symbolique basée sur la
construction d'automates finis pour résoudre les jeux d'accessibilité, de
récurrence (Büchi), et les jeux avec une condition Sigma_3. Avec cette méthode
on construit un automate alternant qui reconnaît l'ensemble des configurations
gagnantes d'un jeu : les configurations depuis lesquelles le joueur 0 dispose
d'une stratégie gagnante. Cet automate permet aussi de calculer deux types de
stratégies gagnantes : positionnelles ou à pile.
D'un autre côté les méthodes de << réduction >> existantes
ont été étendues d'abord aux jeux de parité sur les graphes préfixes
reconnaissables
puis aux graphes des automates à pile de pile et aux graphes de la
hiérarchie définie par Caucal.
Ces méthodes consistent, pour résoudre un jeu, à le simuler par un autre jeu
plus petit ou plus simple, que l'on sait déjà résoudre.
Cela a permis aussi d'obtenir une
meilleure complexité pour la procédure de décision de la logique monadique du
second ordre sur ces graphes.
On peut trouver aussi une version
française de ma thèse, mais elle n'est pas à jour.
Thierry Cachat
Last modified: Mon Apr 3 16:10:50 CEST 2006
