Computational Techniques for Hybrid System Verification

Abstract—This paper concerns computational methods for ver-ifying properties of polyhedral invariant hybrid automata (PIHA), which are hybrid automata with discrete transitions governed by polyhedral guards. To verify properties of the state trajectories for PIHA, the planar switching surfaces are partitioned to define a finite set of discrete states in an approximate quotient transition system (AQTS). State transitions in the AQTS are determined by the reachable states, or flow pipes, emitting from the switching sur-faces according to the continuous dynamics. This paper presents a method for computing polyhedral approximations to flow pipes. It is shown that the flow-pipe approximation error can be made arbi-trarily small for general nonlinear dynamics and that the computa-tions can be made more efficient for affine systems. The paper also describes CheckMate, a MATLAB-based tool for modeling, simu-lating and verifying properties of hybrid systems based on the com-putational methods previously described. Index Terms—Hybrid systems, model checking, reachability, verification. I