Conceptual game theoretic model for an example robotic lawnmower or general controller aimed at wide audience.

Nowadays, more and more aspects of our society depend on critical reactive systems, i.e., systems that  continuously interact with their uncontrollable environment. Think about control programs of power plants,  ABS for cars or airplane and railway traffic managing. Therefore, we are in dire need of systems capable of  sustaining a safe behavior despite the nefarious effects of their environment.  

Good developers know that testing do not capture the whole picture: never will it proves that no bug or  flaw is present in the considered system. So for critical systems, it is useful to apply formal verification.  That means using mathematical tools to prove that the system follows a given specification which models  desired behaviors. 

While verification applies a posteriori, checking that the formal model of a system satisfies  the needed specification, it is most of the time desirable to start from the specification and automatically  build a system from it, in such a way that desired properties are proved to be maintained in the process.  This a priori process is known as synthesis.  The mathematical framework we use is game theory. It is a wide field with extensive formal bases and applications in numerous disciplines as diverse as economics, biology, operations research and, of course, computer science. Games model interactions between cooperating and/or competiting players who play to the best of their abilities in order to satisfy individual or common objectives. While interesting works of  Borel [4] and even Cournot [12] precede them, von Neumann and Morgenstern are generally considered as  the “Founding Fathers of (Modern) Game Theory” through their 1944 book titled Theory of Games and  Economic Behavior [20].  Roughly speaking, we consider a reactive system as a player (player 1), and his uncontrollable environment  as its adversary (player 2). 

We model their interactions in a game on a graph, where vertices model states  of the system and its environment, and edges model their possible actions. Constructing a correct system  controller then means devising a strategy (i.e., a succession of choices of actions) for player 1 such that,  whatever the strategy of player 2, the outcome of the play satisfies the specification. Such game-theoretic  formulations have proved useful for synthesis [11,17,18], verification [1], refinement [15], and compatibility  checking [13] of reactive systems, as well as in analysis of emptiness of automata [19]. 

In this paper, we do not address the full theoretical deepness of such an approach but rather try to motivate and illustrate its usefulness towards an audience who may not be familiar with it. To that end,  we discuss a motivating toy example. First, we present the informal description of a reactive system and  the behavior it should enforce. Second, we show how to use the game-theoretic framework to model its  relationship with its environment and formalize the desired specification. Third, we use the sound theory  of synthesis and exhibit a suitable controller that ensures satisfaction of the specification. Our discussion is  mostly high level and intuitive.
http://arxiv.org/abs/1204.3283

Reactive computer systems bear inherent complexity due to continuous interactions with their environment. While this environment often proves to be uncontrollable, we still want to ensure that critical computer systems will not fail, no matter what they face. Examples are legion: railway traffic, power plants, plane navigation systems, etc. Formal verification of a system may ensure that it satisfies a given specification, but only applies to an already existing model of a system. In this work, we address the problem of synthesis: starting from a specification of the desired behavior, we show how to build a suitable system controller that will enforce this specification. In particular, we discuss recent developments of that approach for systems that must ensure Boolean behaviors (e.g., reachability, liveness) along with quantitative requirements over their execution (e.g., never drop out of fuel, ensure a suitable mean response time). We notably illustrate a powerful, practically useable algorithm for the automated synthesis of provably safe reactive systems.