On Verification of Controlled Hybrid Dynamics through Ellipsoidal Techniques

This paper deals with the dynamics of controlled hybrid systems under piecewise open-loop controls restricted by hard bounds. The system equations may be reset when crossing some prespecified domains ("the guards") in the state space. Here the continuous dynamics which govern the motion between the guards are complemented by discrete transitions which govern the resets. A state space model for such systems is proposed and the reach sets for such models are described. A verification problem is considered whose solution indicates whether the reach set (at given time or at some time within a given time interval) intersects or avoids a prespecified target set. The computational side of verification is treated through ellipsoidal techniques that indicate routes for numerical algorithms including parallel calculations.