Memory and delay in regular infinite games [Elektronische Ressource] / Michael Holtmann

Sujets

• Mathematics

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2011
• Nombre de lectures: 37
• Langue: Deutsch

Extrait

MemoryandDelayinRegularInfiniteGames
Von der Fakultät für Mathematik, Informatik und Naturwissenschaften
der RWTH Aachen University zur Erlangung des akademischen Grades
eines Doktors der Naturwissenschaften genehmigte Dissertation
vorgelegt von
Diplom-Informatiker
Michael Holtmann
aus Düsseldorf
Berichter: Universitätsprofessor Dr. Dr.h.c. Wolfgang Thomas
Universitätsprofessor Dr. Erich Grädel
Tag der mündlichen Prüfung: 9. Mai 2011
Diese Dissertation ist auf den Internetseiten der Hochschulbibliothek
online verfügbar.Zusammenfassung
Unendliche Zwei-Personen-Spiele sind ein ausdrucksstarkes und anpassungsfä-
higes Werkzeug bei der Modellierung und Verifikation reaktiver Systeme. Es ist
allgemein bekannt, dass beispielsweise die Konstruktion eines Controllers, der
beliebig lange in der Umgebung eines Systems agiert, reduziert werden kann auf
die Berechnung einer Gewinnstrategie in einem unendlichen Spiel (Pnueli und
Rosner, 1989). Für die Klasse der Spiele mit regulärer Gewinnbedingung haben
Büchi und Landweber 1969 gezeigt, dass einer der Spieler eine Gewinnstrategie
hat, die durch einen endlichen Automaten realisierbar ist. Basierend auf diesem
grundlegenden Resultat hat die Forschung viele Versuche unternommen, die Lö-
sungsverfahren für unendliche Spiele weiterzuentwickeln. Dies betrifft sowohl
den zeitlichen Aufwand, den man benötigt, um Gewinnstrategien zu berechnen,
als auch denSpeicherbedarf, um diesedann zu programmieren.In dervorliegen-
denArbeitgehteshauptsächlich umdenzweitenAspekt.EswerdenzweiProble-
me betrachtet, die im Hinblick auf die Konstruktion kleiner Controllerspezifika-
tionen von Bedeutungsind.
Im ersten Teil der Arbeit beschäftigen wir uns mit dem klassischen Problem,
endlich repräsentierbareGewinnstrategien zu berechnen, die von Automaten mit
möglichst wenig Speicher (das heißt mit möglichst wenig Zuständen) realisiert
werden können. Auch wenn ein Resultat von Dziembowski et al. aus dem Jah-
re 1997 besagt, dass es exotische reguläre Spiele gibt, für die Gewinnstrategien
nur durch Automaten implementiert werdenkönnen,die gemessenan der Größe
der Spielarena mindestens exponentiell groß sind, so erfordern die meisten prak-
tischen Beispiele doch weit weniger Speicherplatz. Wir stellen einen effizienten
Algorithmus für die Reduktion des für die Implementierung von Gewinnstrate-
gien verwendeten Speichers vor und wenden ihn auf mehrere Klassen regulärer
Bedingungenan.Außerdemzeigenwir,dassmitunseremVerfahreneinexponen-
tieller Gewinn bezüglich der Speichergröße erzielt werden kann.
Im zweiten Teil dieser Arbeit führen wir einen verallgemeinerten Begriff von
Strategien ein. Einer der Spieler darf jeden seiner Züge für eine endliche Anzahl
von Schritten hinauszögern. Mit anderen Worten, er kann bei seinen Entschei-
dungen einen Vorgriff auf die Züge des Gegners ausnutzen. Dieses Szenario lässt
sich beispielsweise in verteilten Systemen wiederfinden, zum Beispiel, wenn Puf-
ferspeicherfürdieKommunikationzwischenentferntenKomponenteneingesetzt
werden. Unser Konzept von Strategien erfasst die Klasse der stetigen Operatoren
und ist damit eine Erweiterungder Arbeit von Hosch und Landweber(1972) und
insbesondere auch der von Büchi und Landweber (1969). Wir zeigen, dass das
Problem, ob eine gegebene reguläre Spezifikation durch einen stetigen Operator
erfüllt werden kann, entscheidbar ist und dass jede solche Lösung auch auf ei-
ne mit beschränktem Vorgriff reduziert werden kann. Aus unseren Ergebnissen
leiten wir eine verallgemeinerte Determiniertheit regulärer Bedingungen ab.Abstract
Infinite two-player games constitute a powerful and flexible framework for the
design and verification of reactive systems. It is well-known that, for example,
the construction of a controller acting indefinitely within its environment can be
reduced to the computation of a winning strategy in an infinite game (Pnueli
and Rosner, 1989). For the class of regular games, Büchi and Landweber (1969)
showed that one of the players has a winning strategy which can be realized by a
finite-state automaton. Based on this fundamental result, many efforts have been
made by the research community to improve the solution methods for infinite
games. This is meant with respect to both the time needed to compute winning
strategies and the amount of space required to implement them. In the present
work we are mainly concerned with the second aspect. We study two problems
related to the construction of small controller programs.
In the first part of the thesis, we address the classical problem of computing
finite-state winning strategies which can be realized by automata with as little
memory, i.e., number of states, as possible. Even though it follows from a result
of Dziembowski et al. (1997) that there exist exotic regular games for which the
size of automata implementing winning strategies is at least exponential in the
size of the game arena, most practical cases require far less space. We propose
an efficient algorithm which reduces the memory used for the implementation of
winning strategies,forseveralclassesofregularconditions,andweshowthatour
technique can effect an exponential gain in the size of the memory.
In the second part of this thesis, we introduce a generalized notion of a strat-
egy. One of the players is allowed to delay each of his moves for a finite num-
ber of steps, or, in other words, exploit in his strategy some lookahead on the
moves of the opponent. This setting captures situations in distributed systems,
for example, when buffers are presentin communication between remotecompo-
nents. Our concept of strategiescorrespondsto the class of continuous operators,
thereby extending the work of Hosch and Landweber (1972) and, in particular,
that of Büchi and Landweber (1969). We show that the problem whether a given
regular specification is solvable by a continuous operator is decidable and that
each continuoussolution can be reducedtoone ofboundedlookahead. Fromour
results, we derive a generalized determinacy of regular conditions.Acknowledgments
I am very grateful to all the people who have contributed to the success of this
thesis, either directly or indirectly.
First and foremost, I would like to thank my supervisor Wolfgang Thomas
for giving me the opportunity to work as an academic researcher. His continu-
ing support and helpful advice have been of great value to me throughout the
past years. It was him who suggested to me to apply for the AlgoSyn Research
Training Group, where I enjoyed three years of interdisciplinary exchange.
IwouldliketothankErichGrädelforhiskindreadinesstoactasaco-examiner
of this thesis.
I would like to thank all my co-authors whom I have had the pleasure to
work with: Marcus Gelderie, Łukasz Kaiser, Christof Löding and, again, Wolf-
gang Thomas.
I would like to thank all my colleagues at I7 and MGI, especially those who
helpedmewithproofreadingafirstdraftofthisthesisandwhomademanyhelp-
ful comments on its contents: Tobias Ganzow, Marcus Gelderie, Łukasz Kaiser,
DanielNeider,BerndPuchala,RomanRabinovich,FrankRadmacherandMichaela
Slaats.
Finally, I am deeply indebted to my friends and family for their constant sup-
port throughout the past years. Especially, I would like to mention my affection-
ate girlfriend Franzi for continuing encouragement and plenty of patience she
had with me.Contents
Introduction 1
1 Preliminaries 11
1.1 Basic Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.2 Words and Formal Languages . . . . . . . . . . . . . . . . . . . . . . 11
1.3 Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.4 Infinite Games . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2 SynopsisofWinningConditions 19
2.1 Games with Positional Winning Strategies . . . . . . . . . . . . . . 20
2.2 Game Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.3 Games with Non-Positional Winning Strategies . . . . . . . . . . . 27
I Memory Reductionfor Strategies in InfiniteGames
3 An Algorithmfor Memory Reduction 41
3.1 Retrospection: Mealy Automata . . . . . . . . . . . . . . . . . . . . . 42
3.2 Reduction of Game Graphs . . . . . . . . . . . . . . . . . . . . . . . 47
3.3 Staiger-Wagner Conditions . . . . . . . . . . . . . . . . . . . . . . . 54
3.4 Request-ResponseConditions . . . . . . . . . . . . . . . . . . . . . . 61
3.5 Muller and Streett Conditions . . . . . . . . . . . . . . . . . . . . . . 66
3.6 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74
Conclusionof Part I 87
II Infinite Games with Finite Delay
4 Games with Delay 93
4.1 Delay Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
4.2 Decision Problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100
ixx Contents
5 Finite Delay in Regular Games 105
5.1 The Block Game . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
5.2 The Semigroup Game . . . . . . . . . . . . . . . . . . . . . . . . . . 109
5.3 Delay Values . . . . . . . . . . . . . . . . . . . . . . . . . . . .