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

Jianqiang Ding; Shankar A. Deka

REVIEW 4 major objections 5 minor 29 references

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

T0 review · 4 major / 5 minor · reviewed 2026-08-03 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper claims that finite-data Koopman spectral approximations yield reach-time intervals whose Hausdorff distance from the true interval is bounded by Δ with probability at least 1−δ, enabling data-driven reachability certificates.

desk verdict A sensible idea for Koopman-based reachability verification, but Theorem 3's probabilistic bound is not computable in practice — the gap is real and needs fixing before the main claim holds. read the letter →

arxiv 2511.23322 v2 pith:ADB6XKHQ submitted 2025-11-28 eess.SY cs.SY

Jianqiang Ding , Shankar A. Deka This is my paper · ORCID

classification eess.SYcs.SY MSC 93B0393C10

keywords Koopmanoperatorreachabilityverificationdata-drivencontrolprobabilisticguaranteesspectraluncertaintyreach-timeboundseigenfunctionerrorsampling

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper attempts to show that reachability verification of an unknown continuous-time system can be reduced to checking whether a time interval computed from finitely many data points is empty or non-empty, with a formal probabilistic guarantee. It encodes finite-data uncertainty in the Koopman eigenvalues and eigenfunctions, then bounds the Hausdorff distance between the true reach-time interval and the empirical interval. The practical payoff would be verifying reachability without computing reachable sets, which is especially valuable for nonlinear or high-dimensional systems. The guarantee's computability rests on an unproven bridge between the abstract eigenfunction error norm and the pointwise log-magnitude and phase errors that actually enter the final bound.

What carries the argument

The central object is the time-to-reach bound derived from a Koopman eigenpair (λ,ψ): for a trajectory leaving X0 into XF, the real part of λ·t must lie between two log-ratio terms involving eigenfunction extrema on the sets, and the imaginary part must lie between two phase-difference terms. The paper's machinery combines these two interval constraints with two error sources: a multiplicative eigenfunction error (bounded in the observable space by δ_ψ) and an empirical-extremum error (bounded by i.i.d. sampling). The key mechanism is that both errors propagate linearly through the interval endpoints, producing the closed-form Hausdorff bound Δ in Theorem 3.

What would settle it

Take a system whose true Koopman eigenfunctions are known analytically, compute the true reach-time interval, draw finite data, and on each trial evaluate both sides of inequality (11) using the paper's Δ from (12); if the observed frequency of the Hausdorff distance being ≤ Δ falls below 1−δ for any ε, then the bridge from the abstract error bound (5) to Δ_L and Δ_A is invalid.

Watch

Extended reading notes

Core claim

Using a multiplicative-error model for approximate eigenfunctions and i.i.d. sampling of extrema, the paper proves (Theorem 3) that for any error tolerance ε and confidence δ there exists a sufficiently large sample count N such that the Hausdorff distance between the true reach-time interval and the empirical one is at most Δ, with probability at least 1−δ. The total error splits into a model part and a sampling part, and Δ = max((ε+Δ_L)/min|Re λ_i|, (ε+Δ_A)/min|Im λ_i|), where Δ_L and Δ_A are worst-case eigenfunction log-magnitude and phase errors. The proof decomposes the error via Lemma 1 (model uncertainty) and Lemma 2 (sampling uncertainty), then unions over the principal eigenpairs. I

Load-bearing premise

The whole guarantee rests on two premises the paper does not prove: eigenvalues are known exactly, and the eigenfunction error bound stated in the abstract function space can be converted into bounds on the pointwise log-magnitude and phase errors that actually enter the final Hausdorff bound.

Editorial extensions

If this is right

