TIGHTENED REACHABILITY CONSTRAINTS FOR SAFETY VERIFICATION OF LINEAR HYBRID SYSTEMS

摘要

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