We propose a scalable reachability-based framework for probabilistic, data-driven safety verification of unknown nonlinear dynamics. We use Koopman theory with a neural network (NN) lifting function to learn an approximate linear representation of the dynamics and design linear controllers in this space to enable closed-loop tracking of a reference trajectory distribution. Closed-loop reachable sets are efficiently computed in the lifted space and mapped back to the original state space via NN verification tools. To capture model mismatch between the Koopman dynamics and the true system, we apply conformal prediction to produce statistically-valid error bounds that inflate the reachable sets to ensure the true trajectories are contained with a user-specified probability. These bounds generalize across references, enabling reuse without recomputation. Results on high-dimensional MuJoCo tasks (11D Hopper, 28D Swimmer) and 12D quadcopters show improved reachable set coverage rate, computational efficiency, and conservativeness over existing methods.
Given N length-(T+1) open-loop, dynamically-feasible trajectories generated by P via black-box queries of (?), forming dataset \mathcal{D}=\{(x_{0:T}^{(i)},u_{0:T-1}^{(i)}\}_{i=1}^N, (a) train a Koopman model (\phi,\psi,K_{A},K_{B}) and (b) use the Koopman model to design a time-varying trajectory-tracking controller \pi: \mathcal{X} \times \mathcal{T} \rightarrow \mathcal{U} to stabilize to references generated by P.
Given M length-(T+1) closed-loop trajectories generated by tracking references from P with the controller \pi from Prob. 1, compute a (1-\delta)-confident RSOA \overline{\mathcal{X}}_{0:T} for the closed-loop dynamics (?), which guarantees for any random reference (x^\textrm{ref}_{0:T}, u^\textrm{ref}_{0:T-1}) produced by the planner P with x_0^\textrm{ref} \in \mathcal{X}_0 and initial state x_0 \in \mathcal{B}_\epsilon(x_0^\textrm{ref}), the closed-loop trajectory remains in \overline{\mathcal{X}}_{0:T} with probability at least 1-\delta, i.e., \mathbb{P}\big(\bigwedge_{t=0}^T (x_t \in \overline{\mathcal{X}}_t) \big) \ge 1-\delta.
The text on this page is from arXiv:2601.01076v1 by Devesh Nath, Haoran Yin and Glen Chou, under the licence CC BY 4.0. The corpus made these changes: it read the items out of the LaTeX source, it expanded the macros of the paper, it put each proof after its statement, and it converted the text to HTML. The formulas are the TeX of the paper, and KaTeX renders them. A formula or a reference can look different from the PDF. The page is published under CC BY 4.0.
The record of each item is in analysis/objects/2601/2601.01076.jsonl.