Reachability verification becomes a check of interval non-emptiness, so no reachable set needs to be computed or propagated.
The method handles non-convex, disconnected, or high-dimensional initial and target sets, since only eigenfunction extrema over sets are needed.
The probabilistic guarantee is uniform over eigenpairs: the sample size N can be chosen so the confidence δ is met jointly for all m principal eigenpairs.
An empty empirical interval is, in principle, a finite-data certificate of unreachability with confidence at least 1−δ.
The bound degrades when eigenvalues have small real or imaginary parts, so the certificate weakens for near-pure-oscillatory or near-stable dynamics.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Editorial inference: As stated, the guarantee is not a fully computable certificate, because Δ_L and Δ_A are expressed in terms of the true eigenfunction's worst-case log-errors over the sets; without a computable upper bound that uses only data, Theorem 3 is an existence result rather than an algorithm.
Editorial inference: Removing Assumption 2 (exact eigenvalues) would likely introduce time-dependent terms into the interval endpoints, making a uniform-in-time Hausdorff bound difficult; eigenvalue uncertainty would dominate for long time horizons.
Editorial inference: A practical testable extension is to use extreme-value or order-statistic bounds to estimate the ϵ-optimal-region probability P_ϵ, turning Lemma 3's implicit sample complexity into an explicit finite-N confidence interval.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Short version: this is a reasonable step toward data-driven reachability verification via Koopman spectral uncertainty, and the paper is honest about building on the authors' own earlier time-to-reach results. The genuinely new material — Lemma 1's propagation of multiplicative eigenfunction error and Theorem 3's probabilistic Hausdorff bound — is mostly sound as far as it goes. But the central guarantee is not a usable certificate: Δ in Theorem 3 depends on Δ_L and Δ_A, worst-case sup-norm log-errors of the eigenfunction perturbation over the sets, and the paper provides no way to bound or estimate those from the only assumption on eigenfunction error, an F-norm bound in (5). No bridge from that norm to these uniform log-error quantities is given. This is not a corner case; it is the load-bearing part of the advertised quantifiable error bounds.

Lemma 3's sample complexity is also non-constructive, since N_0 is expressed via the unknown measure P_ϵ of the ϵ-optimal region. That makes the 'there exists N' in Theorem 3 purely existential, and a user has no way to compute a confidence interval from the theorem. The abstract overstates the reachability guarantee: Corollary 1 is a necessary condition only, so the method can certify unreachability but not reachability.

Credit where due: the paper is self-contained regarding Theorems 1–2 (reproved in appendices), the error propagation in Lemma 1 checks out, the proof of Theorem 3 is a clean worst-case argument, and the numerical experiments do a reasonable job of demonstrating empirical convergence, even though they cannot compensate for the missing computable bound. The literature review is fair and the limitations are at least partially acknowledged in Remark 3.

Who this is for: researchers in data-driven verification or Koopman methods who want a clear statement of the current limits of spectral-uncertainty reachability. It deserves a serious referee, but with an expectation of major revision: make Δ computable (or replace the F-norm assumption with a sup-norm one), make the sample complexity constructive, and correct the abstract. I would not cite this in its current form, but the problem it targets is real and the building blocks are mostly sound.

Referee Report

4 major / 5 minor

Summary. The paper proposes a data-driven reachability verification framework for unknown continuous-time systems, based on the Koopman operator spectrum. It recalls time-to-reach bounds from Ding and Deka (2024) using principal eigenpairs, then accounts for two sources of uncertainty: (i) approximation error in learned Koopman eigenfunctions, modeled as a multiplicative error ε(x) with a norm bound in (5), and (ii) sampling error when extrema of eigenfunction magnitudes/phases over the initial and target sets are estimated from i.i.d. samples. The main result, Theorem 3, states that for any tolerance ε>0 and confidence δ∈(0,1), there exists N such that the Hausdorff distance between the true time-to-reach interval and its empirical estimate is bounded by Δ with probability at least 1−δ. Numerical experiments with ResDMD and polynomial dictionaries illustrate the method on systems with known eigenfunctions, the Duffing oscillator, and the Rössler attractor.

