Synthesis of winning strategies for interaction under partial information

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