Data-Driven Reachability of Nonlinear Lipschitz Systems via Koopman Operator Embeddings
This addresses safety verification for autonomous vehicles and robotics, offering reduced conservatism while maintaining formal guarantees, though it is incremental as it builds on existing zonotopic and Koopman methods.
The paper tackles the problem of overly conservative reachability analysis for nonlinear robotic systems by proposing a data-driven framework using Koopman operator embeddings, which yields substantially tighter reachable set over-approximations than existing methods, especially over long horizons.
Data-driven safety verification of robotic systems often relies on zonotopic reachability analysis due to its scalability and computational efficiency. However, for nonlinear systems, these methods can become overly conservative, especially over long prediction horizons and under measurement noise. We propose a data-driven reachability framework based on the Koopman operator and zonotopic set representations that lifts the nonlinear system into a finite-dimensional, linear, state-input-dependent model. Reachable sets are then computed in the lifted space and projected back to the original state space to obtain guaranteed over-approximations of the true dynamics. The proposed method reduces conservatism while preserving formal safety guarantees, and we prove that the resulting reachable sets over-approximate the true reachable sets. Numerical simulations and real-world experiments on an autonomous vehicle show that the proposed approach yields substantially tighter reachable set over-approximations than both model-based and linear data-driven methods, particularly over long horizons.