Data-Driven Reachability of Nonlinear Lipschitz Systems via Koopman Operator Embeddings

TL;DR

This paper introduces a data-driven method using Koopman operator embeddings to compute less conservative reachable sets for nonlinear systems, enhancing safety verification for robotic systems.

Contribution

It presents a novel Koopman-based approach that lifts nonlinear dynamics into a linear space, enabling tighter over-approximations of reachable sets with formal guarantees.

Findings

Tighter reachable set over-approximations than existing methods.

Method reduces conservatism over long prediction horizons.

Validated on autonomous vehicle experiments showing improved accuracy.

Abstract

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.