Synthesis of winning strategies for interaction under partial information

• Synthese von Gewinnstrategien für Interaktion unter partieller Information

Puchala, Bernd; Grädel, Erich (Thesis advisor)

Aachen : Publikationsserver der RWTH Aachen University (2013)
Doktorarbeit

Aachen, Techn. Hochsch., Diss., 2013

Kurzfassung

Diese Arbeit befasst sich mit dem Strategie-Problem für unendliche Mehrpersonen-Spiele mit imperfekter Information und (höchstens) kontextfreien Gewinnbedingungen. Ein besonderes Augenmerk liegt auf Anwendungen in der Synthese von Controllern für nicht-terminierende reaktive Systeme. Synthese bedeutet, aus einem gegebenen formalen Modell des Systems und einer formalen Spezifikation, gewisse Controller für das System herzustellen, welche ein korrektes System garantieren. Dies steht im Kontrast zur Verifikation, welche erfolgreiche Systemläufe betrachtet, wohingegen Synthese auf Gewinnstrategien in Spielen hinausläuft. Der wesentliche Ausgangspunkt für die Theorie der Synthese ist Churchs "Circuit Synthesis Problem", welches er 1957 eingeführt hat und welches 1969 von Büchi und Landweber in seiner vollen Allgemeinheit gelöst wurde. Für die Modellierung und Lösung praktisch relevanter Szenarien ist Churchs ursprüngliches Modell allerdings häufig nicht besonders geeignet. Einerseits ist die Lösung zu aufwändig, da sie die Übersetzung von MSO-Formeln in Muller Automaten beinhaltet. Andererseits ist das Modell zu schlicht, da lediglich ein einzelner Controller vorhanden ist, der volle Information über alle Ereignisse im System hat. Darüberhinaus wird ein System angenommen, welches vollständig durch einen endlichen Automaten dargestellt werden kann. Ein weiterer großer Nachteile ist zum Beispiel die Beschränkung auf lineare Spezifikationen. Wir behandeln einige dieser Beschränkungen: Wir betrachten Systeme mit mehreren Controllern, die jeweils unterschiedliche Information sowie Kontrolle über die Ereignisse im System haben. Insbesondere haben damit die Controller partielle Information über das System. Außerdem betrachten wir kontextfreie Spezifikationen, was die Modellierung gewisser Systeme mit unendlichem Zustandsraum erlaubt. Im Allgemeinen ist die Existenz einer Gewinnstrategie in einem gegebenen unendlichen Mehrpersonen-Spiel mit imperfekter Information bereits für reguläre Spezifikationen unentscheidbar. Durch sorgfältige Anpassung gewisser Parameter lassen sich jedoch relevante (effizient) lösbare Fälle herausstellen. Am deutlichsten macht sich der Unterschied zwischen zwei und drei (oder mehr) Spielern bemerkbar und wir werden den Fall von Spielen auf endlichen Graphen mit zwei Spielern detailliert betrachten, insbesondere im Hinblick auf die strukturelle Komplexität der Spielgraphen. Wir zeigen, dass Erreichbarkeits-Spiele mit imperfekter Information auf Graphen der DAG-Weite höchstens drei EXPTIME-schwer sind. Ein relevanter Spezialfall entsteht durch die Beschränkung der partiellen Information von Spieler 1 über die Positionen des Spielgraphen. Wir beweisen, dass in diesem Fall Spiele mit zwei Spielern und observierbaren Paritäts-Bedingungen in polynomieller Zeit gelöst werden können auf Graphen mit beschränkter DAG-Weite. Hierzu definieren und analysieren wir ein neuartiges Maß für die strukturelle Komplexität gerichteter Graphen. Weitere wichtige Parameter sind die Komplexität des Informationsflusses zwischen den Controllern sowie inwieweit die Spezifikationen Fakten adressieren können, welche die Controller nicht beobachten können. Wir identifizieren eine Reihe entscheidbarer Fälle entlang dieser Art von Einschränkungen, insbesondere lokal zerlegbare Spezifikationen. Wir liefern eine vollständige Charakterisierung aller Kommunikationsgraphen für welche Synthese entscheidbar ist für lokal zerlegbare reguläre und (deterministisch-) kontextfreie Spezifikationen. Weiterhin betrachten wir Mehrpersonen-Spiele mit imperfekter Information von einem mehr epistemologischen Standpunkt, womit nicht so sehr die strategischen Möglichkeiten sondern das Wissen der Spieler in den Mittelpunkt rückt. Insbesondere werden wir demonstrieren wie die möglichen Wissenszustände der Spieler sowie deren Dynamik explizit dargestellt werden können, was eine allgemeine Methode zur Kartierung der Wissensentwicklung liefert. Für observierbare Gewinnbedingungen ist die Quotientenbildung modulo homomorphischer Äquivalenz korrekt, womit man zeigen kann, dass Spiele auf endlichen Graphen mit hierarchischer Information und observierbaren, deterministisch-kontextfreien Gewinnbedingungen entscheidbar sind.

Einrichtungen

• Fachgruppe Mathematik [110000]
• Lehr- und Forschungsgebiet Mathematische Grundlagen der Informatik (Logik und Komplexität) [117220]