Significance. If Theorem 3 were fully instantiable, the framework would be a useful probabilistic reachability certificate that bypasses expensive set propagation. The paper has several strengths: it separates model uncertainty from sampling uncertainty, it makes the recalled time-to-reach theorems self-contained in appendices, and it honestly identifies eigenvalue uncertainty as future work. However, the central probabilistic guarantee depends on quantities that are not computable from the stated assumptions or from data. In particular, Δ_L and Δ_A in Theorem 3 are sup-norm logarithmic error quantities of the true multiplicative eigenfunction error ε, while Assumption (5) only supplies a norm bound in an unspecified Banach space F. No bridge from that norm bound to the sup-norm quantities is given, and no estimation procedure for Δ_L and Δ_A is provided. Consequently, the advertised 'quantifiable error bounds' are not evaluable as stated, and the theorem cannot currently serve as a verification certificate. This is a load-bearing gap rather than a presentation issue.

major comments (4)

[§3, Theorem 3 (Eq. 12) and §2.3, Eq. (5)] The bound Δ is defined via Δ_L and Δ_A, which are worst-case log-magnitude and phase errors of the true multiplicative eigenfunction error ε_i over X0 and XF. These are uniform (sup-norm) quantities. The only assumption on eigenfunction error, Eq. (5), bounds ||εψ−ψ||_F ≤ δ_ψ in an unspecified Banach space F. The paper gives no argument that a small F-norm error controls sup_{x∈X0∪XF} |log|ε(x)|| or the phase log-error, especially in regions where ψ is small. In the typical L2 setting, L2 convergence does not imply uniform control. Thus Δ_L and Δ_A cannot be computed from δ_ψ or from data, and the probabilistic guarantee in (11) is not evaluable. This is the central claim of the paper, so it must be repaired by either proving a sup-norm bridge under additional assumptions or providing a computable data-driven estimate of Δ.
[Appendix C, Lemma 3] The sample complexity N0 = ⌈ log(σ)/log(1−P_ϵ) ⌉ depends on P_ϵ, the probability measure of the ϵ-optimal region of the unknown function h. This quantity depends on the true function, the sampling distribution, and the tolerance, and is not available in practice. Lemma 2 and Theorem 3 therefore only assert the existence of a sufficiently large N, without a computable construction. For a certification method, this is a serious limitation: a user cannot determine how many samples are needed to reach the claimed confidence. A distribution-free sample bound (e.g., based on covering numbers or VC dimension) or an explicit bound on P_ϵ is needed.
[§3, Theorem 3 and §4, Example 3] Theorem 3 states a bound on d_H(Î(λ,ψ), Ĩ(λ,ψ)), the Hausdorff distance between the true and empirical reach-time intervals. If either interval is empty, the usual Hausdorff distance is not defined (or is infinite if exactly one is empty). The motivating unreachability certificate in Example 3 uses an empty empirical interval. The theorem as stated does not cover this case. The paper should either introduce an extended Hausdorff distance convention for empty intervals or formulate a separate theorem that directly gives the probability of an empty empirical interval under unreachability.
[§2.3, Assumption 2] Assumption 2 assumes the Koopman eigenvalues are known precisely or estimated with negligible error (δ_λ=0). This significantly narrows the claim of 'spectral uncertainty': only eigenfunction uncertainty is treated. The abstract and introduction promise encoding 'model uncertainty from finite data' into Koopman spectral representation, and the title says 'under Koopman spectral uncertainty'; the eigenvalue part is excluded. The conclusion acknowledges this as future work, but the assumption should be stated prominently before Theorem 3 and the scope of the title/abstract adjusted accordingly.

minor comments (5)

