Abstract:
A controller for a non-deterministic hybrid plant must ensure that the closed-loop system meets some requirement, regardless of what the plant does. When the plant is viewed as an adversary, controller synthesis becomes the task of solving a two-person game to find the system configurations from which the controller wins. For hybrid systems, the moves of each player can be either discrete or continuous. Thus winning strategies can involve a non-trivial mix of continuous and discrete actions, and are in general not easy to find. Fortunately, there is a systematic procedure to find all winning strategies in the case of safety properties (Tomlin, Lygeros, & Sastry 1998; Lygeros, Tomlin, & Sastry 1999). To assess the applicability of the procedure, we study a hybrid model of a heating system. The system incorporates both discrete controls and disturbances, and continuous controls and disturbances. For this system, we detail how to compute the set of winning configurations, using a combination of case analysis in the discrete domain and solving min-max problems in the continuous domain. The steps of the synthesis procedure for our case study have been implemented in Matlab, enabling us to experiment with different parameter settings. We also discuss preliminary lessons learned from this case study, and suggest areas for future research that will enable the synthesis procedure to be more applicable in practice. Lygeros, J.; Tomlin, C.; and Sastry, S. 1999. Controllers for reachability specifications for hybrid systems. Automatica 35(3). To appear. Tomlin, C.; Lygeros, J.; and Sastry, S. 1998. Synthesizing controllers for nonlinear hybrid systems. In Henzinger, T., and Sastry, S., eds., Hybrid Systems: Computation and Control, LNCS 1386, 360-373.