arxiv: 2604.02625 · v1 · submitted 2026-04-03 · 📡 eess.SY · cs.SY

Recognition: 2 theorem links

· Lean Theorem

Data-Driven Nonconvex Reachability Analysis using Exact Set Propagation

Zhen Zhang , M. Umar B. Niazi , Michelle S. Chong , Karl H. Johansson , Amr Alanwar

Authors on Pith no claims yet

Pith reviewed 2026-05-13 20:34 UTC · model grok-4.3

classification 📡 eess.SY cs.SY

keywords data-driven reachabilityconstrained polynomial zonotopesnonconvex reachable setsexact set propagationmodel set refinementpolynomial dynamics

0 comments

The pith

Constrained polynomial matrix zonotopes enable algebraically exact multiplication with state sets for nonconvex reachability analysis.

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

The paper shows how to represent data-consistent models using constrained polynomial matrix zonotopes so that their product with constrained polynomial zonotope state sets can be computed exactly as another constrained polynomial zonotope. This algebraic exactness removes the structural over-approximation that occurs in standard zonotope-based data-driven methods during set propagation. Consequently, reachable sets for unknown systems can be computed without added conservatism and can preserve nonconvex shapes. New data can be used to intersect and tighten the model set online, leading to progressively tighter reachable sets. The framework also extends to polynomial dynamics by providing exact set representations for monomials and their compositions.

Core claim

The central claim is that the multiplication between a constrained polynomial matrix zonotope model set and a constrained polynomial zonotope state set admits an algebraically exact representation as a constrained polynomial zonotope. This enables reachability analysis to proceed entirely within the CPZ representation without propagation-induced over-approximation, even for nonconvex sets. For polynomial systems, exact CPZ representations of monomials and their compositions allow direct set-level propagation without interval arithmetic or relaxations.

What carries the argument

constrained polynomial matrix zonotopes (CPMZs) that represent data-consistent models and permit exact algebraic multiplication with constrained polynomial zonotopes (CPZs) for states

Load-bearing premise

The system dynamics admit an exact polynomial representation that is consistent with observed data, allowing the multiplication to remain algebraic without needing relaxation.

What would settle it

A concrete counterexample with known polynomial dynamics where the computed reachable set after multiplication is strictly larger than the true reachable set, or where the product cannot be expressed exactly as a single CPZ without added terms.

Figures

Figures reproduced from arXiv: 2604.02625 by Amr Alanwar, Karl H. Johansson, Michelle S. Chong, M. Umar B. Niazi, Zhen Zhang.

