Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Alireza Naderi Akhormeh, Ahmad Hafez, Abdulla Fawzy, Amr Alanwar

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.

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

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.

Paper Structure

This paper contains 13 sections, 2 theorems, 52 equations, 5 figures, 1 algorithm.

Table of Contents

  1. INTRODUCTION
  2. Problem Statement and Preliminaries
  3. Set Representations
  4. Problem Statement
  5. Noise Zonotope and Notations
  6. Koopman Operator Representation
  7. Approximating the Koopman Operator From Data
  8. Data-Driven Reachability Analysis
  9. Evaluation
  10. Example 1: Affine Lipschitz dynamic system
  11. Example 2:Non-affine Lipschitz dynamic system
  12. Example 3: Autonomous Vehicle
  13. Conclusion

Key Result

Lemma 1

Let the lifting function $\psi:\mathcal{X}_k\times\mathcal{U}_k\to\mathbb R^p$ be Lipschitz continuous in $x_k$, uniformly in $u_k$, with constant $L_\psi$. Consider the disturbed dynamics in eq:sysnonlingen, then the perturbation induced in the lifted coordinates satisfies Consequently, if $w_k\in\mathcal{Z}_w=\langle c_{\mathcal{Z}_w},G_{\mathcal{Z}_w} \rangle$, the lifted residual satisfies $

Figures (5)

  • Figure 3: Over-approximated reachable sets derived from the reachable sets of the Koopman-lifted system, with residual set modeling to account for approximation errors.
  • Figure 4: Comparison of computed reachable sets using CORA v2025 althoff2015introduction, a least-squares (LS) data-driven model alanwar2021data, and the proposed Koopman-based method, all consistent with noisy input–state data.
  • Figure 5: Comparison of computed reachable sets using CORA v2025 althoff2015introduction, a least-squares (LS) data-driven model alanwar2021data, and the proposed Koopman-based method, all consistent with noisy input–state data for the non-affine system.
  • Figure 6: The JetRacer ROS AI Kit.
  • Figure 7: Comparison of reachable sets consistent with noisy input–state data using the LS method proposed in alanwar2021data and the proposed Koopman method for real world autonomous car.

Theorems & Definitions (11)

  • Definition 1: Zonotope conf:zono1998
  • Definition 2: Exact Reachable Set
  • Remark 1: Bilinear Representation
  • Remark 2: LTI Representation
  • Remark 3: Lifting Function Selection
  • Lemma 1: Lifted Noise Over-approximation
  • proof
  • Theorem 1: Reachable set over-approximation
  • proof
  • Remark 4
  • ...and 1 more