Forward inner-approximated reachability of non-linear continuous systems

We propose an approach for computing inner-approximations (also called under-approximations) of reachable sets of dynamical systems defined by non-linear, uncertain, ordinary differential equations. This is a notoriously difficult problem, much more intricate than outer-approximations (also called over-approximations), for which there exist well known solutions, mostly based on Taylor models. The few methods developed recently for inner-approximation mostly rely on backward flowmaps, and extra ingredients, either coming from optimization, or involving topological criteria, are required. Our solution, in comparison, builds on rather inexpensive set-based methods, namely a generalized mean-value theorem combined with Taylor models outerapproximations of the flow and its Jacobian with respect to the uncertain inputs and parameters. We demonstrate with a C/C++ prototype implementation that our method is both efficient and precise on classical examples. The combination of such forward inner and outer Taylor-model based approximations can be used as a basis for the verification and falsification of properties of cyber-physical systems.