Scalable Data-Driven Reachability Analysis and Control via Koopman Operators with Conformal Coverage Guarantees

Devesh Nath, Haoran Yin and Glen Chou

arXiv: 2601.01076v1 · PDF · 3 January 2026
Categories: eess.SY, cs.AI, cs.LG, cs.RO, cs.SY, math.OC
Licence: CC BY 4.0 The site shows the text.

Abstract

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.

Items 9

Proposition

Proposition 1 (CG Robustness)

0BBQ

-1For some CG G and interval \mathcal{S} \doteq \{s \in \mathbb{R}^{n_i} \mid \underline{s} \le s \le \overline{s}\}, there are affine functions \underline{G}, \overline{G} such that \forall s \in \mathcal{S}, \underline{G}(s) \leq G(s) \leq \overline{G}(s). The inequalities hold element-wise and \underline{G}(s) = \Psi s + \alpha, \overline{G}(s) = \Phi s + \beta, with \Psi, \Phi \in \mathbb{R}^{n_o \times n_i} and \alpha, \beta \in \mathbb{R}^{n_o}.

Used by Proof

Problem

Problem 1 (Model learning & controller design)

73FU

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.

Problem

Problem 2 (1-\delta)-confident RSOA computation)

BXFN

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.

Lemma

Lemma 1 (KRS overapproximation)

LB4Z

11 Let \Gamma denote the closed-loop CG of TKFL, and let \mathcal{X}_0 be the initial set. Suppose the KRS \hat{\overline{\mathcal{X}}}_{0:T} is defined as in (?). Then, for any initial state x_0 \in \mathcal{X}_0, the decoded closed-loop trajectory (?), i.e., \hat{x}_{0:T} = \Gamma(x_0, z^{\text{ref}}_{0:T}, u^{\text{ref}}_{0:T-1}) satisfies \hat{x}_t \in \hat{\mathcal{X}}_t for all t \in \mathcal{T}.

Theorem

Theorem 1 (CKRS Coverage Guarantee)

0E8I

Let \hat{\overline{\mathcal{X}}}_{0:T} be the KRS defined in (?) and let \bar e_t = [\bar e_{t,1}, \ldots, \bar e_{t,n}]^\top \in \mathbb{R}^n. Define the conformalized Koopman reachable set (CKRS) as

\overline{\mathcal{X}}_{0:T}^{1-\delta} \equiv \bigl\{ \hat{\overline{\mathcal{X}}}_t \oplus \mathrm{diag}(\bar e_t) \mathcal{B}_1(0) \bigr\}_{t=0}^T,

where \mathrm{diag}(\bar e_t) \in \mathbb{R}^{n\times n} is a diagonal matrix with \bar e_t on its diagonal. Then, for a new reference trajectory x_{0:T}^{\textrm{ref}, (0)} drawn from the same distribution, the CKRS contains the true closed-loop system trajectory generated by (?) with probability at least 1-\delta, i.e., \mathbb{P}\big( \bigwedge_{t=0}^T x_t^{(0)} \in \overline{\mathcal{X}}_t^{1-\delta} \big) \ge 1-\delta.

Lemma

Lemma 1 (KRS overapproximation)

M6JZ

Let \Gamma denote the closed-loop CG of TKFL, and let \mathcal{X}_0 be the initial set. Suppose the KRS \hat{\overline{\mathcal{X}}}_{0:T} is defined as in (?). Then, for any initial state x_0 \in \mathcal{X}_0, the decoded closed-loop trajectory (?), i.e., \hat{x}_{0:T} = \Gamma(x_0, z^{\text{ref}}_{0:T}, u^{\text{ref}}_{0:T-1}) satisfies \hat{x}_t \in \hat{\mathcal{X}}_t for all t \in \mathcal{T}.

Used by Proof

Proof of Lemma 1

The closed-loop graph \Gamma is a computational graph G as defined in Proposition 1. Using the auto_LiRPA library [Xu2020AutoLiRPA], we compute sound, vector-valued affine bounding functions \underline{\Gamma}_t and \overline{\Gamma}_t (corresponding to \underline{G} and \overline{G} in Proposition 1) for the t-th state output.

By Proposition 1, these bounds are guaranteed to be sound. That is, for any specific input x_0 \in \mathcal{X}_0, the predicted state \hat{x}_t = \Gamma_t(x_0, z^{\text{ref}}_{0:T}, u^{\text{ref}}_{0:T-1}) satisfies

\underline{\Gamma}_t(x_0, z^{\text{ref}}_{0:T}, u^{\text{ref}}_{0:T-1}) \le \hat{x}_t \le \overline{\Gamma}_t(x_0, z^{\text{ref}}_{0:T}, u^{\text{ref}}_{0:T-1}).

