Controller synthesis for hybrid systems with a lower bound on event separation

A systematic procedure for synthesizing all full-state feedback controllers for a hybrid system subject to a safety (state-invariance) specification has been proposed in the literature. The interaction between the controller and a non-deterministic hybrid plant is viewed as a two-person game. The controller wins if it keeps the state of the closed-loop system within a specified set of good states; its adversarial environment tries to force the system outside the good set. The synthesis procedure iteratively augments the set of states from which the environment wins via either one additional discrete step, or one additional continuous flow. The key difficulty in carrying out the synthesis procedure lies in the computations for continuous flows. One must essentially solve a differential game in which the environment is trying to drive the system into its target set at the same time as avoiding the target set of the controller. In this paper, we study hybrid systems with lower bounds on the separation between occurrence times of consecutive discrete moves. These systems arise when modelling minimal delay times between events, either in the controller, or in the environment. For such systems, we provide techniques for solving the differential games in reduced state spaces. The main idea is to discretize information about whether discrete moves are enabled or not. We demonstrate our technique by successfully synthesizing the maximal set of controllers for a hybrid model of a heating system with discrete controls and disturbances and continuous controls and disturbances.