Tightened reachability constraints for the verification of linear hybrid systems

In this paper, we first generalize reachability constraints for linear differential equations, then tighten them by using the information of multiplicity of the eigenvalues and eigenvectors of such equations and put them into our constraint based approach for safety verification of hybrid systems that employs recursive reasoning to improve the method of constraint propagation based abstraction refinement.