[§3, Theorem 3] The definition of Δ_L,i is written as a set: Δ_L,i = {|L_{ε_i}(X0,XF)|, |L_{ε_i}(XF,X0)|}. It should be a scalar, presumably Δ_L,i = max{...}, since it is used in arithmetic expressions in Eq. (13)–(14).
[§3, Lemma 1 proof] The displayed inequality in the proof of Lemma 1 has a typo: 'log|ψ(V)|+ log|ε(V)| −log|ψ(V)|+ log |ε(V)|' appears to be missing the overline/underline notation distinguishing sup and inf.
[§3, Theorem 3] The denominators |Re(λ_i)|_min and |Im(λ_i)|_min must be assumed nonzero for the bound to be finite. No nondegeneracy condition is stated. If a principal eigenpair has zero real or imaginary part, the bound in Eq. (12) is undefined or trivial.
[§2.3, Assumption 2] The text says 'Please refer to subsection 2.3 for further discussion' but subsection 2.3 does not contain a discussion of when eigenvalue estimates can be treated as negligible. Adding a remark with applicable conditions would improve the paper.
[§4, Example 2] The claim that the empirical Hausdorff distance 'remains strictly below the estimated upper bound with Theorem 3' is only meaningful if the bound was computed without using ground-truth eigenfunctions. The paper should clarify how Δ_L and Δ_A were obtained in the experiments; using the true ε would not demonstrate a data-driven certificate.

Circularity Check

1 steps flagged · score 6.0 of 10

Theorem 3's probabilistic error bound is defined via the unknown eigenfunction error, so the central guarantee reduces to a sensitivity bound on its own input.

self definitional [Theorem 3 (Eq. 11-12) and proof Eq. (13); Assumption (5)/Section 2.3]
"Here,∆ L .= max i∈{1,···,m} {∆L,i}where each∆ L,i rep- resents the worst-case model error fromψ i, given by∆ L,i = {|Lεi (X0, XF )|,|L εi (XF , X0)|}, and∆ A is defined anal- ogously for the phase. ... Under the eventE i, we have | ˜L ˜ψi − Lψi | ≤ |˜L ˜ψi − L ˜ψi |+|L ˜ψi − Lψi | ≤ϵ+ max{|L εi (X0, XF )|,|L εi (XF , X0)|} =ϵ+ ∆ L,i (13)"

The advertised data-driven error bound Δ is not computed from data: it is defined as the true eigenfunction log-error L_{ε_i} and A_{ε_i} involving the unknown relative error ε_i. Inequality (13) then bounds the reach-time interval discrepancy by exactly ϵ + Δ_{L,i}, i.e. the same input error plus the sampling tolerance. Thus the probabilistic guarantee is a restatement of the assumption that the eigenfunction approximation is accurate; it does not quantify the model uncertainty from finite data. Assumption (5) only bounds an unspecified F-norm, and no bridge to these sup-norm log-extrema is supplied, so Δ cannot be evaluated from data. The central certificate reduces by construction to the unknown eigenfunction error it was meant to bound.

full rationale

Theorems 1 and 2 are recalled from the authors' prior work Ding and Deka (2024) but are fully reproven in Appendices A-B, so that self-citation is not load-bearing. Lemma 2 and Lemma 3 provide a legitimate probabilistic sampling-error argument, although the sample complexity depends on the unknown probability P_ϵ of the ϵ-optimal region, making the existence of N non-constructive. The circularity is concentrated in Theorem 3: the total error bound Δ is defined through L_{ε_i} and A_{ε_i}, i.e. the true worst-case eigenfunction errors. The proof's key inequality (13) then shows the reach-time interval error is no more than this same input error plus the sampling tolerance. Consequently, the advertised 'quantifiable error bound' is not a data-computable certificate; it restates the unknown eigenfunction error as if it were a known bound. This makes the central probabilistic guarantee partially circular, even though the supporting lemmas and the error propagation steps are independently meaningful.

Assumptions & free parameters 3 free parameters · 4 assumptions · 0 invented entities

No new physical or mathematical entities are introduced; principal eigenpairs and the semigroup E come from prior literature (Bollt 2021; Kvalheim & Revzen 2021). The ledger lists the assumptions and uncomputable quantities that the central probabilistic bound rests on.

