In this paper, we approximate a hybrid system with arbitrary flow functions by systems with polynomial flows; the verification of certain properties in systems with polynomial flows can be reduced to the first order theory of reals, and is therefore decidable. The polynomial approximations that we construct epsilon-simulate (as opposed to "simulate") the original system, and at the same time are tight. We show that for systems that we call tolerant, safety verification of a system can be reduced to the safety verification of the polynomial approximation. Our main technical tool in proving this result is a logical characterization of epsilon-simulations. We demonstrate the construction of the polynomial approximation, as well as the verification process, by applying it to an example protocol in air traffic coordination.

30th IEEE Real-Time Systems Symposium (RTSS), 2009

Back