Infinite regular games in the higher-order pushdown and the parametrized setting

Slaats, Michaela; Thomas, Wolfgang

doi:3927

Infinite regular games in the higher-order pushdown and the parametrized setting = Unendliche reguläre Spiele in der Higher-Order Pushdown und der parametrisierten Fassung

Slaats, Michaela

2011 & 2012

Verantwortlichkeitsangabevorgelegt von Michaela Slaats

ImpressumAachen : Publikationsserver der RWTH Aachen University 2011

UmfangVI, 141 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2011

Zsfassung in dt. und engl. Sprache. - Prüfungsjahr: 2011. - Publikationsjahr: 2012

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Thomas, Wolfgang (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2011-11-23

Online
URN: urn:nbn:de:hbz:82-opus-39273
URL: https://publications.rwth-aachen.de/record/64083/files/3927.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Unendliches Spiel (Genormte SW) ; Unendlicher Zustandsraum (Genormte SW) ; Kellerautomat (Genormte SW) ; Zählerautomat (Genormte SW) ; Informatik (frei) ; Higher-Order Pushdown automata (frei) ; caucal hierarchy (frei) ; infinite regular games (frei) ; parametrized regular games (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Pushdown-Systeme höherer Ordnung (auch Kellersysteme höherer Ordnung genannt) erweitern die Standard-Kellersysteme durch die Nutzung eines „Kellers höherer Ordnung”. Dies ist eine geschachtelte Kellerstruktur; so ist ein Level-1 Keller ein Standardkeller und ein Level-2 Keller ein Keller von Kellern. Wir untersuchen Kellersysteme höherer Ordnung im Kontext von unendlichen regulären Spielen. Im ersten Teil geben wir einen k-ExpTime Algorithmus an, um globale positionelle Gewinnstrategien für Paritätsspiele zu berechnen, die auf dem Konfigurationsgraphen eines Level-k Kellersystems gespielt werden. Damit diese Strategien in einer endlichen Weise dargestellt werden können, bedarf es einer Definition von Regularität für Mengen von Kellern höherer Ordnung, welche auf der Nutzung von bestimmten („symmetrischen”) Operationen beruht, die gebraucht werden, um einen Keller aufzubauen. Die Konstruktion der Strategien basiert auf automatentheoretischen Techniken und benutzt die Tatsache, dass die Keller höherer Ordnung, welche mit symmetrischen Operationen konstruiert werden, in Form eines Baumes dargestellt werden können. Im zweiten Teil befassen wir uns mit der Lösung von Spielen im Sinne von Gale und Stewart, bei denen die Gewinnbedingung durch eine MSO-Formel phi(P) angegeben wird, wobei P ein Parameter ist. Dieses Szenarium entspricht einem Spiel mit drei Spielern, bei dem die i-te Runde zwischen den beiden ursprünglichen Spielern dadurch erweitert wird, dass ein Bit hinzugefügt wird, welches signalisiert, ob i in P ist oder nicht. Wir betrachten den Fall, dass der Parameter durch eine deterministische Maschine, den „Parametergenerator”, erzeugt wird. Wir lösen diese parameterisierten regulären Spiele für Paramerter P, die durch zwei verschiedene Arten von Generatoren erzeugt werden, und zwar Kellerautomaten höherer Ordnung und „Kollaps”-Kellerautomaten. Im dritten Teil vergleichen wir Kellersysteme höherer Ordnung und Zählersysteme höherer Ordnung (bei diesen besteht das Kelleralphabet nur aus einem Symbol), durch Analyse der entsprechenden Sprachklassen. Beispielsweise zeigen wir, dass Level-k Kellersprachen auch Level-(k+1) Zählersprachen sind.

Higher-order pushdown systems extend the idea of pushdown systems by using a "higher-order stack" (which is a nested stack). More precisely on level 1 this is a standard stack, on level 2 it is a stack of stacks, and so on. We study the higher-order pushdown systems in the context of infinite regular games. In the first part, we present a k-ExpTime algorithm to compute global positional winning strategies for parity games which are played on the configuration graph of a level-k higher-order pushdown system. To represent those winning strategies in a finite way we use a notion of regularity for sets of higher-order stacks that relies on certain ("symmetric") operations to build higher-order stacks. The construction of the strategies is based on automata theoretic techniques and uses the fact that the higher-order stacks constructed by symmetric operations can be arranged uniquely in a tree structure. In the second part, we study the solution of games in the sense of Gale and Stewart where the winning condition is specified by an MSO-formula phi(P) with a parameter P subset of N. This corresponds to a three player game where the i-th round between the two original players is extended by the choice of the bit 1 or 0 depending on whether i is in P or not. We consider the case that the parameter can be constructed by some deterministic machine, a "parameter generator". We solve the parametrized regular games for parameters P given by two kinds of such generators, namely: higher-order pushdown automata and collapsible pushdown automata. In the third part, we study higher-order pushdown systems and higher-order counter systems (where the stack alphabet contains only one symbol), by comparing the language classes accepted by corresponding automata. For example, we show that level-k pushdown languages are level-(k+1) counter languages.

Volltext:
PDF