h1

h2

h3

h4

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

Random games = Randomisierte Spiele



Verantwortlichkeitsangabevorgelegt von Florian Horn

ImpressumAachen : Publikationsserver der RWTH Aachen University 2008

Umfang137 S. : graph. Darst.


Aachen, Techn. Hochsch., Diss., 2008


Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter


Tag der mündlichen Prüfung/Habilitation
2008-10-28

Online
URN: urn:nbn:de:hbz:82-opus-29712
URL: https://publications.rwth-aachen.de/record/51451/files/Horn_Christian.pdf

Einrichtungen

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

Inhaltliche Beschreibung (Schlagwörter)
Verifikation (Genormte SW) ; Logiksynthese (Genormte SW) ; Kombinatorisches Spiel (Genormte SW) ; Stochastisches Spiel (Genormte SW) ; Randomisierung (Genormte SW) ; Informatik (frei) ; verification (frei) ; controller synthesis (frei) ; graph games (frei) ; stochastic games (frei) ; randomised control (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
ccs: G.3 * G.2.2 * D.2.4

Kurzfassung
Spiele bilden einen klassischen Rahmen für Synthese von Controllern in reaktiven Systemen. In diesem Kontext ist ein Spiel definiert durch folgende Komponenten: eine Arena, d.h. ein Graph zur Modellierung des Systems und seiner Dynamik, und eine Gewinnbedingung zur Wiedergabe der Spezifikation, welche der Controller garantieren muss. In jedem Zustand (Knoten) wird eine Transition (Kante) gewählt, und zwar entweder durch den Conroller ("Eva"), durch die nicht-kooperative Umgebung ("Adam") oder durch eine Wahl nach einer Wahrscheinlichkeitsverteilung ("Random"). Dieser Vorgang wird unendlich oft wiederholt, wodurch eine unendliche Partie entsteht, deren Gewinner durch die Gewinnbedingung bestimmt wird. Erster Gegestand unserer Untersuchungen ist der grundlegende Fall der Erreichbarkeitsspiele. Wir entwickeln einen algorithmischen Ansatz zur Berechnung der Werte solcher Spiele, der auf den Permutationen der Zufallszustände beruht. Die Berechnungskomplexität des entstehenden "Permutations-Algorithmus" is orthogonal zum Fall der klassischen Strategie-basierten Algorithmen: Die Komplexität ist exponentiell in der Anzahl der Zufallszustände, jedoch nicht in der Anzahl der anderen Zustände. Wir entwickeln eine heuristische Verbesserung des Algorithmus, der auch auf der Idee des Algorithmus der Strategie-Verbesserung beruht. Weiterhin betrachten wir die allgemeine Klasse der Präfix-unabhängigen Spiele. Wir beweisen die Existenz optimaler Strategien für derartige Spiele. Wir zeigen auch, wie der Permutationsalgorithmus zu einem "Meta-Algorithmus" erweitert werden kann, so dass aus einem qualitativen Algorithmus ein quantitativer Algorithmus entsteht. Weiterhin studieren wir die Komplexität optimaler Strategienin Muller-Spielen, insbesondere hinsichtlich der Einsparung von Speicherbedarf bei Verwendung randomisierter Strategien. Mit Hilfe der Struktur des Zielonka-Baumes zeigen wir scharfe Schranken für den Speicherbedarf für randomisierte optimale Strategien in Spielen mit Muller-Gewinnbedingung. Wir entwickeln auch einen Polynomzeit-Algorithmus für die Bestimmung des Gewinners in Muller-Spielen mit expliziter Darstellung der Muller-Gewinnbedingung. Mit Ergebnissen der vorangehenden Abschnitte ergeben sich unmittelbar NP- bzw. co-NP-Algorithmen für die Bestimmung der Werte. Zum Schluss betrachten wir finitäre Versionen von Paritäts- und Streett-Spielen, wobei die regulären Gewinnbedingungen durch universelle Schranken für die Verzögerung ergänzt sind. Wir entwickeln einen Polynomzeit-Algorithmus für die Bestimmung des Gewinners in finitären Paritätsspielen. Für finitäre Streett-Spiele erhalten wir durch eine Reduktion auf Request-Response-Spiele einen EXPTIME-Algorithmus für die qualitative Lösung, und wir zeigen, dass das Problem PSPACE-schwer ist.

Games are a classical tool for the synthesis of controllers in reactive systems. In this setting, a game is defined by: an arena, which is a graph modelling the system and its evolution; and a winning condition, which models the specification that the controller must ensure. In each state, the outgoing transition is chosen either by the controller (Eve), an hostile environment (Adam), or a stochastic law (Random). This process is repeated for an infinite number of times, generating an infinite play whose winner depends on the winning condition. Our first object of study is the fundamental case of reachability games. We present a new effective approach to the computation of the values, based on permutations of random states. In terms of complexity, the resulting "permutation algorithm" is orthogonal to the classical, strategy-based algorithms: it is exponential in the number of random states, but not in the number of controlled states. We also present an improvement heuristic for this algorithm, inspired by the "strategy improvement" algorithm. We turn next to the very general class of prefix-independent games. We prove the existence of optimal strategies in these games. We also show that our permutation algorithm can be extended into a "meta-algorithm", turning any qualitative algorithm into a quantitative algorithm. We study then the complexity of optimal strategies for Muller games, focusing on the amount of memory that can be saved through the use of randomised strategies. Using the Zielonka tree, we show tight bounds on the necessary and sufficient memory needed to define randomised optimal strategies for any given Muller condition. We also propose a polynomial algorithm for the winner problem in explicit Muller games. The results of the former chapter yield immediately NP and co-NP algorithms for the values problem. Lastly, we consider the finitary versions of parity and Streett games, where the regular conditions are supplemented by universal bounds on delays. We propose a polynomial algorithm for the winner problem on finitary parity games. For finitary Streett games, a reduction to Request-Response games provides an EXPTIME algorithm for qualitative problems, and we show that the problem is PSPACE-hard.

Fulltext:
Download fulltext PDF

Dokumenttyp
Dissertation / PhD Thesis

Format
online, print

Sprache
English

Interne Identnummern
RWTH-CONV-113742
Datensatz-ID: 51451

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)