The KRS \hat{\overline{\mathcal{X}}}_t is defined in (?) as the interval \textsf{Int}(\hat{x}_t^L, \hat{x}_t^U), where \hat{x}_t^L = \min_{x_0' \in \mathcal{X}_0} \underline{\Gamma}_t(x_0', \dots) and \hat{x}_t^U = \max_{x_0' \in \mathcal{X}_0} \overline{\Gamma}_t(x_0', \dots). By the definitions of the minimum and maximum, we have

\begin{aligned} \hat{x}_t &\ge \underline{\Gamma}_t(x_0, \dots) \ge \min_{x_0' \in \mathcal{X}_0} \underline{\Gamma}_t(x_0', \dots) = \hat{x}_t^L,\\ \hat{x}_t &\le \overline{\Gamma}_t(x_0, \dots) \le \max_{x_0' \in \mathcal{X}_0} \overline{\Gamma}_t(x_0', \dots) = \hat{x}_t^U. \end{aligned}

Hence, \hat{x}_t \in \textsf{Int}(\hat{x}_t^L, \hat{x}_t^U) = \hat{\overline{\mathcal{X}}}_t. Since this holds for all t \in \mathcal{T}, the trajectory \hat{x}_{0:T} is contained within \hat{\overline{\mathcal{X}}}_{0:T}.

Uses Proposition 1

Theorem

Theorem 1 (CKRS Coverage Guarantee)

RF9R

\overline{\mathcal{X}}_{0:T}^{1-\delta} \equiv \bigl\{ \hat{\overline{\mathcal{X}}}_t \oplus \mathrm{diag}(\bar e_t) \mathcal{B}_1(0) \bigr\}_{t=0}^T,

where \mathrm{diag}(\bar e_t) \in \mathbb{R}^{n\times n} is a diagonal matrix with \bar e_t on its diagonal. Then, for a new reference trajectory x_{0:T}^{\textrm{ref}, (0)} drawn from the same distribution, the CKRS contains true closed-loop system trajectory generated by (?) with probability at least 1-\delta:

\mathbb{P}\Big( \bigwedge_{t=0}^T x_t^{(0)} \in \overline{\mathcal{X}}_t^{1-\delta} \Big) \ge 1-\delta.

Proof of Theorem 1

The proof combines a deterministic containment guarantee with a probabilistic coverage guarantee.

Step 1: KRS Containment. By Lemma 1, the decoded closed-loop lifted trajectory \hat{x}_{t,j}^{(0)} is deterministically contained within the hyper-rectangular KRS:

\hat{x}_{t,j}^{(0)} \in \hat{\overline{\mathcal{X}}}_{t,j} = \textsf{Int}(\hat{x}_{t,j}^L, \hat{x}_{t,j}^U), \quad \forall t \in \mathcal{T},\quad \forall j \in \{1,\ldots,n\}.

Step 2: Probabilistic Coverage. The CP guarantee requires exchangeability of the nonconformity scores \{R^{(i)}\}_{i=0}^{K^{\mathrm{cal}}}. In our framework, all calibration and test trajectories share the same reference (z_{0:T}^{\mathrm{ref}}, u_{0:T-1}^{\mathrm{ref}}) and controller G_t, and their initial states x_0^{(i)} are sampled i.i.d. from \mathcal{B}_\epsilon(x_0^{\mathrm{ref}}). Since the decoded closed-loop lifted trajectory (?), true closed-loop trajectory (?), and the nonconformity score are deterministic functions of x_0^{(i)}, the resulting scores R^{(i)} are also i.i.d., and hence exchangeable. By the CP guarantee, the event

\mathcal{E} \equiv \{ |e_{t,j}^{(0)}| \le \bar e_{t,j}, \forall t,j \}

occurs with probability at least 1-\delta.

Step 3: Combined Guarantee. The true state can be decomposed as x_{t,j}^{(0)} = \hat{x}_{t,j}^{(0)} + e_{t,j}^{(0)}. When \mathcal{E} occurs, we have

\hat{x}_{t,j}^L - \bar e_{t,j} \le \hat{x}_{t,j}^{(0)} + e_{t,j}^{(0)} \le \hat{x}_{t,j}^U + \bar e_{t,j},

which by definition implies x_{t,j}^{(0)} \in \overline{\mathcal{X}}_{t,j}^{1-\delta}. Since this holds for all t and j, the trajectory x_{0:T}^{(0)} is contained in the CKRS \overline{\mathcal{X}}_{0:T}^{1-\delta} with probability at least 1-\delta.

Uses Lemma 1

Source and licence

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.