Synthesis of winning strategies for interaction under partial information

Puchala, Bernd; Grädel, Erich

doi:4711

Synthesis of winning strategies for interaction under partial information = Synthese von Gewinnstrategien für Interaktion unter partieller Information

Puchala, Bernd (Author)

2013

Verantwortlichkeitsangabevorgelegt von Bernd Puchala

ImpressumAachen : Publikationsserver der RWTH Aachen University 2013

Umfang260 S. : graph. Darst.

Aachen, Techn. Hochsch., Diss., 2013

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Grädel, Erich (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2013-06-10

Online
URN: urn:nbn:de:hbz:82-opus-47110
URL: https://publications.rwth-aachen.de/record/230317/files/4711.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Unendliches Spiel (Genormte SW) ; Reaktives System (Genormte SW) ; Partielle Information (Genormte SW) ; Automatentheorie (Genormte SW) ; Informatik (frei) ; Controller-Synthese (frei) ; Graphkomplexität (frei) ; infinite game (frei) ; reactive system (frei) ; partial information (frei) ; automata theory (frei) ; controller synthesis (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

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.

This work adresses the strategy problem for multiplayer games with imperfect information which are of infinite duration and have (up to) contextfree winning conditions. A particular focus is on applications to synthesis of controllers for nonterminating reactive systems. Synthesis means that one tries to construct, from a formal model of the system and some formal specification, implementations for certain controllers which guarantee a correct system. This is in contrast to verification where the interactive aspect of the system is already implemented: While verification deals with successful system runs, synthesis deals with winning strategies in games. The major starting point of synthesis is Church's "Circuit Synthesis Problem" which was introduced in 1957 and has been solved in its full generality by Büchi and Landweber in 1969. However, for modelling and solving practically relevant scenarios, Church's original setting is not the ultimate deal. On the one hand, the solution is too complex, due to a translation of MSO-formulas into Muller automata. On the other hand, the scenario is too simple because we have only a single controller with full information about all the events in the system. Moreover, it assumes a system that can be completely modelled by a finite state automaton. In particular, there are no probabilistic events and no continuous components. Other major drawbacks include the restriction to linear time specifications and to systems with synchronous behavior. We tackle several of these limitations: We consider systems with multiple controllers, each of which has different information and control about the events in the system. So, in particular, the controllers have partial information about the system. Moreover, we consider contextfree specifications, which incorporates an infinite state aspect into the model. As underlying finite models we consider finite game graphs with partial information as well as distributed systems. In general, the existence of a winning strategy in a given infinite multiplayer game with imperfect information is undecidable, already for three players and regular (even safety) specifications. However, by elaborately tuning certain parameters, one can obtain interesting and relevant subcases which are decidable and, in more restricted scenarios, even tractable. The most crucial aspect is the difference between two and three (or more) players and we analyze the case of two-player games on finite game graphs in detail, especially with regard to structural complexity of the graphs. We show that reachability games with imperfect information on graphs of DAG-width at most three are EXPTIME-hard. Moreover, they are still PSPACE-hard on acyclic graphs. A natural restriction is to bound the amount of uncertainty that player 1 may have about the positions of the game graph. We prove that in this case, two-player games with observable parity conditions on graphs of bounded DAG-width are in PTIME. For this, we introduce and analyze a new concept of graph searching with multiple robbers. Other important parameters are the complexity of information flow between the controllers and the extent, to which the specification may involve facts that the controllers cannot observe. We identify several decidable subcases along this kind of restrictions, especially locally decomposable specifications which are those that can be decomposed into a collection of local specifications for the individual controllers. We provide a complete characterization of all communication graphs for which synthesis is decidable for locally decomposable regular and (deterministic) contextfree specifications and we extend the decision methods to synthesis procedures for all decidable cases. We also consider multiplayer games with imperfect information from a more epistemological viewpoint, focussing on knowledge rather than strategic powers. In particular, we show how the possible states of minds of the players and the dynamics of these states can be represented explicitly, yielding a generalized knowledge tracking method. For the special case of observable winning conditions, this construction can be soundly quotiented by homomorphic equivalence which can be used to show that the strategy problem for games on finite graphs with hierarchical partial information and observable determinsitic contextfree winning conditions is decidable.

Fulltext:
PDF