Controller Synthesis and Infinite Games: a short introduction
The controller synthesis problem is a generalization of the formal verification problem. Here, one considers a system $\cS with controllable inputs $V_C$, uncontrollable inputs $V_U$, and state variables $V_X$ that should satisfy a given specification $\Phi$. To this end, one has to define a controller $\cC$ to determine suitable values for the variables in $V_C$ based on the values of the variables in $V_U$ and $V_X$. Controller synthesis can be viewed as a two-player game where the environment as a player determines values for $V_U$, while the controller as its opponent determines values for $V_C$ to direct each transition to satisfy the specification. The goal of the controller is to make the choices so that the given specification holds regardless what the environment will choose. In this talk I'll give an introduction to the controller synthesis problem, outline some of the problems and present some of the solutions proposed in the literature.