h1

h2

h3

h4

h5
h6
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png

Solving infinite games with bounds = Unendliche Spiele mit Schranken



Verantwortlichkeitsangabevorgelegt von Martin Zimmermann

ImpressumAachen : Publikationsserver der RWTH Aachen University 2012

UmfangIX, 185 S. : graph. Darst.


Aachen, Techn. Hochsch., Diss., 2012

Zsfassung in dt. und engl. Sprache


Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter


Tag der mündlichen Prüfung/Habilitation
2012-02-27

Online
URN: urn:nbn:de:hbz:82-opus-39864
URL: https://publications.rwth-aachen.de/record/64089/files/3986.pdf

Einrichtungen

  1. Lehrstuhl für Informatik 7 (Logik und Theorie diskreter Systeme) (122110)
  2. Fachgruppe Informatik (120000)

Inhaltliche Beschreibung (Schlagwörter)
Theoretische Informatik (Genormte SW) ; Verifikation (Genormte SW) ; Mathematische Logik (Genormte SW) ; Synthese (Genormte SW) ; Informatik (frei) ; unendliche Spiele (frei) ; lineare temporale Logik (frei) ; theoretical computer science (frei) ; verification (frei) ; synthesis (frei) ; infinite games (frei) ; linear temporal logic (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Wir untersuchen die Existenz von optimalen Strategien in unendlichen Spielen auf Graphen, sowie die Komplexität die nötig ist, um diese zu berechnen und zu implementieren. Parametrisierte lineare temporale Logiken sind Erweiterungen von „Linear Temporal Logic” (LTL) mit temporalen Operatoren, die mit variablen Zeitschranken versehen werden können. Solche Logiken wurden als „PLTL” von Alur et al. und als „PROMPT-LTL” von Kupferman et al. für das Model-Checking entwickelt. Wir zeigen, dass in doppelt-exponentieller Laufzeit entschieden werden kann, ob ein Spieler ein Spiel mit PLTL-Gewinnbedingung bezüglich mindestens einer, unendlich vieler, oder aller Variablenbelegungen gewinnt. Diese Probleme sind also nicht schwerer als das Lösen von LTL-Spielen. Weiterhin stellen wir einen Algorithmus mit dreifach-exponentieller Laufzeit vor, der optimale Variablenbelegungen bestimmt, bezüglich derer ein Spieler gewinnt. Schließlich zeigen wir doppelt-exponentielle obere und untere Schranken für die Werte von optimalen Variablenbelegungen. In Muller-Spielen messen wir die Qualität einer Gewinnstrategie mit McNaughtons Score-Werten. Wir konstruieren Gewinnstrategien, die alle Score-Werte des verlierenden Spielers mit zwei beschränken und zeigen, dass der Wert zwei optimal ist. Damit verringern wir die bisher beste obere Schranke n! in einem Muller-Spiel mit n Knoten von McNaughton. Unter Benutzung dieser Strategien zeigen wir, wie aus einen Muller-Spiel ein Safetyspiel konstruiert werden kann, dessen Lösung es ermöglicht, beide Gewinnregionen und eine Gewinnstrategie für einen Spieler im ursprünglichen Muller-Spiel zu bestimmen. Dadurch erhalten wir eine neue Antiketten-basierte Speicherstruktur und die erste Definition von permissiven Strategien für Muller-Spiele. Zusätzlich verallgemeinern wir diese Konstruktion, indem wir einen neuen Begriff einer Spielreduktion von beliebigen Spielen auf Safety-Spiele einführen, und zeigen, dass dieser auf viele andere Gewinnbedingungen anwendbar ist.

We investigate the existence and the complexity of computing and implementing optimal winning strategies for graph games of infinite duration. Parameterized linear temporal logics are extensions of Linear Temporal Logic (LTL) by temporal operators equipped with variables for time bounds. In model-checking, such specifications were introduced as "PLTL" by Alur et al. and as PROMPT-LTL by Kupferman et al. We show how to determine in doubly-exponential time, whether a player wins a game with PLTL winning condition with respect to some, infinitely many, or all variable valuations. Hence, these problems are not harder than solving LTL games. Furthermore, we present an algorithm with triply-exponential running time to determine optimal variable valuations that allow a player to win a game. Finally, we give doubly-exponential upper and lower bounds on the values of optimal variable valuations. In Muller games, we measure the quality of a winning strategy using McNaughton's scoring functions. We construct winning strategies that bound the losing player's scores by two and show this to be optimal. This improves the previous best upper bound of n! in a game with n vertices, obtained by McNaughton. Using these strategies, we show how to transform a Muller game into a safety game whose solution allows to determine the winning regions of the Muller game and to compute a finite-state winning strategy for one player. This yields a novel antichain-based memory structure and the first definition of permissive strategies for Muller games. Moreover, we generalize our construction by presenting a new type of game reduction from infinite games to safety games and show its applicability to several other winning conditions.

Fulltext:
Download fulltext PDF

Dokumenttyp
Dissertation / PhD Thesis

Format
online, print

Sprache
English

Interne Identnummern
RWTH-CONV-125444
Datensatz-ID: 64089

Beteiligte Länder
Germany

 GO


OpenAccess

QR Code for this record

The record appears in these collections:
Document types > Theses > Ph.D. Theses
Faculty of Mathematics, Computer Science and Natural Sciences (Fac.1) > Department of Computer Science
Publication server / Open Access
Public records
Publications database
120000
122110

 Record created 2013-01-28, last modified 2023-10-24


Fulltext:
Download fulltext PDF
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)