Strategiesynthese für Paritätsspiele auf endlichen Graphen

Vöge, Jens; Thomas, Wolfgang

doi:HT013047428

Strategiesynthese für Paritätsspiele auf endlichen Graphen

Vöge, Jens (Author)

2000 & 2001

Verantwortlichkeitsangabevorgelegt von Jens Vöge

ImpressumAachen : Publikationsserver der RWTH Aachen University 2000

Umfang131 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2000

Prüfungsjahr: 2000. - Publikationsjahr: 2001

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Thomas, Wolfgang (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2000-12-18

Online
URN: urn:nbn:de:hbz:82-opus-1282
URL: https://publications.rwth-aachen.de/record/56433/files/01_040.pdf

Einrichtungen

Fakultät für Mathematik, Informatik und Naturwissenschaften (100000)

Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei) ; Unendliches Spiel (frei) ; Zweipersonenspiel (frei) ; Endlicher Graph (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Paritätsspiele sind unendliche Zwei-Personen-Spiele, hier betrachtet auf endlichen Graphen. Eine Partie ist ein unendlicher Pfad durch den Graphen, der von den beiden Spielern durch wechselseitige Wahl von Knoten aufgebaut wird. Der Gewinner der Partie ist durch die in ihr unendlich oft auftretenden Knoten festgelegt. Das Problem der Lösung von Paritätsspielen (d.h. die Bestimmung des Gewinners für Partien von einem gegebenen Anfangsknoten aus sowie einer Gewinnstrategie) gehört zur Komplexitätsklasse NP Schnittmenge co-NP. Es ist eines der Kernprobleme der Theorie der Programmverifikation, denn viele Model-Checking-Probleme lassen sich in Polynomzeit auf die Lösung von Paritätsspielen reduzieren. In der vorliegenden Arbeit wird ein neuer Algorithmus zur Lösung von Paritätsspielen vorgestellt. Im Gegensatz zu den bisherigen diskreten Verfahren folgt er einem Ansatz der Strategieverbesserung, wie er bereits für stochastische Spiele bekannt ist. Anders als für die Verfahren der Literatur ist noch kein Beispiel bekannt, welches eine exponentielle Laufzeit belegen würde. Der Algorithmus basiert auf einer neuartigen Bewertung unendlicher Partien.

Parity games are infinite two person games, here considered on finite graphs. A play is an infinite path in the graph, whose vertices are chosen by the two players in alternation. The winner of the play is determined by the vertices that are visited infinitely often in the play. The problem of solving a parity game (i.e., finding the winner for plays starting in a given vertex and the construction of a winning strategy) belongs to the complexity class NP intersection co-NP. It is one of the core problems in the theory of program verification, because many model checking problems can be reduced to solving parity games by a polynomial time reduction. In this thesis a new algorithm for solving parity games is presented. Contrary to known discrete procedures this one uses the method of strategy improvement as it is already known from stochastic games. Unlike for procedures in the literature, no example is known for the present algorithm which requires polynomial time. The algorithm is based on a new kind of valuation for infinite plays.

Fulltext:
PDF
(additional files)