Verification for Non-polynomial Hybrid Systems Using Rational Invariants

Hybrid systems with non-polynomial components are widely used in modeling safety critical applications. Due to the complexity arisen from the non-polynomial expression, safety verification for such systems presents a grand challenge. In this paper, we present a new general approach to synthesizing rational invariants for safety verification of non-polynomial hybrid systems (NPHSs). Through system transformation and rational approximation, a NPHS is transformed into an overapproximate hybrid system in rational form. Then, for the over-approximate rational hybrid system, the proposed framework exploits a symbolic-numeric computation method to generate its exact rational invariants, which guarantees the safety property of the original NPHS. The test results show that the rational invariants yield better performances than those obtained from polynomial invariants.