free parameters (3)

Δ_L (worst-case log-magnitude eigenfunction error)
Appears in the bound Δ in Theorem 3 (eq. 12) as Δ_L = max_i max{|L_{ε_i}(X0,XF)|, |L_{ε_i}(XF,X0)|}. It is not fitted to data, but it is the true worst-case error of the learned eigenfunctions, unknown and not computable from the stated assumptions; the theorem's guarantee presupposes this quantity without providing an estimator.
Δ_A (worst-case phase log-error)
Same for phase; appears in eq. (12). The guarantee cannot be instantiated without it.
N_0 (required sample count)
Lemma 3 gives N_0 = ⌈log(σ)/log(1−P_ϵ)⌉, which depends on the unknown probability mass P_ϵ of the ϵ-optimal region of each eigenfunction over the sets; the paper does not show how to choose N in practice.

assumptions (4)

domain assumption Assumption 1: finite dataset D={(x_k,y_k)} of exact snapshot pairs y_k = s_Δt(x_k) with noiseless state measurements.
Section 2, Assumption 1. Load-bearing: any measurement noise or partial-state observation would invalidate the spectral error analysis, and the experiments use noise-free simulation data.
ad hoc to paper Assumption 2: Koopman eigenvalues are known precisely or estimated with negligible error (δ_λ=0).
Section 2, Assumption 2 and footnote 1. Eliminates eigenvalue uncertainty from the 'spectral uncertainty' the paper claims to analyze; the conclusion section lists eigenvalue uncertainty as future work.
ad hoc to paper The eigenfunction approximation error is modeled as multiplicative ε(x) with an F-norm bound (5): ‖εψ−ψ‖_F ≤ δ_ψ.
Section 2.3, eq. (5). The stated bound is in the space F, but Theorem 3 needs pointwise sup-norm bounds on log|ε| (Δ_L, Δ_A); the paper provides no bridge, so the F-norm bound is not sufficient as stated.
domain assumption Extrema of eigenfunctions on X0 and XF are estimated from i.i.d. samples with known ϵ-optimal-region probability (Lemma 3).
Section 3, Lemma 2–3. The sample-size prescription requires unknown P_ϵ; in practice the uniform-over-the-set sampling assumption may not match trajectory-generated data.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Data-driven Reachability Verification with Probabilistic Guarantees under Koopman Spectral Uncertainty." pith.science (2026). https://pith.science/paper/ADB6XKHQ

@misc{pith2026251123322,
  author       = {Pith},
  title        = {Pith review of: Data-driven Reachability Verification with Probabilistic Guarantees under Koopman Spectral Uncertainty},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/ADB6XKHQ}},
  note         = {Machine review of arXiv:2511.23322}
}

read the original 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. We finally demonstrate the efficacy of our framework in numerical examples.

Figures

Figures reproduced from arXiv: 2511.23322 by the authors.

