Verification of a class of hybrid systems using mathematical programming

A computational procedure for the analysis of a class of hybrid systems evolving under the influence of initial conditions and exogenous inputs is presented in this paper. The procedure consists of constructing a non-deterministic finite state automaton whose behaviors contain the behaviors of the hybrid system and specification, and solving the corresponding language emptiness problem. The underlying computations use convex/LMI techniques and graph search. Specifically, convex/LMI methods are used to outer approximate reach sets and to check if there is a transition between two states of the automaton, while depth first and similar algorithms are employed for emptiness checking. The overall verification procedure iteratively refines the approximating automaton and provides the following guarantee: if the iterations terminate, then the hybrid system satisfies the specifications. Examples are given to illustrate the procedures.