Computing invariants of hybrid system using quantifier elimination

This paper presents a new approach to generate inequalities invariants of hybrid system based on template and quantifier elimination. The main idea is to introduce a candidate parametric invariant as template and then reduce the verification condition into a quantifier elimination problem. The challenge is to deal with the continuous consecution condition of hybrid system because of the existence of differential equation. From the preliminary experiment results, we demonstrate the feasibility of our approach.