Safety Verification of Non-linear, Planar Proportional Control with Differential Inclusions

A mathematical model of an embedded control system will rarely exhibit the exact behavior of the system, but one can still capture this behavior by including some measure of uncertainty in the models. Physical systems are also often influenced by embedded controllers, adding to the complexity of the models. To verify safety properties of such systems we must be able to check reachability, that is, whether the systems may end up in some undesirable state. A Generalized Polygonal Hybrid System (GSPDI) is a restricted form of hybrid automaton where reachability is decidable, unlike hybrid automata in general. By over-approximating a system given by a complex class of hybrid automata by a GSPDI, we may still verify the safety of the system. In this paper we give a new algorithm which over-approximates a restricted, yet powerful, class of planar hybrid automata where the behavior can be non-linear, non deterministic, and with different dynamics for different parts of the state space. We also show that this class of automata is expressive enough to model embedded proportional control systems.