Games on pushdown graphs and extensions [Elektronische Ressource] / vorgelegt von Thierry Cachat

Thierry Cachat

Sujets

• Informatik
• Mathematics

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2003
• Nombre de lectures: 7
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Games on Pushdown Graphs and
Extensions
Von der Fakultat˜ fur˜ Mathematik, Informatik und
Naturwissenschaften der Rheinisch-Westfalischen Technischen˜
Hochschule Aachen zur Erlangung des akademischen Grades eines
Doktors der Naturwissenschaften genehmigte Dissertation
vorgelegt von
Thierry Cachat
diplom^ ¶e d’¶etudes approfondies (DEA) en informatique
aus Mont¶elimar, Dr^ ome, Frankreich
Berichter: Prof. Dr. Wolfgang Thomas
Dr. Hab. Didier Caucal
Tag der mu˜ndlichen Pru˜fung: 18. Dezember 2003
Diese Dissertation ist auf den Internetseiten der Hochschulbibliothek online
verfu˜gbar.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 flnite description
of the game, our aim is to compute the winner and a winning strategy. For flnite
graphs these problems have been solved for a long time, although some complexity
questions remain open.
We consider several classes of inflnite graphs, from transition graphs of pushdown
automata up to graphs of the Caucal hierarchy, and we investigate difierent winning
conditions: reachability, recurrence (Buchi), parity, and the a called § -condition.˜ 3
Two kinds of techniques are developed: a symbolic approach based on flnite
automata recognizing inflnite sets of conflgurations and a game simulation which
reduces a given game into a simpler one and solves it. Difierent 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 typi-
scherweise 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 Speziflkation eines Spiels ist es das Ziel, den
Gewinner und eine Gewinnstrategie zu berechnen. Fu˜r endliche Spielgraphen sind
diese Probleme seit langem gel˜ost, obwohl einige Komplexit˜atsfragen ofien bleiben.
Wir betrachten verschiedene Klassen von unendlichen Graphen, von Kellerautomaten-
Transitionsgraphen bis Graphen der Caucal-Hierarchie, und wir studieren verschie-
dene Gewinnbedingungen: Erreichbarkeits-, Rekurrenz- (Buchi-), Paritats- und eine˜ ˜
sogenannte § -Bedingung\.3"
Zwei Arten von Methoden werden entwickelt: die symbolische Methode benutzt
endliche Automaten, um unendliche Mengen von Konflgurationen zu erkennen; die
Spielreduktion wandelt ein gegebenes Spiel in einem vereinfachten um, und lost˜ es.
Verschiedene Arten von Strategien werden auch konstruiert: entweder positionell
oder mit Kellerspeicher.R¶esum¶e
Les syst?emes r¶eactifs peuvent ^etre mod¶elis¶es de fa» con naturelle par des jeux a?
deux joueurs, ou? typiquement un joueur est le contr^ oleur, et l’autre est l’environnement.
Un jeu est gagn¶e par un joueur s’il a une strat¶egie gagnante, c’est- a-dire s’il peut
¶gagner toutes les parties. Etant donn¶e la description flnie d’un jeu, notre but est de
calculer le gagnant et une strat¶egie gagnante. Pour les graphes flnis, ces probl?emes
sont r¶esolus depuis longtemps, m^eme si des questions de complexit¶e restent ouvertes.
On consid?ere difi¶erentes classes de graphes inflnis, des graphes de transition des
automates a? pile jusqu’au graphes de la hi¶erarchie de Caucal, et on ¶etudie difi¶erentes
conditions de gain : accessibilit¶e, r¶ecurrence (Buchi), parit¶e, et une condition de type˜
§ .3
Deux sortes de techniques sont d¶evelopp¶ees : l’approche symbolique, qui utilise
des automates flnis pour reconna^‡tre des ensembles inflnis de conflguration, et la jeu-
simulation, qui transforme un jeu donn¶e en un autre plus simple pour le r¶esoudre.
Difi¶erentes sortes de strat¶egies sont aussi construites : soit positionnelles, soit avec
une m¶emoire a? pile.Danksagung
Wolfgang Thomas hat mir eine Assistentenstelle und ein sehr interessantes For-
schungsthema angeboten. Er hat mir immer in kurzer Zeit tiefe Hinweise gegeben.
Die drei Jahren in Aachen waren wissenschaftlich und auch pers˜onlich besonders
interessant und angenehm.
Didier Caucal a guid¶e mes premiers pas vers la recherche, et a su m’aider a? trouver
la voie qui me convenait. Il a rapport¶e ce document en anglais, il ne l’a pas jet¶e, et
il s’est accommod¶e de ma pr¶esentation en anglais.
Alle Mitarbeiter am Lehrstuhl fu˜r Informatik VII in Aachen waren sehr nett und
haben mir oft geholfen.
Ohne Madeleine Paupard, unsere damalige Deutschlehrerin, hatte ich nicht so gerne˜
Deutsch gelernt, und Deutschland kennengelernt.
Patricia Bouyer und Tanguy Urvoy haben Teile dieser Arbeit probegelesen.
Danke auch an alle anderen, die mir in dieser Zeit geholfen haben.Contents
1 Introduction 1
2 Framework 9
2.1 Deflnitions of Games, Winning Conditions, Strategies . . . . . . . . . 9
2.1.1 Basic Notations, Automata . . . . . . . . . . . . . . . . . . . 9
2.1.2 Game Graph . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
2.1.3 Winning Conditions . . . . . . . . . . . . . . . . . . . . . . . 10
2.1.4 Strategies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
2.2 Motivations and Algorithmic Problems . . . . . . . . . . . . . . . . . 12
2.2.1 Algorithmic Issues . . . . . . . . . . . . . . . . . . . . . . . . 12
2.2.2 Application to the Veriflcation of Reactive Systems . . . . . . 13
2.2.3 Pushdown Game System . . . . . . . . . . . . . . . . . . . . . 13
2.3 Logics and Decidability . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.3.1 The „-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.3.2 Monadic Second Order Logic . . . . . . . . . . . . . . . . . . 15
2.3.3 Syntax of MSO . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.3.4 MSO Deflnability of Winning Strategies . . . . . . . . . . . . 17
2.3.5 Discussion and Extensions . . . . . . . . . . . . . . . . . . . . 19
2.4 Limitations to Solutions of Games . . . . . . . . . . . . . . . . . . . . 19
2.4.1 Intersection of Context-Free Languages . . . . . . . . . . . . . 20
2.4.2 Other Graphs . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.4.3 A Recursive Game Graph . . . . . . . . . . . . . . . . . . . . 21
3 Symbolic Presentation of Winning Strategies 23
3.0.4 Technical Preliminaries, P-Automata . . . . . . . . . . . . . 23
3.1 Reachability Game: Computing the Attractor . . . . . . . . . . . . . 25
3.1.1 Reachability . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.1.2 Determining Membership in the Attractor . . . . . . . . . . . 30
viiviii CONTENTS
3.2 Winning Strategy for Player 0 . . . . . . . . . . . . . . . . . . . . . . 31
3.2.1 Preparation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.2.2 Positional Min-rank Strategy . . . . . . . . . . . . . . . . . . 32
3.2.3 Proof of Lemma 3.2.5 . . . . . . . . . . . . . . . . . . . . . . . 35
3.2.4 Pushdown Strategy . . . . . . . . . . . . . . . . . . . . . . . . 40
3.2.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
3.3 Back to the Basic Example of Chapter 1 . . . . . . . . . . . . . . . . 42
3.4 Buchi Condition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44˜
j
3.4.1 Computation of Bu˜chi for all j > 0 . . . . . . . . . . . . . . . 470
3.4.2 Computation of Bu˜chi Using an Acceleration . . . . . . . . . 500
3.4.3 Simple Example . . . . . . . . . . . . . . . . . . . . . . . . . . 55
3.4.4 Example of convergence to the flxed-point . . . . . . . . . . . 57
3.5 Safety Game and Co-Bu˜chi Game . . . . . . . . . . . . . . . . . . . . 59
3.6 A § Winning Condition . . . . . . . . . . . . . . . . . . . . . . . . . 623
3.6.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
3.6.2 Outline of the Solution . . . . . . . . . . . . . . . . . . . . . . 64
3.6.3 Details . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
3.7 Discussion, Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
3.7.1 Firstle . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
3.7.2 Second Example . . . . . . . . . . . . . . . . . . . . . . . . . 78
3.8 Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82
3.8.1 Modifying the Winning Condition . . . . . . . . . . . . . . . . 82
3.8.2 Preflx-recognizable Graphs . . . . . . . . . . . . . . . . . . . . 83
4 Game-Reduction and Parity Games over PDGS 87
4.1 Deflnition of the Game Simulation . . . . . . . . . . . . . . . . . . . . 88
4.2 Pushdown Games and Walukiewicz’s Results . . . . . . . . . . . . . . 88
4.3 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
4.4 Extension to a Uniform Solution . . . . . . . . . . . . . . . . . . . . . 97
4.5 Parity Games on Preflx-Recognizable Graphs . . . . . . . . . . . . . . 98
4.5.1 Reduction to Parity Game on Pushdown Graph . . . . . . . . 99
5 Parity Games over Caucal Graphs 103
5.1 The Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
5.1.1 Higher Order Pushdown Game System . . . . . . . . . . . . . 104
5.1.2 Caucal Hierarchy . . . . . . . . . . . . . . .