Reachability analysis is a formal method that rigorously proves whether a dynamical system can reach certain states. Inner approximations of the exact reachable set contain only states that are definitely reachable and are therefore used to falsify specifications. While the majority of state-of-the-art approaches for nonlinear systems obtain an inner approximation via first computing an outer approximation of the reachable set, we directly obtain sound inner approximations by using the Minkowski difference in a reachability algorithm for nonlinear systems. Our implementation uses a combination of polytopes and constrained zonotopes as set representations, resulting in a low polynomial time complexity in the state dimension. A comparison with state-of-the-art approaches on several benchmarks demonstrates the advantages of our approach.     «

Reachability analysis is a formal method that rigorously proves whether a dynamical system can reach certain states. Inner approximations of the exact reachable set contain only states that are definitely reachable and are therefore used to falsify specifications. While the majority of state-of-the-art approaches for nonlinear systems obtain an inner approximation via first computing an outer approximation of the reachable set, we directly obtain sound inner approximations by using the Minkowski...     »