Computing the evolution of hybrid systems using rigorous function calculus

Hybrid systems exhibit all the complexities of finite automata, nonlinear dynamic systems and differential equations, and are extremely difficult to analyze. A rigorous mathematical approach is needed to achieve provable approximation bounds along the computations. In this paper we describe a rigorous numerical calculus for working with functions that can be used for computing the evolution of nonlinear hybrid systems, and the implementation in the tool Ariadne for reachability analysis of hybrid systems. The method is based around expressing the sets attained during the evolution in terms of functions, and computing approximations to these functions, and allows highly accurate approximations for the evolved sets to be computed. An example of the control of the water level in a tank is presented.