Taylor approximation for hybrid systems

We propose a new approximation technique for Hybrid Automata. Given any Hybrid Automaton H, we call Approx(H, k) the Polynomial Hybrid Automaton obtained by approximating each formula ϕ in H with the formulae ϕk obtained by replacing the functions in ϕ with their Taylor polynomial of degree k. We prove that Approx(H, k) is an over-approximation of H. We study the conditions ensuring that, given any ϵ > 0, some k0 exists such that, for all k > k0, the “distance” between any vector satisfying ϕk and at least one vector satisfying ϕ is less than ϵ. We study also conditions ensuring that, given any ϵ > 0, some k0 exists such that, for all k > k0, the “distance” between any configuration reached by Approx(H, k) in n steps and at least one configuration reached by H in n steps is less than ϵ.