Reachability computation for hybrid systems with Ariadne

Ariadne is an in-progress open environment to design algorithms for computing with hybrid automata, that relies on a rigorous computable analysis theory to represent geometric objects, in order to achieve provable approximation bounds along the computations. In this paper we discuss the problem of reachability analysis of hybrid automata to decide safety properties. We describe in details the algorithm used in Ariadne to compute over-approximations of reachable sets. Then we show how it works on a simple example. Finally, we discuss the lower-approximation approach to the reachability problem and how to extend Ariadne to support it