Decidability of hybrid systems with rectangular differential inclusions

A hybrid system is modeled with a finite set of locations and a differential inclusion associated with each location. We discuss a subclass of hybrid systems with constant rectangular differential inclusions. The continuous state of the system is x ∃ IRn with x_i evolving with differential inclusion x _i [L _i , U _i ] where L _i , U _i are integers (i.e., the slope of trajectory of x_i could be changing, but is restricted to remain within [L _i , U _i ]). A transition from one location to another can be made provided the state satisfies the enabling condition for the transition. The state can also be initialized to a new value during the transition. The differential inclusion for x _i can be changed when x _i is an integer or when x _i is initialized to a new value. We show that the verification problem for this class of hybrid systems is decidable. With this approach, systems with unsynchronized and drifting clocks can be modeled, a general differential equation can be abstracted by breaking the state space into regions with constant differential inclusions, and many previously presented hybrid system examples can be verified.