Modeling: Controller Synthesis

While verification is concerned with proving that a system is correct with respect to all external disturbances, synthesis attempts to mechanize the choice between design options for the system in order to produce a system which is provably correct with respect to all disturbances. Clearly this problem is more difficult than verification although the underlying algorithmic principles are similar. The first step in formulating a design problem as controller synthesis is to identify the various “players” in the game, that is the components of the system and classify them as controller (the part that we want to design), and environment (the thing that we do not control and that our designed system has to cope with). In the context of scheduling and resource allocation problems, the controller will be a scheduler which makes decisions concerning resource allocation at certain situations while the environment consists of tasks or jobs that may arrive according to some under-specified constraints and terminate after some under-specified duration. In other contexts the environment actions may include certain faults and the controller role is to guarantee correctness and some acceptable performance albeit those faults. After composing the model of the controller and its environment we obtain a transition system with two types of transitions, controllable (those of the controller) and uncontrollable (those of the environment). These objects are also known as game graphs, AND-OR graphs, alternating automata, etc. Algorithm