Data-driven Reachability Verification with Probabilistic Guarantees under Koopman Spectral Uncertainty

TL;DR

This paper introduces a data-driven approach using Koopman spectral theory to provide probabilistic reachability guarantees for complex systems without explicit reachable set computation.

Contribution

It presents a novel framework that encodes model uncertainty into Koopman spectral representation, enabling scalable probabilistic reachability verification from finite data.

Findings

Successfully verifies reachability with probabilistic guarantees

Operates without explicit reachable set computation

Validated on representative dynamical systems

Abstract

Providing rigorous reachability guarantees for unknown complex systems is a crucial and challenging task. In this paper, we present a novel data-driven framework that addresses this challenge by leveraging Koopman operator theory. Instead of operating in the state space, the proposed method encodes model uncertainty from finite data directly into Koopman spectral representation with quantifiable error bounds. Leveraging this spectral information, we systematically determine time intervals within which trajectories from the initial set are guaranteed, with a prescribed probability, to reach the target set. This enables the rigorous reachability verification without explicit computation of reachable sets, thereby offering a significant advantage in scalability and applicability. We finally validate the effectiveness of the proposed framework through case studies on representative dynamical systems.