Time-to-reach Bounds for Verification of Dynamical Systems Using the Koopman Spectrum

TL;DR

This work reframes reachability verification for nonlinear dynamical systems through the Koopman spectrum, avoiding explicit reachable-set computations by focusing on feasible time-to-reach intervals. It defines real-part and phase-based intervals I_mag and I_phase, and shows that a non-empty intersection across Koopman eigenpairs is a necessary condition for reachability, enabling a finite-dimensional LP-based computation via principal eigenfunctions. The method demonstrates applicability to non-convex and disconnected targets, backward reachability, and high-dimensional systems, with case studies including cart-pole and multi-agent consensus, and offers a comparative analysis against established tools. While providing scalable, infinite-horizon reachability insights, the approach yields necessary but not sufficient conditions, motivating integration with simulations and potential extensions to control inputs.

Abstract

In this work, we present a novel Koopman spectrum-based reachability verification method for nonlinear systems. Contrary to conventional methods that focus on characterizing all potential states of a dynamical system over a presupposed time span, our approach seeks to verify the reachability by assessing the non-emptiness of estimated time-to-reach intervals without engaging in the explicit computation of reachable set. Based on the spectral analysis of the Koopman operator, we reformulate the problem of verifying existence of reachable trajectories into the problem of determining feasible time-to-reach bounds required for system reachability. By solving linear programming (LP) problems, our algorithm can effectively estimate all potential time intervals during which a dynamical system can enter (and exit) target sets from given initial sets over an unbounded time horizon. Finally, we demonstrate our method in challenging settings, such as verifying the reachability between non-convex or even disconnected sets, as well as backward reachability and multiple entries into target sets. Additionally, we validate its applicability in addressing real-world challenges and scalability to high-dimensional systems through case studies in verifying the reachability of the cart-pole and multi-agent consensus systems.

Figures (5)

• Figure 1: Reachability verification pipeline with time-to-reach bounds.
• Figure 2: Reach-time bounds estimation for the Duffing's oscillator system.
• Figure 3: Distribution of estimated reach-time bounds $\hat{I}_{mag} (\lambda, \psi)$ with inaccurate principal eigenfunctions. Red dashed lines indicate error-free case, i.e. when $\delta(x) \equiv 0$.
• Figure 4: Simulation of the Cart-pole system with LQR controller. (a) Convergence of the Cart-pole system under LQR control, with the estimated collision time bounds (red) and reach-time bounds (blue). (b) Motion snapshots within $T = [0.955,10.413]$ demonstrate that the system finally stabilizes if there is no collision occurred. (c) Motion snapshots within the estimated collision time interval $I_{U}^{1} = [0.157,0.955]$.
• Figure 5: Reach-time bounds estimation for the Multi-agent consensus system.

Theorems & Definitions (17)

• Definition 1
• Definition 2
• Theorem 1
• proof
• Theorem 2
• proof
• Corollary 1
• Theorem 3
• proof
• Remark 1