h1

h2

h3

h4

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

A study of pushdown games = Pushdown-Spiele



Verantwortlichkeitsangabevorgelegt von Wladimir Fridman

ImpressumAachen : Publikationsserver der RWTH Aachen University 2013

UmfangIX, 155 S. : graph. Darst.


Aachen, Techn. Hochsch., Diss., 2013

Zsfassung in dt. und engl. Sprache


Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter


Tag der mündlichen Prüfung/Habilitation
2013-01-29

Online
URN: urn:nbn:de:hbz:82-opus-44595
URL: https://publications.rwth-aachen.de/record/210437/files/4459.pdf

Einrichtungen

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

Inhaltliche Beschreibung (Schlagwörter)
Automatentheorie (Genormte SW) ; Unendliches Spiel (Genormte SW) ; Kellerautomat (Genormte SW) ; Reaktives System (Genormte SW) ; Informatik (frei) ; Controller-Synthese (frei) ; automata theory (frei) ; infinite game (frei) ; pushdown game (frei) ; controller synthesis (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Unendliche Zwei-Personen-Spiele sind von wesentlicher Bedeutung in der Informatik, denn sie stellen einen algorithmischen Rahmen für die Untersuchung von nicht-terminierenden reaktiven Systemen bereit. Üblicherweise werden unendlichen Spiele durch eine ω-Sprache spezifiziert, die alle gewinnenden Partien für einen der beiden Spieler enthält, oder durch einen Spielgraphen und eine Gewinnbedingung auf den unendlichen Pfaden durch diesen Graphen. Viele algorithmische Resultate sind bekannt für den Fall von regulären Spezifikationen und für endliche Spielgraphen mit Gewinnbedingungen wie der Muller- oder Paritätsbedingung, die reguläre Problemstellungen erfassen. Die Ergebnisse der vorliegenden Arbeit behandeln eine Klasse von nicht-regulären Spezifikationen und eine Klasse von unendlichen Spielgraphen, nämlich solche, die durch Pushdown-Automaten spezifiziert werden, d.h. wir betrachten kontextfreie Spezifikationen und Pushdown-Spielgraphen mit Muller- oder Paritätsgewinnbedingungen. Wir erweitern zahlreiche zentrale für reguläre Spiele bekannte Resultate auf die Klasse der Pushdown-Spiele. Dabei konzentrieren wir uns auf folgende vier Problemstellungen. Zunächst analysieren wir, wie das Format einer Gewinnstrategie mit dem Typ der Spezifikation zusammenhängt. Dabei stellen wir für etliche kontextfreie Fälle eine Verbindung zwischen den Formaten der Spezifikationen und den Formaten der entsprechenden Gewinnstrategien her, zeigen aber auch Fälle von kontextfreien Spielen auf, wo diese Übereinstimmung nicht gilt. Zweitens untersuchen wir Delay-Spiele mit kontextfreien Gewinnbedingungen. In einem Delay-Spiel hat einer der beiden Spieler die Möglichkeit, seine Züge für eine gewisse Zeit hinauszuzögern, damit wird eine Vorausschau auf die Züge des Gegners erzielt. Wir klären, ob der Gewinner eines deterministisch kontextfreien Delay-Spiels berechnet werden kann, und wie groß die erforderliche Vorausschau zum Gewinnen solcher Spiele ist. Drittens untersuchen wir das Synthese-Problem für verteilte Systeme, welche aus mehreren kooperierenden Komponenten bestehen, die miteinander und mit der Umgebung kommunizieren. Dabei wird die Kommunikationsstruktur durch eine Architektur spezifiziert. Es werden beide Hauptkonzepte studiert, das der globalen und das der lokalen Spezifikationen. Wir geben eine Charakterisierung der entscheidbaren Architekturen für lokale Spezifikationen an, welche regulär oder deterministisch kontextfrei sein können. Außerdem zeigen wir Unentscheidbarkeit des verteilten Synthese-Problems für globale deterministisch kontextfreie Spezifikationen. Schließlich wird das Problem behandelt, ob der Gewinner eines unendlichen Spiels bereits nach einem endlichen Partiepräfix bestimmt werden kann. Aufbauend auf den Resultaten für den Fall der endlichen Spielgraphen führen wir eine Paritätsspiele endlicher Dauer auf Pushdown-Graphen ein und zeigen ihre Vollständigkeit zum Lösen von Paritätsspielen auf Pushdown-Graphen. Dies ergibt eine neue Reduktionsmethode, mit welcher der Gewinner eines Pushdown-Spiels durch Lösen eines Erreichbarkeitsspiels auf einem endlichen Spielgraphen bestimmt werden kann.

Infinite two-player games are of interest in computer science since they provide an algorithmic framework for the study of nonterminating reactive systems. Usually, an infinite game is specified by an ω-language containing all winning plays for one of the two players or by a game graph and a winning condition on infinite paths through this graph. Many algorithmic results are known for the case of regular specifications and for finite game graphs with winning conditions like parity or Muller conditions capturing regular objectives. The present thesis offers results that also cover a class of nonregular specifications as well as a class of infinite game graphs, namely those specified by pushdown automata, i.e, we consider contextfree specifications and pushdown game graphs with parity or Muller winning conditions. We extend various central results known for regular games to the class of pushdown games. We focus on the following four questions. Firstly, we analyze how the format of a pushdown winning strategy matches the type of the pushdown game specification. Here, we establish a strong connection between the formats of specifications and formats of corresponding winning strategies for several types of contextfree games, but we also exhibit cases of contextfree games where this correspondence fails. Secondly, we investigate delay games with contextfree winning conditions. In such a game one of the players has the possibility to postpone his moves for some time, thus obtaining a lookahead on the moves of the opponent. We clarify whether the winner of a deterministic contextfree delay game can be determined effectively as well as what amount of lookahead is necessary to win such games. Thirdly, we investigate the synthesis problem for distributed systems which consist of several cooperating components communicating with each other and with the environment. A distributed system is specified by an architecture comprising the communication structure of the system. Here, we study both main concepts, that of global and that of local specifications. We offer a complete characterization of the decidable architectures for local specifications, which may be deterministic contextfree or regular. Moreover, we prove that, for global deterministic contextfree specifications, the distributed synthesis problem is undecidable. Finally, we address the problem whether the winner of an infinite game can be already determined after a finite play prefix. Extending results for the case of finite game graphs, we introduce finite-duration parity pushdown games and establish their completeness for solving parity pushdown games. This yields a new reduction method to determine the winner of a pushdown game by solving a reachability game on a finite game graph.

Fulltext:
Download fulltext PDF

Dokumenttyp
Dissertation / PhD Thesis

Format
online, print

Sprache
English

Interne Identnummern
RWTH-CONV-143589
Datensatz-ID: 210437

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-07-17, last modified 2023-10-24


Fulltext:
Download fulltext PDF
Rate this document:

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