Strategy machines : representation and complexity of strategies in infinite games

Gelderie, Marcus; Thomas, Wolfgang

doi:33597

Strategy machines : representation and complexity of strategies in infinite games = Strategy Machines : Darstellung und Komplexität von Strategien in Unendlichen Spielen

Gelderie, Marcus (Author)

2014

Verantwortlichkeitsangabevorgelegt von Marcus Gelderie

ImpressumAachen 2014

UmfangII, 195 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2014

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Thomas, Wolfgang (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2014-02-06

Online
URN: urn:nbn:de:hbz:82-opus-50253
URL: https://publications.rwth-aachen.de/record/229827/files/5025.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Model Checking (Genormte SW) ; Logiksynthese (Genormte SW) ; Automatentheorie (Genormte SW) ; Mathematische Logik (Genormte SW) ; Unendliches Spiel (Genormte SW) ; Informatik (frei) ; Unendliche Spiele (frei) ; Infinite Games (frei)

Thematische Einordnung (Klassifikation)
DDC: 004
ccs: F.4.1

Kurzfassung
In dieser Arbeit untersuchen wir die Darstellung von Gewinnstrategien in unendlichen Spielen durch Turingmaschinen. Wir zeigen, dass solche Repräsentationen eine feinere Klassifizierung von Strategien erlauben, ein besseres Verständnis der Struktur von Strategien ermöglichen und in traditionell schwierigen Gebieten angewendet werden können, z.B. in der Komposition von Spielen und Strategien. Wir geben eine formale Definition von strategy machines, einem Repräsentationsformalismus, auf Turingmaschinen basiert. Wir adaptieren die klassischen Komplexitätsmaße von Turingmaschinen an unser Gebiet. Diese heißen, Latenzzeit, Speicherverbauch und Größe. Die Latenzzeit ist die Anzahl an Schritten, die benötigt wird um den nächsten Zug zu berechnen. Der Speicherverbrauch bemisst, wie viel Speicherplatz hierfür nötig ist. Zuletzt ist die Größe gerade die Anzahl an Kontrollzuständen der Maschine. Diese Maße, welche in automatenbasierten Modellen nicht existieren, erlauben eine feinere Klassifizierung als vorhandene Modelle. Wir zeigen, dass strategy machine von polynomieller Größe und polynomiellem Platzverbauch für Muller-Spiele synthetisiert werde können. Im Fall von Streett-Spielen kann darüber hinaus sogar eine polynomialle Latenzzeit garantiert werden. Der Synthesealgorithmus ist eine Anpassung von Zielonkas Konstruktion, welche es ermöglicht kostspielige Berechnungen über den Lauf der Partie zu verteilen. Um uns der Komposition von Spielen und Strategien zuzuwenden, betrachten wir Erreichbarkeits- und Büchi-Spiele auf Produkten mehrerer Komponentenarenas. Wir betrachen hier speziell die Komponierbarkeit einer Geweinnstrategie aus einer Zahl von Gewinnstrategien aus Spielen, die auf den Komponenten gespielt werden. Wir definieren Strategiekomposition durch Subroutinen und zeigen, dass eine polynomiell große Komposition mit polynomieller Laufzeit in Polynomzeit berechnet werden kann, wenn die Komponenten nicht kommunizieren. Ist Kommunikation erlaubt, gilt ein entsprechendes Theorem genau dann, wenn Pspace = Exptime. Zuletzt betrachten wir Mean-Payoff Paritätsspiele und Mean-Penalty Paritätsspiele. Wir zeigen, dass optimale und epsilon-optimale Strategien in Mean-Payoff Paritätsspielen eine homogene Struktur haben und aus einer linearen Zahl positionaler Strategien zusammengesetzt werden können. Damit konstruieren wir eine strategy machine Darstellung polynomieller Größe von optimalen und epsilon-optimalen Strategien. Bei epsilon-optimalen Strategien ist außerdem die Latenzzeit polynomiell. Diese Schranke ist optimal. Wir übertragen das Resultat auf Mean-Penalty Paritätsspiele. Hierzu definieren wir permissive stragegy machines und transferieren Strategien vermöge einer Reduktion, die einen Strategietransfer mit automatenbasierten Strategien unmöglich macht. Dies demonstriert wiederum den Nutzen von strategy machines.

This thesis studies the representation of winning strategies in infinite games as Turing machines. We show that Turing-machine-based strategy representation (by "strategy machines") - if compared to the standard setting of Mealy automata - allows for a finer classification of strategies, provides a better understanding of the structure of strategies, and can successfully be used in areas that are difficult to reason about with automaton strategies, such as composition of games and strategies. We give a formal definition of strategy machines and adapt the classical Turing-machine complexity measures to our setting - called latency, space requirement, and size. The latency is the number of computation steps that is required to produce a next move, the space requirement states how much memory is required for this computation and the size is the number of control states of the machine. These complexity measures are not present in representations of strategies that are based on automata and thus provide a finer view on strategies than currently used models. We show that strategy machines of polynomial size with a polynomial space requirement can be synthesized for Muller games. Moreover, we show that for Streett games a polynomial latency can be guaranteed in addition to these bounds. The synthesis procedure is an adaption of Zielonka's algorithm, now making use of the computational power of a Turing machine to spread costly computations across the infinite play. Turning to composition of games and strategies, we study reachability and Büchi games on arenas that are products of several component arenas. We focus on composing a winning strategy on the product arena from winning strategies in suitably chosen games on the components. We define strategy composition based on subroutine calls and show that as long as the component arenas cannot communicate, a composition of polynomial size and latency can be computed in polynomial time. If components may communicate, a similar composition result exists iff Pspace = Exptime. Finally, we study mean-payoff parity and mean-penalty parity games as examples of quantitative games. We prove that optimal and epsilon-optimal strategies in mean-payoff parity games have a very homogeneous structure and can can be composed of a linear number of positional strategies. Using this, we derive a strategy machine implementation of polynomial size of optimal and epsilon-optimal strategies. For epsilon-optimal strategies, the latency is moreover logarithmic in epsilon. This bound is optimal. We lift this result to mean-penalty parity games. For this we introduce permissive strategy machines and translate strategies via a reduction that does not allow for the transfer of automaton strategies. This again demonstrates the usefulness of Turing machine representations of strategies.

Fulltext:
PDF