01. – 06. Februar 2015, Dagstuhl Seminar 15061
Non-Zero-Sum-Games and Control
1 / 3 >
Auskunft zu diesem Dagstuhl Seminar erteilt
Games played on graphs provide the framework to study a wide range of problems that are central in computer science, for example, reactive synthesis, well-formedness of systems, checking compatibility of behavorial type systems, etc. The traditional study of games has been for two-player zero-sum perfect-information deterministic games with Boolean objectives (where a win of one player coincides with a loss by the other player). Fundamental results of this theory are contributions of automata theory that go back to the 1960’s (Büchi, McNaughton, Rabin).
Significant progress has been achieved in the last few decades both in terms of theoretical results (understanding the complexity of such games, developing efficient algorithms) as well as their practical applicability (in reactive synthesis and controller synthesis). The current research directions explore several important extensions of the traditional study, namely, multi-player games, games with partial-observation, quantitative aspects in games, as well as application of game results in other domains. In this regard, the connection to control theory is important: The methodology of ``supervisory control'' has developed in parallel to the emergence of the game-theoretic approach, and a joint and integrating view of these closely related branches of research seemed overdue.
The Dagstuhl Seminar "Non-Zero Sum Games and Control" addressed these developments, with a particular emphasis on the connections to control theory. The response to the call for participation was very positive, and the 42 scientists joining the seminar represented the full range of topics mentioned above. There was a very good mixture between young and "established" researchers, and the participation of female researchers (making a quarter) was high (in the context of computer science). In order to support the understanding between the different research branches, it was decided to have on each half-day at least one survey talk, outlining a field and describing general challenges; some of these talks were contributed by young researchers. The speakers of the survey talks were Rüdiger Ehlers, Tom Henzinger, Barbara Jobstmann, Stéphane Lafortune, Kim Larsen, Peter Bro Miltersen, Jean-Francois Raskin, Armando Solar-Lezama, John Thistle, and Ufuk Topcu. Furthermore, a special evening session was organized on challenges in supervisory control. Besides the aim of joining and integrating different tracks of research in the area, an important objective of the seminar was to bring together (at least some) members of two large research communities in the area, namely the community of automata, logic, and games in Europe and the U.S. research network EXCAPE (Expeditions in Computer Augmented Program Engineering).
During the seminar, several small circles of participants started or continued joint work. As a general result of the seminar, confirmed by many positive and even enthusiastic comments of participants after the seminar, one may say that a much better understanding and appreciation between the various research branches was established. As one of the participants put it, the seminar was "eye-opening".
As an overview of the areas covered in the talks, we give a short description of the topics studied in the seminar.
The study of multi-player games is an important extension of the two-player setting. In terms of theoretical study it gives rise to a rich class of questions related to different notions of equilibria, studying computability and complexity results for them, as well as different logics to express them. In terms of practical applicability, various notions of synthesis such as rational synthesis, secure equilibria, assume-guarantee synthesis, assume-admissible synthesis, etc. have been developed to apply the results of multi-player games for synthesis of component-based systems.
Partial-observation games extend perfect-information games where players do not have perfect knowledge about the game. This is particularly relevant in control theory, where the controller does not have access to private variables of the plant. The results of partial-observation games have been recently extended to the stochastic setting, as well as for finite-memory strategies, leading to a new framework which can potentially solve interesting applications from the control domain.
Quantitative game models
These are a prominent class of game models for applications to verification and synthesis. In particular, taking real-time constraints into account is especially important for such applications. Timed automata and timed games have already played an important role, as they are a convenient and expressive model enjoying efficient algorithms. Statistical model checking in particular offers a very effective technique for strategy optimization. Robustness analysis of timed models makes the verification process even more faithful.
- Weighted timed games extend timed games with the ability of modeling other quantitative aspects of cyber-physical systems. While the expressive power is greatly improved, the verification and synthesis problems get much more complex than for plain timed automata. Still, algorithms sometimes exist for approximating the optimal cost, which in most practical situations is sufficient.
- Timed automata have now reached maturity. Powerful data-structures and efficient symbolic algorithms have been designed to develop efficient algorithms. Statistical model checking is now also used in tools for efficiently optimizing strategies. These tools can now be applied on real-life scenarios, e.g. in home automation and motion planning.
- Probabilistic models form another important class of models of particular interest for representing and reasoning about e.g. systems involving stochastic behaviors. Efficient algorithms have recently been developed for diagnosing probabilistic automata, or for synthesizing strategies that guarantee good performance level with sufficient probability in Markov Decision Processes.
In the quantitative setting, the range of objectives is large; there are mean-payoff objectives, energy objectives, mean-payoff of energy objectives, their Boolean combinations, and combinations of quantitative (e.g., stochastic) semantics with adversarial semantics.
Theoretical results developed for games have been generalized to problems in other settings as well. A prime example is that the lower bound for strategy improvement algorithms for parity games was modified to obtain lower bounds for linear-programming solutions, and recent results show that exploiting structures of Markov decision processes it can be established that several classical rules for linear-programming algorithms solve PSPACE-complete problems.
In the field of control engineering, research on supervisory control of discrete event systems and on formal methods in feedback control has recently emphasized distributed and decentralized control architectures that more accurately capture the physical constraints arising in cyber-physical and networked control systems. In these architectures, a set of controllers, possibly with different run-time information about the system, cooperate as a team in order to achieve a specification (either qualitative or quantitative objective) on the entire system behavior, in the presence of a reactive environment. For instance, costly sensors and actuators, as well as costly communication, lead to challenging synthesis problems, both conceptually (e.g., characterization of the information structure) and computationally (e.g., distributed synthesis of the controllers). Another important consideration is to ensure robustness of the synthesized implementation with respect to classes of disturbances on the controlled system.
Researchers are still trying to establish the precise boundary between decidable and undecidable problems in this research domain. It is known that synthesis for both safety and a form of liveness termed non-blockingness, well-understood in a centralized-information setting, becomes undecidable in a decentralized-information setting. But the decidability of special classes of this problem is still an open issue. Establishing concrete bridges between the theory of partial-observation games and such decentralized/distributed control problems for discrete abstractions of cyber-physical systems is an important research issue, both in terms of answering open undecidability questions and in terms of developing efficient synthesis procedures for decidable problems. Similarly, problems of intrusion by malicious agents into control architectures (e.g., taking over actuators or sensors) also lead to new classes of problems where the theory of games with quantitative objectives can be leveraged.
Recently-developed synthesis techniques for "correct-by-construction" controllers in engineering systems have exploited game formulations between the set of controllers on the one hand and the system/environment on the other hand. Related approaches have considered synthesis of the "complete" controller implementation from a "partial" implementation and a sample set of desired behaviors in the reactive environment under consideration.
Creative Commons BY 3.0 Unported license
Krishnendu Chatterjee, Stéphane Lafortune, Nicolas Markey, and Wolfgang Thomas
- Verification / Logic
- Automata theory
- Infinite games
- Multi-player games
- Non-zero-sum games
- Discrete event systems
- Control engineering