Automatic synthesis of switching controllers for linear hybrid systems: Safety control

In this paper we study the problem of automatically generating switching controllers for the class of Linear Hybrid Automata, with respect to safety objectives. While the same problem has been already considered in the literature, no sound and complete solution has been provided so far. We identify and solve inaccuracies contained in previous characterizations of the problem, providing a sound and complete symbolic fixpoint procedure to compute the set of states from which a controller can keep the system in a given set of desired states. While the overall procedure may not terminate, we prove the termination of each iteration, thus paving the way to an effective implementation.