Ariadne: Dominance Checking of Nonlinear Hybrid Automata Using Reachability Analysis

When designing embedded systems, often the need arises to model systems having a mixed discrete and continuous behavior. Such hybrid systems commonly consist of a discrete control part that operates in a continuous environment and may be represented by hybrid automata. We recently proposed an open-source framework for hybrid automata analysis, called Ariadne, which exploits approximation techniques based on the theory of computable analysis. In this paper we will show how the approximation capabilities of Ariadne can be used to verify nonlinear hybrid automata inside a design space by means of reachability analysis. In particular, we will use the tool to solve a problem of dominance checking.