**Figure 1.** Comparison of the true principal eigenfunctions [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗

**Figure 5.** Convergence analysis of the reach-time error from [PITH_FULL_IMAGE:figures/full_fig_p006_5.png] view at source ↗

Figures from the paper (2 more)

**Figure 4.** Figure 4: Reachable set computed with approximated prin [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]

**Figure 6.** Figure 6: Reachability verification of the Roessler attractor system. [PITH_FULL_IMAGE:figures/full_fig_p007_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

29 extracted references · 4 linked inside Pith

[1]

, " * write output.state after.block = add.period write newline

ENTRY address author booktitle chapter doi edition editor eid howpublished institution journal key month note number organization pages publisher school series title type url volume year label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sent...
[2]

write newline

" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...
[3]

Alanwar, A., Koch, A., Allg \"o wer, F., and Johansson, K.H. (2021). Data-driven reachability analysis using matrix zonotopes. In Learning for Dynamics and Control, 163--175. PMLR

2021
[4]

Alanwar, A., Koch, A., Allg \"o wer, F., and Johansson, K.H. (2023). Data-driven reachability analysis from noisy data. IEEE Transactions on Automatic Control, 68(5), 3054--3069

2023
[5]

Bak, S., Bogomolov, S., Hencey, B., Kochdumper, N., Lew, E., and Potomkin, K. (2025). Reachability of koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement. Formal Methods in System Design, 1--27

2025
[6]

and Tomlin, C

Bansal, S. and Tomlin, C. (2020). Deepreach: A deep learning approach to high-dimensional reachability,''nov. arXiv preprint arXiv:2011.02082

arXiv 2020
[7]

primary eigenfunction,

Bollt, E.M. (2021). Geometric considerations of a good dictionary for koopman analysis of dynamical systems: Cardinality,“primary eigenfunction,” and efficient representation. Communications in Nonlinear Science and Numerical Simulation, 100, 105833

2021
[8]

Colbrook, M.J., Ayton, L.J., and Sz o ke, M. (2023). Residual dynamic mode decomposition: robust and verified koopmanism. Journal of Fluid Mechanics, 955, A21

2023

Show all 29 references

[9]

and Townsend, A

Colbrook, M.J. and Townsend, A. (2024). Rigorous data-driven computation of spectral properties of koopman operators for dynamical systems. Communications on Pure and Applied Mathematics, 77(1), 221--283

2024
[10]

Deka, S.A., Narayanan, S.S., and Vaidya, U. (2023). Path-integral formula for computing koopman eigenfunctions. In 2023 62nd IEEE Conference on Decision and Control (CDC), 6641--6646. IEEE

2023
[11]

and Arcak, M

Devonport, A. and Arcak, M. (2020 a ). Data-driven reachable set computation using adaptive gaussian process classification and monte carlo methods. In 2020 American control conference (ACC), 2629--2634. IEEE

2020
[12]

and Arcak, M

Devonport, A. and Arcak, M. (2020 b ). Estimating reachable sets with scenario optimization. In Learning for dynamics and control, 75--84. PMLR

2020
[13]

and Deka, S.A

Ding, J. and Deka, S.A. (2024). Time-to-reach bounds for verification of dynamical systems using the koopman spectrum. arXiv preprint arXiv:2411.05554

2024
[14]

Herbert, S.L., Bansal, S., Ghosh, S., and Tomlin, C.J. (2019). Reachability-based safety guarantees using efficient initializations. In 2019 IEEE 58th Conference on Decision and Control (CDC), 4810--4816. IEEE

2019
[15]

Ishikawa, I., Hashimoto, Y., Ikeda, M., and Kawahara, Y. (2024). Koopman operators with intrinsic observables in rigged reproducing kernel hilbert spaces. arXiv preprint arXiv:2403.02524

2024
[16]

Kashani, A., Strong, A.K., Bridgeman, L.J., and Danielson, C. (2024). Probabilistic data-driven invariance for constrained control of nonlinear systems. IEEE Control Systems Letters

2024
[17]

u ske, F., and Hamzi, B. (2020). Kernel-based approximation of the koopman generator and schr \

Klus, S., N \"u ske, F., and Hamzi, B. (2020). Kernel-based approximation of the koopman generator and schr \"o dinger operator. Entropy, 22(7), 722

2020
[18]

K \"o hne, F., Philipp, F.M., Schaller, M., Schiela, A., and Worthmann, K. (2025). -error bounds for approximations of the koopman operator by kernel extended dynamic mode decomposition. SIAM journal on applied dynamical systems, 24(1), 501--529

2025
[19]

and Mezi \'c , I

Korda, M. and Mezi \'c , I. (2018). Linear predictors for nonlinear dynamical systems: Koopman operator meets model predictive control. Automatica, 93, 149--160

2018
[20]

Kostic, V., Lounici, K., Novelli, P., and Pontil, M. (2023). Sharp spectral rates for koopman operator learning. Advances in Neural Information Processing Systems, 36, 32328--32339

2023
[21]

and Revzen, S

Kvalheim, M.D. and Revzen, S. (2021). Existence and uniqueness of global Koopman eigenfunctions for stable fixed points and periodic orbits. Physica D: Nonlinear Phenomena, 425, 132959

2021
[22]

and Mezic, I

Mauroy, A. and Mezic, I. (2024). Analytic extended dynamic mode decomposition. arXiv preprint arXiv:2405.15945

2024
[23]

and Mezi \'c , I

Mohr, R. and Mezi \'c , I. (2016). Koopman principle eigenfunctions and linearization of diffeomorphisms. arXiv preprint arXiv:1611.01209

2016 arXiv
[24]

Philipp, F., Schaller, M., Worthmann, K., Peitz, S., and Nueske, F. (2023). Error bounds for kernel-based approximations of the koopman operator. arXiv preprint arXiv:2301.08637

2023 arXiv
[25]

and Rantzer, A

Prajna, S. and Rantzer, A. (2007). Convex programs for temporal verification of nonlinear dynamical systems. SIAM Journal on Control and Optimization, 46(3), 999--1021

2007
[26]

Schmid, P.J. (2010). Dynamic mode decomposition of numerical and experimental data. Journal of fluid mechanics, 656, 5--28

2010
[27]

Tebjou, A., Frehse, G., et al. (2023). Data-driven reachability using christoffel functions and conformal prediction. In Conformal and Probabilistic Prediction with Applications, 194--213. PMLR

2023
[28]

Williams, M.O., Kevrekidis, I.G., and Rowley, C.W. (2015). A data--driven approximation of the koopman operator: Extending dynamic mode decomposition. Journal of Nonlinear Science, 25(6), 1307--1346

2015
[29]

Williams, M.O., Rowley, C.W., and Kevrekidis, I.G. (2014). A kernel-based approach to data-driven koopman spectral analysis. arXiv preprint arXiv:1411.2260

2014 arXiv

Pith tools

Reviewed August 3, 2026 · model on record in the stance chip above.

[1] [1]

, " * write output.state after.block = add.period write newline

ENTRY address author booktitle chapter doi edition editor eid howpublished institution journal key month note number organization pages publisher school series title type url volume year label extra.label sort.label short.list INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sent...

[2] [2]

write newline

" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize " " * FUNCT...

[3] [3]

Alanwar, A., Koch, A., Allg \"o wer, F., and Johansson, K.H. (2021). Data-driven reachability analysis using matrix zonotopes. In Learning for Dynamics and Control, 163--175. PMLR

2021

[4] [4]

Alanwar, A., Koch, A., Allg \"o wer, F., and Johansson, K.H. (2023). Data-driven reachability analysis from noisy data. IEEE Transactions on Automatic Control, 68(5), 3054--3069

2023

[5] [5]

Bak, S., Bogomolov, S., Hencey, B., Kochdumper, N., Lew, E., and Potomkin, K. (2025). Reachability of koopman linearized systems using explicit kernel approximation and polynomial zonotope refinement. Formal Methods in System Design, 1--27

2025

[6] [6]

and Tomlin, C

Bansal, S. and Tomlin, C. (2020). Deepreach: A deep learning approach to high-dimensional reachability,''nov. arXiv preprint arXiv:2011.02082

arXiv 2020

[7] [7]

primary eigenfunction,

Bollt, E.M. (2021). Geometric considerations of a good dictionary for koopman analysis of dynamical systems: Cardinality,“primary eigenfunction,” and efficient representation. Communications in Nonlinear Science and Numerical Simulation, 100, 105833

2021

[8] [8]

Colbrook, M.J., Ayton, L.J., and Sz o ke, M. (2023). Residual dynamic mode decomposition: robust and verified koopmanism. Journal of Fluid Mechanics, 955, A21

2023