Strategies in infinite games : structured reactive programs and transducers over infinite alphabets

• Strategien in unendlichen Spielen: Strukturierte reaktive Programme und Transducer über unendlichen Alphabeten

Brütsch, Benedikt; Thomas, Wolfgang (Thesis advisor); Markey, Nicolas (Thesis advisor); Grohe, Martin (Thesis advisor)

Aachen (2018, 2020)
Doktorarbeit

Dissertation, RWTH Aachen University, 2018

Kurzfassung

Das Thema dieser Arbeit ist die Konstruktion von Gewinnstrategien in unendlichen Spielen folgender Art: Zwei Spieler wählen abwechselnd jeweils ein Symbol aus einem gegebenen Alphabet, so dass sich eine unendliche Symbolfolge ergibt. Als Gewinnbedingung dient eine Menge L solcher Folgen - der zweite Spieler gewinnt, falls die produzierte Folge in L enthalten ist, andernfalls gewinnt der erste Spieler. Solche Spiele sind ein nützliches Modell für die Interaktion zwischen einem sogenannten reaktiven System und dessen Umgebung: Das System nimmt fortwährend Eingabesymbole entgegen und antwortet jeweils mit einem Ausgabesymbol. Eine Gewinnbedingung kann als Spezifikation für solch ein System aufgefasst werden, und eine Gewinnstrategie für das System als korrekte Implementierung. Wir untersuchen zwei Varianten von Churchs Syntheseproblem, das wie folgt formuliert werden kann: Gegeben ist eine ω-reguläre Gewinnbedingung L ⊆ Σ^ω über einem endlichen Alphabet Σ. Bestimme, welcher Spieler eine Gewinnstrategie hat, und konstruiere eine solche Strategie in Form eines endlichen Automaten. Zuerst betrachten wir eine von Madhusudan (2011) vorgeschlagene Verfeinerung: Gesucht ist hier eine Strategie in Form eines strukturierten reaktiven Programms. Madhusudans Lösung basiert auf der Konstruktion eines alternierenden Zwei-Wege-Baumautomaten, der die Programme erkennt, die Gewinnstrategien darstellen. Wir präsentieren eine direkte Konstruktion eines deterministischen Baumautomaten, der ebendiese Programme erkennt, und geben eine untere Schranke für die Größe solcher Baumautomaten an. In beiden Verfahren spielt die Anzahl der (Booleschen) Programmvariablen eine wichtige Rolle, da sie sich doppelt exponentiell auf die Laufzeit des Synthesealgorithmus auswirkt. Wir zeigen, dass für bestimmte in Linear Temporal Logic (LTL) formulierte Spezifikationen eine exponentielle Variablenanzahl nötig ist. Als zweite Variante des Syntheseproblems betrachten wir die folgende Verallgemeinerung: Die Spieler wählen nun Symbole aus einem unendlichen Alphabet der Form Σ*, für eine endlichen Menge Σ. Zur Darstellung von Gewinnbedingungen definieren wir sogenannte ℕ-Memory-Automaten über solchen Alphabeten und untersuchen deren Eigenschaften sowohl auf endlichen Wörtern also auch auf ω-Wörtern. Wir definieren ℕ-Memory-Transducer als Modell für Strategien und beweisen die algorithmische Lösbarkeit des entsprechenden Syntheseproblems: Für eine Gewinnbedingung L ⊆ (Σ*)^ω, die durch einen deterministischen ℕ-Memory-Parity-Automaten gegeben ist, können wir bestimmen, welcher Spieler eine Gewinnstrategie hat, und eine solche Strategie in Form eines ℕ-Memory-Transducers angeben.