Dagstuhl Seminar 15061
Non-Zero-Sum-Games and Control
( Feb 01 – Feb 06, 2015 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/15061
Organizers
- Krishnendu Chatterjee (IST Austria - Klosterneuburg, AT)
- Stéphane Lafortune (University of Michigan - Ann Arbor, US)
- Nicolas Markey (ENS - Cachan, FR)
- Wolfgang Thomas (RWTH Aachen, DE)
Contact
- Christina Schwarz (for administrative matters)
Non-zero-sum games with quantitative objectives constitute a field of growing attraction that is of central interest in all scenarios of computer science where multi-agent reactive systems are studied. The purpose of the seminar is to push forward and integrate the rapidly developing research on non-zero-sum games in its many facets (e.g., timed games, priced timed games, stochastic games, energy games, games with multidimensional optimization criteria, etc.), and to build bridges to related fields, in particular to control engineering.
The interactions in such games are not purely antagonistic as in two-person games but mix collaboration, hostility and optimization. Let us mention questions to be pursued in this context:
Games with quantitative objectives. A starting point is the study of mean-payoff games, a class of games that is still closely related to the classical two-player setting of parity games. The solvability of these games in polynomial time is a long-standing open problem. A great number of variants have been proposed with very interesting applications, for instance energy games that involve the objective to keep values of prefixes of plays within certain bounds; other examples are stochastic games and timed (priced) games. Many promising results have been obtained, e.g. on the computability of optimal or near-optimal strategies in such games. But often the computational complexity involved is open, as is the question how to reconcile multiple (and possibly conflicting) quantitative objectives.
Equilibria in multiplayer games. In multiplayer games, aspects of partial information (or "concurrency") enter, and "winning objectives" are replaced in terms of diverse notions of equilibria that capture an "optimal" behavior of the participating players. There is a host of open questions in this field, not only concerning the existence of equilibria, but more so the computational complexity of finding – and ensuring – such equilibria, and the choice of "good" equilibria.
Controller synthesis, supervisory control. In the field of control engineering, the work on supervisory control of discrete event systems has shifted towards problems of distributed or decentralized control, where a set of controllers cooperate as a team in order to achieve a specification (possibly in the form of a 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.
Tools for Synthesis. While tools for automatic program verification ("model-checkers") are well established both in academic research and in industry, tools supporting synthesis even in restricted scenarios are still in the beginning.
Goals of the Seminar
A first goal is the assessment of the extremely rich landscape of current work in the fields outlined above. A second goal is to work out essentials in the fields mentioned, as an attempt to shape the state-of-the-art (say in survey articles). We think of having an invited talk for each of the topics mentioned above to support this aim. The last and (maybe self-evident) goal is of course to detect problems and approaches where the represented communities from automata theory, logic, formal methods, game theory, and supervisory control can join their forces.
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.
Multi-player games
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
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.
Other domains
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.
Control engineering
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
- Nathalie Bertrand (INRIA Rennes - Bretagne Atlantique, FR) [dblp]
- Dietmar Berwanger (ENS - Cachan, FR) [dblp]
- Patricia Bouyer-Decitre (CNRS, FR) [dblp]
- Romain Brenguier (Free University of Brussels, BE) [dblp]
- Benedikt Brütsch (RWTH Aachen, DE) [dblp]
- Véronique Bruyère (University of Mons, BE) [dblp]
- Krishnendu Chatterjee (IST Austria - Klosterneuburg, AT) [dblp]
- Laurent Doyen (ENS - Cachan, FR) [dblp]
- Rüdiger Ehlers (Universität Bremen, DE) [dblp]
- John Fearnley (University of Liverpool, GB) [dblp]
- Gilles Geeraerts (Free University of Brussels, BE) [dblp]
- Hugo Gimbert (University of Bordeaux, FR) [dblp]
- Alessandro Giua (University of Aix-Marseille, FR & University of Cagliari, IT) [dblp]
- Axel Haddad (Free University of Brussels, BE) [dblp]
- Thomas Anton Henzinger (IST Austria - Klosterneuburg, AT) [dblp]
- Rasmus Ibsen-Jensen (IST Austria - Klosterneuburg, AT) [dblp]
- Barbara Jobstmann (EPFL Lausanne, CH) [dblp]
- Jan Krcal (Universität des Saarlandes, DE) [dblp]
- Jan Kretinsky (IST Austria - Klosterneuburg, AT) [dblp]
- Stéphane Lafortune (University of Michigan - Ann Arbor, US) [dblp]
- Kim Guldstrand Larsen (Aalborg University, DK) [dblp]
- Simon B. Laursen (Aalborg University, DK) [dblp]
- Christof Löding (RWTH Aachen, DE) [dblp]
- Nicolas Markey (ENS - Cachan, FR) [dblp]
- Peter Bro Miltersen (Aarhus University, DK) [dblp]
- Benjamin Monmege (Free University of Brussels, BE) [dblp]
- Necmiye Ozay (University of Michigan - Ann Arbor, US) [dblp]
- Nicolas Perrin (UPMC - Paris, FR) [dblp]
- Sophie Pinchinat (IRISA - Rennes, FR) [dblp]
- Mickael Randour (ENS - Cachan, FR) [dblp]
- Jean-Francois Raskin (Free University of Brussels, BE) [dblp]
- Dorsa Sadigh (University of California - Berkeley, US) [dblp]
- Ocan Sankur (Free University of Brussels, BE) [dblp]
- Sven Schewe (University of Liverpool, GB) [dblp]
- Anne-Kathrin Schmuck (TU Berlin, DE) [dblp]
- Armando Solar-Lezama (MIT - Cambridge, US) [dblp]
- Jiri Srba (Aalborg University, DK) [dblp]
- John G. Thistle (University of Waterloo, CA) [dblp]
- Wolfgang Thomas (RWTH Aachen, DE) [dblp]
- Ufuk Topcu (University of Pennsylvania, US) [dblp]
- Stavros Tripakis (University of California - Berkeley, US) [dblp]
- Martin Zimmermann (Universität des Saarlandes, DE) [dblp]
Classification
- verification / logic
Keywords
- Automata theory
- infinite games
- multi-player games
- non-zero-sum games
- verification
- synthesis
- discrete event systems
- control engineering