**Figure 2.** Figure 2: Illustration of the proof of Proposition [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗

**Figure 3.** Figure 3: Projection of Reachable Sets Computed from Input–State Data Using Algorithm [PITH_FULL_IMAGE:figures/full_fig_p014_3.png] view at source ↗

**Figure 4.** Figure 4: Comparative Projection of Reachable Sets from Input–State Data Using Algorithm [PITH_FULL_IMAGE:figures/full_fig_p014_4.png] view at source ↗

**Figure 5.** Figure 5: Projections of reachable sets for a polynomial system. (a) Model-based reachable sets computed using Algorithm [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗

read the original abstract

This paper studies deterministic data-driven reachability analysis for dynamical systems with unknown dynamics and nonconvex reachable sets. Existing deterministic data-driven approaches typically employ zonotopic set representations, for which the multiplication between a zonotopic model set and a zonotopic state set cannot be represented algebraically exactly, thereby necessitating over-approximation steps in reachable-set propagation. To remove this structural source of conservatism, we introduce constrained polynomial matrix zonotopes (CPMZs) to represent data-consistent model sets, and show that the multiplication between a CPMZ model set and a constrained polynomial zonotope (CPZ) state set admits an algebraically exact CPZ representation. This property enables set propagation entirely within the CPZ representation, thereby avoiding propagation-induced over-approximation and even retaining the ability to represent nonconvex reachable sets. Moreover, we develop set-theoretic results that enable the intersection of data-consistent model sets as new data become available, yielding the proposed online refinement scheme that progressively tightens the data-consistent model set and, in turn, the resulting reachable set. Beyond linear systems, we extend the proposed framework to polynomial dynamics and develop additional set-theoretic results that enable both model-based and data-driven reachability analysis within the same algebraic representation. By deriving algebraically exact CPZ representations for monomials and their compositions, reachable-set propagation can be carried out directly at the set level without resorting to interval arithmetic or relaxation-based bounding techniques. Numerical examples for both linear and polynomial systems demonstrate a significant reduction in conservatism compared to state-of-the-art deterministic data-driven reachability methods.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper delivers an algebraically exact CPMZ-CPZ multiplication that removes one source of over-approximation in data-driven reachability, but the gain still hinges on the model set capturing the dynamics exactly.

read the letter

The central advance is the constrained polynomial matrix zonotope that lets multiplication with a constrained polynomial zonotope stay inside the same representation without extra over-approximation. This is a direct fix for the closure problem that forces conservatism in earlier zonotope-based data-driven methods. They also give an online intersection rule that tightens the model set with new data and extend the same machinery to polynomial dynamics with exact monomial handling at the set level. Those pieces are cleanly derived from the set definitions and the numerical examples show visibly smaller reachable sets than the baselines they compare against. That is useful technical progress for anyone who already works with set propagation for safety verification. The limitation is that the exactness property only holds once the data-consistent model set itself is a faithful polynomial representation of the unknown dynamics. For systems whose behavior does not sit exactly inside a low-degree polynomial family, the model set carries its own conservatism before propagation even starts, so the claimed removal of propagation-induced error does not translate into zero extra conservatism overall. The abstract treats the polynomial-dynamics case separately, which suggests the general data-driven claim rests on how well the CPMZ fits arbitrary data without additional relaxation. This work is aimed at people doing deterministic reachability for control systems and robotics. A reader who needs tighter bounds on nonconvex reachable sets will find the new representations and the exact multiplication result worth examining. I would send it to peer review because the algebraic claims are grounded in the set definitions and the numerical evidence is present to check.

Referee Report

2 major / 1 minor

Summary. The paper introduces constrained polynomial matrix zonotopes (CPMZs) to represent data-consistent model sets for deterministic data-driven reachability analysis of systems with unknown dynamics and nonconvex reachable sets. It claims that multiplication between a CPMZ model set and a constrained polynomial zonotope (CPZ) state set admits an algebraically exact CPZ representation, enabling set propagation entirely within the CPZ class without propagation-induced over-approximation. The work also develops intersection-based online refinement of model sets as new data arrive and extends the framework to polynomial dynamics via exact set-theoretic results for monomials and compositions, with numerical examples claimed to show reduced conservatism versus state-of-the-art zonotopic methods.

Significance. If the algebraic exactness property is rigorously established under the paper's conditions, the contribution would be significant for reducing structural conservatism in data-driven reachability, particularly for nonconvex sets and safety-critical applications. The closure under exact multiplication and the online refinement scheme represent clear technical advances over zonotope-based approaches, and the unified treatment of model-based and data-driven polynomial cases is a strength.

major comments (2)

[Abstract] Abstract and central claim: the algebraically exact CPMZ-CPZ multiplication property (and consequent elimination of propagation over-approximation) holds only when the unknown dynamics are exactly captured by a polynomial representation inside the data-consistent CPMZ; for general nonlinear systems this assumption is not automatically satisfied and may embed implicit conservatism in the model set itself, reintroducing the very source of error the method claims to remove. Explicit conditions, error bounds, or data-exclusion rules are needed to substantiate the data-driven claim for arbitrary systems.
[Abstract] Extension to polynomial dynamics: the abstract separates the polynomial-dynamics case, yet the data-driven claim for linear systems still rests on the same exact-capture requirement; without derivations showing how the CPMZ is constructed from data to guarantee exactness (or quantifying the gap), the central non-conservatism result cannot be verified as load-bearing.

minor comments (1)

[Notation] Clarify notation for CPMZ versus CPZ at first use and ensure consistent use of 'algebraically exact' versus 'exact' throughout.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and insightful comments on the scope of our exactness claims. We address each major comment below and agree that targeted clarifications will strengthen the manuscript.

read point-by-point responses

Referee: [Abstract] Abstract and central claim: the algebraically exact CPMZ-CPZ multiplication property (and consequent elimination of propagation over-approximation) holds only when the unknown dynamics are exactly captured by a polynomial representation inside the data-consistent CPMZ; for general nonlinear systems this assumption is not automatically satisfied and may embed implicit conservatism in the model set itself, reintroducing the very source of error the method claims to remove. Explicit conditions, error bounds, or data-exclusion rules are needed to substantiate the data-driven claim for arbitrary systems.

Authors: We agree that the algebraic exactness of CPMZ-CPZ multiplication presupposes that the true dynamics lie within the polynomial class represented by the CPMZ. Our framework is developed specifically for linear and polynomial systems, where this inclusion holds by construction: the data-consistent CPMZ is defined to contain every linear (or polynomial) model that exactly reproduces the observed trajectories. For general nonlinear systems outside this class the method is not claimed, and any implicit conservatism would indeed arise from model mismatch rather than propagation. We will revise the abstract to state the scope explicitly and add a short paragraph in the introduction clarifying the exact-capture assumption together with a reference to the data-consistency definition in Section 3. revision: yes
Referee: [Abstract] Extension to polynomial dynamics: the abstract separates the polynomial-dynamics case, yet the data-driven claim for linear systems still rests on the same exact-capture requirement; without derivations showing how the CPMZ is constructed from data to guarantee exactness (or quantifying the gap), the central non-conservatism result cannot be verified as load-bearing.

Authors: The explicit construction of the data-consistent CPMZ from input-output data is derived in Section 3.1 for the linear case and extended in Section 5 for polynomial dynamics. The resulting CPMZ is the smallest set (in the chosen generator representation) that contains every model whose input-output behavior is identical to the collected data; hence the true linear model is guaranteed to lie inside the set whenever the system is linear. Because the subsequent multiplication with a CPZ state set is shown to be algebraically exact (Theorem 1), no additional over-approximation is introduced during propagation. We will insert a concise summary of this construction and the exact-capture guarantee into the abstract and add a remark quantifying that the only source of conservatism is the data-consistent enclosure itself. revision: partial

Circularity Check

0 steps flagged

No circularity: core property follows from explicit algebraic definitions of new set representations

full rationale

The paper introduces constrained polynomial matrix zonotopes (CPMZs) and constrained polynomial zonotopes (CPZs) as new set representations and proves that their multiplication admits an algebraically exact CPZ representation by direct construction from those definitions. This enables exact propagation without over-approximation. The extension to polynomial dynamics similarly derives exact representations for monomials and compositions via algebraic operations at the set level. No steps reduce a claimed prediction or uniqueness result to a fitted parameter, self-citation chain, or prior ansatz by the same authors; the data-consistent model set is an explicit modeling choice whose exactness is an assumption rather than a derived output. The derivation is therefore self-contained and independent of its inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claim rests on the algebraic closure properties of the newly defined constrained polynomial matrix zonotopes and constrained polynomial zonotopes; these are introduced in the paper rather than taken from prior literature.

axioms (1)

standard math Standard set-theoretic operations on zonotopes and polynomial zonotopes remain valid when extended to the constrained polynomial matrix version.
Invoked when claiming exact representation after multiplication.

invented entities (2)

constrained polynomial matrix zonotope (CPMZ) no independent evidence
purpose: Represent data-consistent model sets so that multiplication with state sets is algebraically exact.
New object defined in the paper to remove the structural source of conservatism in zonotope multiplication.
constrained polynomial zonotope (CPZ) no independent evidence
purpose: Exact representation of reachable sets after propagation through CPMZ models.
Introduced as the target representation that preserves nonconvexity and exactness.

pith-pipeline@v0.9.0 · 5594 in / 1374 out tokens · 37084 ms · 2026-05-13T20:34:12.098765+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

exact set propagation... avoiding propagation-induced over-approximation

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

32 extracted references · 32 canonical work pages

[1]

Reachability Analysis and its Application to the Safety Assessment of Autonomous Cars,

M. Althoff, “Reachability Analysis and its Application to the Safety Assessment of Autonomous Cars,” Ph.D. dissertation, Technische Universit¨at M ¨unchen, 2010

work page 2010
[2]

Rigorously computed orbits of dynamical systems without the wrapping effect,

W. K ¨uhn, “Rigorously computed orbits of dynamical systems without the wrapping effect,”Computing, vol. 61, no. 1, pp. 47–67, 3 1998

work page 1998
[3]

Rierson,Developing safety-critical software: a practical guide for aviation software and DO-178C compliance

L. Rierson,Developing safety-critical software: a practical guide for aviation software and DO-178C compliance. CRC Press, 2017

work page 2017
[4]

Data- driven reachability analysis using matrix zonotopes,

A. Alanwar, A. Koch, F. Allg ¨ower, and K. H. Johansson, “Data- driven reachability analysis using matrix zonotopes,” inLearning for Dynamics and Control, 2021, pp. 163–175

work page 2021
[5]

Data- driven reachability analysis from noisy data,

A. Alanwar, A. Koch, F. Allgower, and K. H. Johansson, “Data- driven reachability analysis from noisy data,”IEEE Transactions on Automatic Control, vol. 68, no. 5, pp. 3054–3069, 2023

work page 2023
[6]

Model-free stochastic reachability using kernel distribution embeddings,

A. J. Thorpe and M. M. Oishi, “Model-free stochastic reachability using kernel distribution embeddings,”IEEE Control Systems Letters, vol. 4, no. 2, pp. 512–517, 2019

work page 2019
[7]

SReachTools kernel module: Data-driven stochastic reachability using Hilbert space em- beddings of distributions,

A. J. Thorpe, K. R. Ortiz, and M. M. Oishi, “SReachTools kernel module: Data-driven stochastic reachability using Hilbert space em- beddings of distributions,” in60th IEEE Conference on Decision and Control (CDC), 2021, pp. 5073–5079

work page 2021
[8]

Data-driven reachability and support estimation with Christoffel functions,

A. Devonport, F. Yang, L. El Ghaoui, and M. Arcak, “Data-driven reachability and support estimation with Christoffel functions,”IEEE Transactions on Automatic Control, vol. 68, no. 9, pp. 5216–5229, 2023

work page 2023
[9]

Data-driven reachability analysis for gaussian process state space models,

P. Griffioen and M. Arcak, “Data-driven reachability analysis for gaussian process state space models,” in62nd IEEE Conference on Decision and Control (CDC), 2023, pp. 4100–4105

work page 2023
[10]

Statistical reacha- bility analysis of stochastic cyber-physical systems under distribution shift,

N. Hashemi, L. Lindemann, and J. V . Deshmukh, “Statistical reacha- bility analysis of stochastic cyber-physical systems under distribution shift,”IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 43, no. 11, pp. 4250–4261, 2024

work page 2024
[11]

Data-driven reachability analysis for human-in-the-loop systems,

V . Govindarajan, K. Driggs-Campbell, and R. Bajcsy, “Data-driven reachability analysis for human-in-the-loop systems,” in56th IEEE Conference on Decision and Control (CDC), 2017, pp. 2617–2622

work page 2017
[12]

Data-driven forward stochastic reachability analysis for human-in-the-loop systems,

J. Choi, S. Byeon, and I. Hwang, “Data-driven forward stochastic reachability analysis for human-in-the-loop systems,” in62nd IEEE Conference on Decision and Control (CDC), 2023, pp. 1730–1735

work page 2023
[13]

Stochastic reachability of uncontrolled systems via probability measures: Approximation via deep neural networks,

K. Sivaramakrishnan, V . Sivaramakrishnan, R. A. Devonport, and M. M. Oishi, “Stochastic reachability of uncontrolled systems via probability measures: Approximation via deep neural networks,” in 2024 IEEE 63rd Conference on Decision and Control (CDC). IEEE, 2024, pp. 7534–7541

work page 2024
[14]

Constrained zonotopes: A new tool for set-based estimation and fault detection,

J. K. Scott, D. M. Raimondo, G. R. Marseglia, and R. D. Braatz, “Constrained zonotopes: A new tool for set-based estimation and fault detection,”Automatica, vol. 69, pp. 126–136, 2016

work page 2016
[15]

Enhancing data-driven reachability analysis using temporal logic side information,

A. Alanwar, F. J. Jiang, M. Sharifi, D. V . Dimarogonas, and K. H. Jo- hansson, “Enhancing data-driven reachability analysis using temporal logic side information,” inInternational Conference on Robotics and Automation (ICRA), 2022, pp. 6793–6799

work page 2022
[16]

Robust data-driven tube-based zonotopic predictive control with closed-loop guarantees,

M. Farjadnia, A. Fontan, A. Alanwar, M. Molinari, and K. H. Johans- son, “Robust data-driven tube-based zonotopic predictive control with closed-loop guarantees,”arXiv preprint arXiv:2409.14366, 2024

work page arXiv 2024
[17]

Boyd and L

S. Boyd and L. Vandenberghe,Convex optimization. Cambridge university press, 2004

work page 2004
[18]

Nonconvex scenario optimization for data-driven reachability,

E. Dietrich, A. Devonport, and M. Arcak, “Nonconvex scenario optimization for data-driven reachability,” in6th Annual Learning for Dynamics & Control Conference, 2024, pp. 514–527

work page 2024
[19]

Data-driven reachability analysis of lipschitz nonlinear systems via support vector data descrip- tion,

Z. Wang, B. Chen, R. M. Jungers, and L. Yu, “Data-driven reachability analysis of lipschitz nonlinear systems via support vector data descrip- tion,” in62nd IEEE Conference on Decision and Control (CDC), 2023, pp. 7043–7048

work page 2023
[20]

On-the-fly control of unknown systems: From side information to performance guarantees through reachability,

F. Djeumou, A. P. Vinod, E. Goubault, S. Putot, and U. Topcu, “On-the-fly control of unknown systems: From side information to performance guarantees through reachability,”IEEE Transactions on Automatic Control, vol. 68, no. 8, pp. 4857–4872, 2022

work page 2022
[21]

Reachability analysis for polynomial dynamical systems using the bernstein expansion

T. Dang and R. Testylier, “Reachability analysis for polynomial dynamical systems using the bernstein expansion.”Reliab. Comput., vol. 17, no. 2, pp. 128–152, 2012

work page 2012
[22]

Reachability computation for polynomial dynamical systems,

T. Dreossi, T. Dang, and C. Piazza, “Reachability computation for polynomial dynamical systems,”Formal Methods in System Design, vol. 50, no. 1, pp. 1–38, 2017

work page 2017
[23]

Reachable set estimation and safety verification of nonlinear systems via iterative sums of squares pro- gramming,

W. Lin, Z. Yang, and Z. Ding, “Reachable set estimation and safety verification of nonlinear systems via iterative sums of squares pro- gramming,”Journal of Systems Science and Complexity, vol. 35, no. 3, pp. 1154–1172, 2022

work page 2022
[24]

Using sos and sublevel set vol- ume minimization for estimation of forward reachable sets,

M. Jones and M. M. Peet, “Using sos and sublevel set vol- ume minimization for estimation of forward reachable sets,”IFAC- PapersOnLine, vol. 52, no. 16, pp. 484–489, 2019

work page 2019
[25]

Sparse polynomial zonotopes: A novel set representation for reachability analysis,

N. Kochdumper and M. Althoff, “Sparse polynomial zonotopes: A novel set representation for reachability analysis,”IEEE Transactions on Automatic Control, vol. 66, no. 9, pp. 4043–4058, 2020

work page 2020
[26]

Data-driven reachability analysis for nonlinear systems,

H. Park, V . Vijay, and I. Hwang, “Data-driven reachability analysis for nonlinear systems,”IEEE Control Systems Letters, 2024

work page 2024
[27]

Constrained polynomial zonotopes,

N. Kochdumper and M. Althoff, “Constrained polynomial zonotopes,” Acta Informatica, vol. 60, no. 3, pp. 279–316, 2023

work page 2023
[28]

Reachability analysis for linear systems with uncertain parameters using polynomial zonotopes,

E. Luo, N. Kochdumper, and S. Bak, “Reachability analysis for linear systems with uncertain parameters using polynomial zonotopes,” in Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control, 2023, pp. 1–12

work page 2023
[29]

Dissipativity verification with guarantees for polynomial systems from noisy input-state data,

T. Martin and F. Allg ¨ower, “Dissipativity verification with guarantees for polynomial systems from noisy input-state data,”IEEE Control Systems Letters, vol. 5, no. 4, pp. 1399–1404, 2020

work page 2020
[30]

Polynomial logical zonotope: A set representation for reachability analysis of logical systems,

A. Alanwar, F. J. Jiang, and K. H. Johansson, “Polynomial logical zonotope: A set representation for reachability analysis of logical systems,”Automatica, vol. 171, p. 111896, 2025

work page 2025
[31]

An introduction to cora 2015,

M. Althoff, “An introduction to cora 2015,” inProc. of the workshop on applied verification for continuous and hybrid systems, 2015, pp. 120–151

work page 2015
[32]

Efficient elimination of redundancies in polyhedra by raytracing,

A. Mar ´echal and M. P ´erin, “Efficient elimination of redundancies in polyhedra by raytracing,” inInternational Conference on Verification, Model Checking, and Abstract Interpretation. Springer, 2017, pp. 367–385

work page 2017