Einführung in die mathematische Theorie und algorithmischen Resultate über Graph-Spiele, Graph-Spiele als Grundlage von Formale Methoden, Einsatz von Graph-Spielen in AI.
Spiele über Graphen sind eine nützliche mathematische Modellierung von vielen Phänomenen in der Informatik, die eine Interaktion zwischen Spielern/Agenten/Komponenten beinhalten. Ein Spiel zu lösen bedeutet zu entscheiden, ob ein Spieler eine Gewinnstragie hat. Es gibt einige Klassen von Spielen deren Komplexität in der Schnittmenge von NP und co-NP liegt, aber für die nicht bekannt ist ob die Komplexität auch in P liegt, wie zum Beispiel parity games, mean-payoff games, discounted payoff games, simple stochastic games. Dieses Jahr gab es einen Durchbruch in der Analyse von parity games, einer täuschend einfachen Klasse von Spielen mit engen Verbindungen zu tiefen Resultaten in Logik und Automatentheorie. Ein Team aus Neuseeland und Singapure [Calude et. al. 2017] hat einen Quasipolynomialzeit-Algorithmus für das Lösen von parity games veröffentlicht --- frühere Algorithmen waren knapp unter Exponentialzeit.
Ich werde einen Streifzug durch die Theorie von Spielen über Graphen präsentieren und dabei die Determiniertheit von Spielen, den zum Gewinnen benötigten Speicher und die Komplexität von Spielen behandeln.
Ich starte mit grundlegenden Arbeiten und ende mit neuen Resultaten.
Ich werde Material aus folgenden Artikeln verwenden:
- Ehrenfeucht and Mycielski (1979). Positional strategies for mean payoff games
- McNaughton (1993). Infinite games played on finite graphs.
- Zwick and Paterson (1995). The complexity of mean payoff games.
- Dziembowski, Jurdzinski, and Walukiewicz (1997). How much memory is needed to win infinite games?
- Zielonka (1998). Infinite games on finitely coloured graphs with applications to automata on infinite trees.
- Voge and Jurdzinski (2000). A discrete strategy improvement algorithm for solving parity games.
- Chatterjee, Henzinger, and Jurdzinski (2005). Mean-payoff parity games.
- Schewe (2007). Solving Parity Games in Big Steps.
- Jurdzinski, Paterson, and Zwick (2008). A deterministic subexponential algorithm for solving parity games.
- Friedmann (2009). An exponential lower bound for the parity game strategy improvement algorithm as we know it.
- Benerecetti, Dell'Erba and Mogavero (2016). Solving parity games via priority promotion
- Aminof and Rubin (2016). First Cycle Games.
- Calude, Jain, Khoussainov, Li, and Stephan (2017). Deciding parity games in quasipolynomial time.
- Jurdzinski and Lazic (2017). Succinct progress measures for solving parity games.
ECTS breakdown:
25h Vorlesung
25h Lesen und Diskussion der vom Vortragenden besprochenen Artikel
25h Vorbereiten und Halten der Abschlusspräsentation
Schedule: 8 Vorlesungen zu je 2 Stunden
Der Kurs wird geblockt abgehalten im Zeitraum vom 20.11.-1.12. . Die Präsentationen der Kursteilnehmer finden an einem noch zu bestimmenden Datum in der Woche vom 4.12.-8.12. statt.
Für ECTS Punkte geben die Kursteilnehmer einen Vortrag über einen klassischen oder neuen Artikel. Es gibt hierfür eine Auswahl aus unterschiedlichen Themen: die enge Verbindung zwischen Graph-Spielen und Automatentheorie und Logik, der Einsatz von Spielen in Formalen Methoden (modeling, verification, synthesis, testing, composition, simulation), den Einsatz von Graph-Spielen in AI (automated planning, verification in robotics, general-game playing) oder Erweiterungen des Basismodells (multiplayer games, partial-information games, stochastic games, pushdown games, timed games).
