The synthesis of controllers for linear hybrid automata

We present a semi-decision procedure for synthesizing controllers for hybrid systems modeled as linear hybrid automata. The procedure is easily modified for partial observability, at the cost of completeness. The procedure has been implemented, and tested on the synthesis of controllers for various models of a steam boiler. Since the synthesis procedure may generate controllers that are Zeno, i.e. they prevent time from diverging, we provide sufficient, but not necessary, conditions on linear hybrid automata that guarantee that any synthesized controller is non-Zeno