Eingang zum Volltext

Urheberrechtshinweis / Copyright notice

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:hbz:82-opus-21296
URL: http://darwin.bth.rwth-aachen.de/opus3/volltexte/2008/2129/

Wallmeier, Nico

Strategien in unendlichen Spielen mit Liveness-Gewinnbedingungen : Syntheseverfahren, Optimierung und Implementierung

Strategies in Infinite Games with Liveness Winning Condition : Synthesis, Optimization and Implementation

pdf-Format:
Dokument 1.pdf (1.266 KB)

Kurzfassung (Deutsch)

Gegenstand dieser Arbeit sind Lösungsverfahren für unendliche Spiele und die Implementierung entsprechender Algorithmen im Rahmen einer Experimentierplattform. Der Schwerpunkt liegt auf Spielen mit Gewinnbedingungen, welche gewisse Liveness-Eigenschaften fordern. Eine für Anwendungen (etwa in der Controller-Synthese) zentrale Liveness-Eigenschaft ist die „Request-Response-Bedingung”. Sie ist eine Konjunktion von Bedingungen der folgenden Gestalt: Immer wenn ein „Request”-Zustand besucht wird, folgt irgendwann später auch der Besuch eines entsprechenden „Response”-Zustandes. Eng verwandt damit sind die sogenannten „Streett-Bedingungen”, in denen für wiederholte Besuche gewisser Zustände wiederholte Besuche anderer Zustände gefordert werden. Es werden verschiedene Lösungsverfahren für Request-Response-Spiele und Streett-Spiele vorgestellt, mit Anwendungen etwa in der Analyse von Live-Sequence-Charts. Der Hauptbeitrag besteht in einer quantitativen Analyse der Request-Response-Spiele. Ein natürlicher Ansatz zur quantitativen Abstufung von Gewinnstrategien berücksichtigt die Wartezeiten, die in einer unendlichen Partie zwischen den Besuchen von „Request”- und nachfolgenden „Response”-Zuständen verstreichen. Dazu werden verschiedene Qualitätsmaße für Partien in Request-Response-Spielen (über endlichen Spielgraphen) eingeführt und diskutiert. Für Maße, in denen die „Strafe” mehr als linear in den Wartezeiten steigt, wird eine algorithmische Berechnung optimaler Gewinnstrategien vorgestellt. Kernpunkt ist eine Reduktion auf Mean-Payoff-Spiele über endlichen Zustandsräumen, mit der zugleich gezeigt wird, dass optimale Strategien durch endliche Automaten implementierbar sind.
Die Experimentierplattform GaSt („Games, Automata & Strategies”) integriert zahlreiche Algorithmen zur Theorie der Omega-Automaten und zur Lösung unendlicher Spiele.

Kurzfassung (Englisch)

In this thesis we develop methods for the solution of infinite games and present implementations of corresponding algorithms in the framework of a platform for the experimental study of automata theoretic algorithms. Our focus is on games with winning conditions that express certain liveness properties. A central type of liveness requirement in applications (e.g., in controller synthesis) is the “request-response condition”. It has the form of a conjunction of conditions “Whenever a “request”-state is visited, sometime later a corresponding “response”-state is visited”. A closely related winning condition is the “Streett condition” in which for repeated visits of certain states the repeated visits of other states is required. We present methods for the solution of request-response games and Streett games, the latter with an application in the analysis of live-sequence-charts. The main contribution is a quantitative analysis of request-response games. We pursue a natural approach for the quantitative evaluation of winning strategies by taking into account the waiting times that elapse between visits of “request”-states and subsequent visits of “response”-states in an infinite play. We introduce and discuss several related measures of plays in request-response games (over finite game arenas). For measures that induce a “penalty” which grows more than linearly in the waiting times, we present an algorithm to compute optimal winning strategies. The core of the argument is a reduction to mean-payoff games over finite arenas; it also shows that optimal strategies are implementable by finite-state machines. The experimental platform GaSt (”Games, Automata & Strategies”) offers numerous algorithms of the theory of omega-automata and for the solution of infinite games.

SWD-Schlagwörter: Spieltheorie , Automatentheorie
Freie Schlagwörter (englisch): game theorie , automata theorie
Institut: Lehrstuhl für Informatik 7 (Logik und Theorie diskreter Systeme) [122110]
Fakultät: 01 Fakultät für Mathematik, Informatik und Naturwissenschaften
Hochschule: RWTH Aachen
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Hauptberichter: Thomas, Wolfgang (Prof. Dr. Dr. hc.)
Sprache: Deutsch
Tag der mündlichen Prüfung: 06.09.2005
Erstellungsjahr: 2005
Publikationsdatum: 11.03.2008

 Home  |   Hilfe  |   Viewer  |   Fragen und Anregungen an opus@bth.rwth-aachen.de  |  
 auskunft@bth.rwth-aachen.de  ©Hochschulbibliothek  Haftungsausschluss