BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems

Chelsea Sidrane; Jana Tumova

REVIEW 4 major objections 6 minor 22 references

BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems

T0 review · 4 major / 6 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read Underapproximate backward reachability makes goal-reaching verification sound for nonlinear neural feedback loops.

desk verdict A genuinely useful algorithm for underapproximate backward reachability of nonlinear neural feedback loops, but the soundness proof has a serious undefined-semantics gap that needs to be fixed before the paper can be accepted as a rigorous verification result. read the letter →

arxiv 2505.03643 v1 pith:QJOL3Z4N submitted 2025-05-06 cs.AI cs.LOcs.SYeess.SY

Chelsea Sidrane , Jana Tumova This is my paper · ORCID

classification cs.AIcs.LOcs.SYeess.SY MSC 68Q6068T0790C1193B03

keywords underapproximatebackwardreachabilityneuralfeedbackloopsgoal-reachingverificationmixed-integerlinearprogrammingnonlineardiscrete-timesystemsnetworkanalysis

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

The paper introduces BURNS, an algorithm for computing underapproximate backward reachable sets of discrete-time nonlinear systems whose controller is a fixed neural network. Underapproximate backward reachable sets are the right tool for goal-reaching verification: if the starting set of states is contained in the computed union of norm balls, then every state in the starting set will reach the goal within $k$ steps, with no false alarms. The algorithm overapproximates the nonlinear closed-loop dynamics by a piecewise-linear multi-valued function, encodes that abstraction as a mixed-integer linear program, and solves a sequence of optimization problems to grow norm balls until they touch the boundary of the true backward reachable set. The paper proves the resulting union of balls is a valid underapproximation and demonstrates on a 2-D robot navigation example that the approach can check candidate starting sets in under a tenth of a second.

What carries the argument

The load-bearing object is the underapproximate backward reachable set, represented as a union of $p$-norm balls and computed ball-by-ball through mixed-integer linear programming. The mechanism that makes this tractable is a double approximation: the nonlinear plant $f(x, \mathrm{NN}(x))$ is first overapproximated by a multi-valued piecewise-linear function $\hat f$ built from max/min functions and ReLU activations, each encodable exactly with mixed-integer linear constraints; then, for a sampled center $x_d$, the algorithm solves an optimization problem that maximizes the ball radius subject to the constraint that the terminal state of the $k$-step trajectory leaves the interior of the goal set (opt. prob. 3). The proof that the resulting ball is boundary-coincident with the true backward reachable set guarantees the ball is the largest sound ball centered at $x_d$, and an induction argument (Lemma IV.7) extends the guarantee to all $k$ time steps.

What would settle it

Build a one-step system where the true map sends $x$ to a point outside the goal, while the overapproximation $\hat f$ also contains a spurious branch sending the same $x$ into the goal. The algorithm would include $x$ in its 'underapproximate' backward reachable set of the goal, yet $x$ is not in the true backward reachable set, directly contradicting Theorem IV.8 on that instance.

Watch

Extended reading notes

Core claim

The paper claims that Algorithm 1 produces a valid underapproximation of the $k$-step backward reachable set of a goal set $G$. Concretely, the algorithm outputs a collection of $p$-norm balls whose union is a subset of the true set of states that reach $G$ within $k$ steps under the closed-loop dynamics $f_{\mathrm{cl}}(x) = f(x, \mathrm{NN}(x))$. Because the computed set is an underapproximation, checking that a starting polytope $X_s$ lies inside the union of balls is a sound proof of the goal-reaching specification: every state in $X_s$ is guaranteed to enter $G$ within $k$ steps. The soundness argument combines two pieces: each norm ball is constructed as the largest ball centered at a sampled point that stays inside the true backward reachable set (a boundary-coincident subset), and replacing the true dynamics by a multi-valued overapproximation preserves the underapproximation property over multiple time steps. The numerical example shows that with 25 samples per timestep the union of balls covers roughly $90\%$ to $96\%$ of the true backward reachable set at early timesteps, while the goal-reaching checks themselves take under $0.1$ seconds.

Load-bearing premise

The proof that replacing the true dynamics with the overapproximation preserves the underapproximation relies on an unstated rule: a point counts as reaching the goal only if every branch allowed by the overapproximation reaches it; if the opposite rule is used, the claim is false.

Editorial extensions

If this is right

Goal-reaching properties for nonlinear neural feedback loops become soundly checkable offline: a candidate starting polytope is contained in the union of balls, or a counterexample point is found, via a single MILP.
The volume-fraction estimates used in the paper give a quantitative, tunable measure of verification strength: increasing the number of sampled centers trades computation time for tighter coverage of the true backward reachable set.
Because the method only requires a piecewise-linear overapproximation of the dynamics and piecewise-linear activations in the controller, it applies to any nonlinear discrete-time system for which such an abstraction can be constructed, not only the neural-feedback-loop setting.
The numerical results show solve time growing steeply with the horizon, so the practical frontier is scaling the MILP, which the paper suggests addressing with hybrid-symbolic reachability techniques.

Reading between the lines

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

The computed norm balls are reusable certificates: once a per-step backward reachable set is stored, checking many candidate starting sets costs only one small MILP each, which could make the method practical for runtime monitoring.
The boundary-coincidence construction is not tied to norm balls in principle; the same largest-container-inside-the-set logic should work with ellipsoids or zonotopes, provided their enclosing constraints can be encoded, opening the door to richer underapproximate set families.
The volume-fraction table suggests a direct way to grade a neural controller's verifiability: the coverage of the true backward reachable set measures how far the current policy is from being certified for a given goal, which could drive counterexample-guided policy improvement.
A remaining gap between theory and practice is the sampling of centers: the soundness proof assumes a center is in the true backward reachable set, while the implementation obtains it by rejection sampling; replacing that with a method that can certify membership would close the gap.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

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

This paper tackles a real gap: underapproximate backward reachability for nonlinear neural feedback loops. The algorithmic idea is sensible: overapproximate the closed-loop dynamics with a piecewise-linear multivalued map, then grow norm balls around sampled points by solving MILPs that, in effect, search for a trajectory that exits the goal set. The numerical example is well chosen and the coverage numbers are encouraging. The inclusion-checking reduction in Section IV-F is also a nice piece of work.

That said, the soundness proof has a serious hole. The paper never defines the backward reachable set for the multivalued overapproximation \hat f. Lemmas IV.6 and IV.7 use that notation as if it were self-explanatory, but the claim only holds under a universal ('all branches reach the goal') semantics. Under the natural existential reading, the claimed inclusion is simply false, as the stress-test counterexample shows. The proof of Lemma IV.7 also misapplies Lemma IV.6 by taking Z=G and X=R_f^{(-1)}(G), which does not satisfy the lemma's hypotheses. And in Lemma IV.5's proof, constraint (3d) is misstated as x0 not in G instead of x0 not in int G—minor by itself, but indicative of sloppiness around the boundary cases.

Here is the nuance: the algorithm itself may be sound under the right interpretation. The MILP feasibility check asks whether there exists a branch of \hat f that takes a point outside the goal's interior. If no such branch exists for points in a ball, then all branches of the overapproximation stay in the goal, which is exactly a universal guarantee. The paper's proofs do not capture this, and the exposition does not say it. So I think the flaw is in the proof and the formalization, not necessarily in the algorithm. But as written, Theorem IV.8 is unproven.

Other soft spots: no code is provided, and the evaluation is a single 2D benchmark, which limits confidence in scalability claims. The related work comparison to [14] seems accurate, though.

Bottom line: this is a solid idea that deserves a real referee and major revision. The authors need to define the semantics of \hat f's backward reachable sets, rewrite Lemmas IV.6 and IV.7 with the universal reading, and connect the MILP encoding to that semantics explicitly. If they do that, the paper would be a useful contribution to the verification community. I would not cite the current version in my own work, but I would cite a corrected version. Worth bringing to a reading group as a case study in how a plausible algorithm can be let down by an underspecified proof.

Referee Report

4 major / 6 minor

Summary. The paper introduces BURNS, an algorithm for underapproximate backward reachable set computation for discrete-time nonlinear neural feedback loops, using an overapproximation of the dynamics combined with mixed-integer linear programming. The algorithm samples points in the true backward reachable set, computes maximal norm balls centered at those points via MILPs, and unions the balls to form per-step underapproximations. The paper claims soundness of this construction, uses the resulting sets to check goal-reaching properties, and presents a 2-D navigation example with an ablation over the number of samples. The central idea is plausible and the numerical demonstration is a useful first step, but the current manuscript has several load-bearing gaps in the formal development, most importantly an undefined semantics for backward reachability of the multivalued abstraction and a proof step that relies on a vacuous lemma. These issues are repairable but require substantive rewriting of Section IV-D and the associated optimization encoding.

Significance. If the soundness gaps are fixed, the paper addresses a real gap in the literature: underapproximate backward reachability for nonlinear neural feedback loops, which is the right tool for certifying reach properties. The algorithmic structure, based on OVERT-style overapproximation followed by MILP-based norm-ball maximization, is sensible and the numerical example shows nontrivial coverage of the backward reachable set. The paper is also transparent about its scalability limitation and does not overclaim experimental generality. The main contribution is conditional on a precise semantics for the multivalued abstraction and a correct proof of the inclusion R_hat-f^{-t}(G) ⊆ R_f^{-t}(G); with those fixed, the work would be a meaningful advance in learning-enabled system verification.

major comments (4)

[Section IV-D, Lemmas IV.6 and IV.7] Definition III.1 defines the k-step backward reachable set only for a single-valued function f. Lemmas IV.6 and IV.7 and Theorem IV.8 use the notation R_hat-f^{(-t)}(G) for the multivalued overapproximation hat-f without defining it. This is not cosmetic. Under the existential semantics, where x is included if some branch of hat-f reaches G, the claimed inclusion is false: for f(a)=b, f(b)=c, and hat-f(a)={b,c}, hat-f(b)=c, with G={c}, we have a ∈ R_hat-f^{(-1)}(G) but a ∉ R_f^{(-1)}(G). Under universal semantics, where all branches must reach G, the inclusion can hold, but the paper never states this semantics. Moreover, the MILP encoding in Section IV-A selects a single feasible assignment of binary variables, which corresponds to the existential reading, and the paper never shows that this encoding enforces the universal property needed for soundness. Please define the semantics explicitly, state which one the proofs use, and adapt the optimization encoding and proofs accordingly.
[Section IV-D, Lemma IV.6 and Lemma IV.7] Lemma IV.6 is vacuous as stated. Its hypothesis that Z={f(x)|x∈X} implies R_f^{(-1)}(Z)=X, so the conclusion R_hat-f^{(-1)}(Z)⊆R_f^{(-1)}(Z) reduces to the trivial inclusion R_hat-f^{(-1)}(Z)⊆X. In Lemma IV.7 the lemma is invoked with Z=G and X=R_f^{(-1)}(G), but G is generally not the image of f over X, so the lemma does not apply. Consequently the base case and the inductive step of Lemma IV.7, and therefore Theorem IV.8, are not established. A correct proof must either generalize Lemma IV.6 to arbitrary target sets under the universal semantics or provide a different induction argument.
[Section IV-F, eq. (10)] The encoding of x∉Ball via the max-over-halfspaces construction replaces the complement of a closed ball, {x : ||x||>r}, with {x : ||x||≥r}. A point on the boundary of a ball is therefore treated as being outside the union of balls even though it belongs to the union. If the optimization finds such a boundary point, it is not a genuine counterexample to Xs⊆Q. The paper's statement that using ≥ constraints 'actually enforces P⊂Q rather than P⊆Q but a stricter guarantee is acceptable' is not accurate: the check remains a sufficient condition only if the 'no point found' outcome is the one used to conclude the property holds, and the possibility of a false positive should be stated precisely.
[Theorem IV.8 and Algorithm 1] The theorem statement says Algorithm 1 produces a valid underapproximation of the 'k-step backward reachable set,' but Algorithm 1 actually computes, for each t=1,...,k, a separate underapproximation of R_f^{(-t)}(G) and does not form a single underapproximation of R_f^{(-k)}(G) unless k is the final step. The statement should be rephrased as: for each t∈{1,...,k}, Algorithm 1 produces a valid underapproximation of the t-step backward reachable set of G. This is a logical clarification of the central claim and should be fixed in the next revision.

minor comments (6)

[Lemma IV.5, part b] The proof says constraint (3d) is x0∉G, but the optimization problem in eq. (3) states x0∉intG. Please correct the proof to use the actual constraint and explain whether the intended argument requires x0∉G or x0∉intG.
[Section IV-D, proof of Lemma IV.6] The proof refers to 'theorem III.1' when it means Definition III.1; the same reference error appears in the proof of Lemma IV.6 and in the proof of Lemma IV.5, which refers to 'theorem IV.5' instead of Lemma IV.5.
[Section IV-A, Lemma IV.4 proof] The proof of Lemma IV.4 cites 'theorem II.1' but no such theorem is stated; it should cite Lemma IV.4 itself or the relevant closure property from the preliminaries.
[Section V] The text says 'Sobel sequence' and 'global sobel sampler' in Algorithms 1 and 2; the correct name is the Sobol sequence. Please fix the spelling.
[Section IV-F] The text refers to 'theorem III.2 and theorem III.3' but these are Definitions III.2 and III.3 in the problem statement; please correct the cross-references.
[Section V, Table I] The volume-fraction estimates are computed by Monte Carlo sampling rather than by exact integration; the caption and text should state that these are estimates so that the reader does not overinterpret the reported coverage values.

Circularity Check

0 steps flagged · score 1.0 of 10

No circular derivation; the multivalued-BRS semantic gap is a soundness defect, not a circular reduction.

full rationale

The claimed derivation chain is not circular. Algorithm 1 contains no fitted parameters that are later renamed as predictions: n_samp, the error tolerance, and the domain D are user-chosen knobs that affect coverage and tightness, not the validity of the underapproximation. The single-ball soundness argument (Lemma IV.5) is an optimization/geometry proof showing the minimizer of (3) cannot contain a point outside R_f^{(-k)}(G), so the ball is a subset of the true backward reachable set. The multi-step argument (Lemmas IV.6-IV.7) has a genuine rigor gap: R_{\hat f}^{(-t)} is never defined for the multivalued overapproximation, and under an existential reading the claimed inclusion is false; the proof silently needs a universal 'all branches' semantics and additional monotonicity arguments. That is a correctness/soundness defect in Section IV-D, not circularity, because the proof does not assume Theorem IV.8 and does not fit any value to force the conclusion. The cited prior work [13], [18] supplies OVERT and MILP encodings; these are external, reproducible techniques and are not invoked as an authority to establish the underapproximation result. Thus there is no load-bearing reduction to the paper's own inputs and no self-citation chain on which the central claim depends; the score 1 reflects the minor definitional gap rather than any circular dependency.

Assumptions & free parameters 2 free parameters · 5 assumptions · 0 invented entities

The main mathematical object \hat f is a standard abstraction, not an invented entity. The load-bearing assumptions are the unstated 'all branches' semantics for multivalued backward reachability and the closedness/continuity needed for the closure argument.

free parameters (2)

n_samp = 5, 15, 25
User-chosen number of norm balls per timestep; ablated in Section V. Affects coverage (Table I) but not soundness.
relative error tolerance for OVERT encoding = 1e-6
User-chosen parameter used to encode dynamics in the numerical example, Section V. Controls tightness of the abstraction.

assumptions (5)

domain assumption The true backward reachable sets are closed sets; f_cl is continuous and the goal set G is closed.
Used in Lemma IV.4 and IV.5 to take closures and conclude ball inclusion; not stated as an assumption in Section III.
ad hoc to paper The multivalued abstraction \hat f is an overapproximation of f and its backward reachable set is interpreted with 'for all branches' semantics.
Lemma IV.6 and IV.7 are valid only under this semantics, which the paper never defines. This is load-bearing for the soundness of the abstraction step.
domain assumption Rejection sampling in Algorithm 2 terminates and returns a point in the true backward reachable set.
The algorithm assumes a Sobol sequence over domain D can find such a point; no termination or completeness proof is given.
standard math The MILP solver returns a global optimum for optimization problem (3).
Required for the largest-ball claim in Lemma IV.5; standard for MILP solvers, though solve time may be exponential.
domain assumption Activation functions are piecewise linear, e.g. ReLU, so the closed loop can be encoded into a MILP.
Stated in Section IV-A; excludes smooth activations and is a scope limitation for the method.

how reviews work

0 comments

Cite this review

Pith. "Pith review of BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems." pith.science (2026). https://pith.science/paper/QJOL3Z4N

@misc{pith2026250503643,
  author       = {Pith},
  title        = {Pith review of: BURNS: Backward Underapproximate Reachability for Neural-Feedback-Loop Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/QJOL3Z4N}},
  note         = {Machine review of arXiv:2505.03643}
}

read the original abstract

Learning-enabled planning and control algorithms are increasingly popular, but they often lack rigorous guarantees of performance or safety. We introduce an algorithm for computing underapproximate backward reachable sets of nonlinear discrete time neural feedback loops. We then use the backward reachable sets to check goal-reaching properties. Our algorithm is based on overapproximating the system dynamics function to enable computation of underapproximate backward reachable sets through solutions of mixed-integer linear programs. We rigorously analyze the soundness of our algorithm and demonstrate it on a numerical example. Our work expands the class of properties that can be verified for learning-enabled systems.

Figures

Figures reproduced from arXiv: 2505.03643 by the authors.

**Figure 1.** Visual illustration of algorithm by computing a region around a specific training image where the label does not change [16]. The robust region around the training point is then a set in input space which maps to the label ‘cat.’ A single robustness region does not capture all images that could be labelled ‘cat’ by the network, meaning that it is an underapproximation of the backward reachable set of the label ‘cat’… view at source ↗

**Figure 2.** Illustration of sets relevant to proof of theorem IV.5. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗

**Figure 4.** Visual illustration of theorem IV.6, which demon [PITH_FULL_IMAGE:figures/full_fig_p005_4.png] view at source ↗

Figures from the paper (4 more)

**Figure 3.** Figure 3: Comparison of two figures side by side If there exists a point ∃x1.x1 ∈ (R fcl (−k) (G))c V x1 ∈ intBallp(xd, ϵ∗ ), we can then define its distance to xd to be ϵ1 = ||x1 − xd||p. It follows that ϵ1 < ϵ∗ because all points ∈ intBallp(xd, ϵ∗ ) will have distance to the c…

**Figure 5.** Figure 5: Underapproximate backward reachable sets for seven [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]

**Figure 6.** Figure 6: Computation time taken per steps of backwards [PITH_FULL_IMAGE:figures/full_fig_p007_6.png]

**Figure 7.** Figure 7: Visualization of underapproximation error of back [PITH_FULL_IMAGE:figures/full_fig_p008_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

22 extracted references · 14 canonical work pages

[14]

Backward reachability analysis of neural feedback loops: Techniques for linear and nonlinear systems,

N. Rober, S. M. Katz, C. Sidrane, E. Yel, M. Everett, M. J. Kochen- derfer, and J. P. How, “Backward reachability analysis of neural feedback loops: Techniques for linear and nonlinear systems,”IEEE Open Journal of Control Systems, vol. 2, pp. 108–124, 2023

work page 2023
[1]

Mpcc++: Model predictive contouring con- trol for time-optimal flight with safety constraints,

M. Krinner, A. Romero, L. Bauersfeld, M. Zeilinger, A. Carron, and D. Scaramuzza, “Mpcc++: Model predictive contouring con- trol for time-optimal flight with safety constraints,”arXiv preprint arXiv:2403.17551, 2024

arXiv 2024
[2]

Scal- able multi-robot cooperation for multi-goal tasks using reinforcement learning,

T. An, J. Lee, M. Bjelonic, F. De Vincenti, and M. Hutter, “Scal- able multi-robot cooperation for multi-goal tasks using reinforcement learning,”IEEE Robotics and Automation Letters, 2024

work page 2024
[3]

Learning robust autonomous navigation and locomotion for wheeled- legged robots,

J. Lee, M. Bjelonic, A. Reske, L. Wellhausen, T. Miki, and M. Hutter, “Learning robust autonomous navigation and locomotion for wheeled- legged robots,”Science Robotics, vol. 9, no. 89, p. eadi9641, 2024

2024
[4]

Reaching the limit in autonomous racing: Optimal control versus reinforcement learning,

Y . Song, A. Romero, M. M ¨uller, V . Koltun, and D. Scaramuzza, “Reaching the limit in autonomous racing: Optimal control versus reinforcement learning,”Science Robotics, vol. 8, no. 82, p. eadg1462, 2023

2023
[5]

Baier and J.-P

C. Baier and J.-P. Katoen,Principles of model checking. MIT press, 2008

2008
[6]

Backward reachability analysis of perturbed continuous-time linear systems using set propagation,

M. Wetzlinger and M. Althoff, “Backward reachability analysis of perturbed continuous-time linear systems using set propagation,”arXiv preprint arXiv:2310.19083, 2023

work page arXiv 2023
[7]

Reachability analysis of multi-affine systems,

M. Kloetzer and C. Belta, “Reachability analysis of multi-affine systems,” inInternational Workshop on Hybrid Systems: Computation and Control. Springer, 2006, pp. 348–362

work page 2006

Show all 22 references

[8]

Flow*: An analyzer for non-linear hybrid systems,

X. Chen, E. ´Abrah´am, and S. Sankaranarayanan, “Flow*: An analyzer for non-linear hybrid systems,” inComputer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25. Springer, 2013, pp. 258–263

2013
[9]

The arch-comp friendly verification competition for continuous and hybrid systems,

A. Abate, M. Althoff, L. Bu, G. Ernst, G. Frehse, L. Geretti, T. T. Johnson, C. Menghi, S. Mitsch, S. Schuppet al., “The arch-comp friendly verification competition for continuous and hybrid systems,” inInternational TOOLympics Challenge. Springer, 2024, pp. 1–37

2024
[10]

Hamilton-jacobi reachability: A brief overview and recent advances,

S. Bansal, M. Chen, S. Herbert, and C. J. Tomlin, “Hamilton-jacobi reachability: A brief overview and recent advances,” in2017 IEEE 56th Annual Conference on Decision and Control (CDC). IEEE, 2017, pp. 2242–2253

2017
[11]

Reachable polyhedral marching (rpm): A safety verification algorithm for robotic systems with deep neural network components,

J. A. Vincent and M. Schwager, “Reachable polyhedral marching (rpm): A safety verification algorithm for robotic systems with deep neural network components,” in2021 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 2021, pp. 9029–9035

2021
[12]

Reachability analysis of neural feedback loops,

M. Everett, G. Habibi, C. Sun, and J. P. How, “Reachability analysis of neural feedback loops,”IEEE Access, vol. 9, pp. 163 938–163 953, 2021

2021
[13]

Overt: An algorithm for safety verification of neural network control policies for nonlinear systems,

C. Sidrane, A. Maleki, A. Irfan, and M. J. Kochenderfer, “Overt: An algorithm for safety verification of neural network control policies for nonlinear systems,”Journal of Machine Learning Research, vol. 23, no. 117, pp. 1–45, 2022

2022
[15]

Algorithms for verifying deep neural networks,

C. Liu, T. Arnon, C. Lazarus, C. Strong, C. Barrett, M. J. Kochenderfer et al., “Algorithms for verifying deep neural networks,”Foundations and Trends® in Optimization, vol. 4, no. 3-4, pp. 244–404, 2021

2021
[16]

A dual approach to scalable verification of deep networks

K. Dvijotham, R. Stanforth, S. Gowal, T. A. Mann, and P. Kohli, “A dual approach to scalable verification of deep networks.” inUAI, vol. 1, no. 2, 2018, p. 3

2018
[17]

Premap: A unifying preimage approximation framework for neural networks,

X. Zhang, B. Wang, M. Kwiatkowska, and H. Zhang, “Premap: A unifying preimage approximation framework for neural networks,” arXiv preprint arXiv:2408.09262, 2024

2024 arXiv
[18]

Verifying inverse model neural networks,

C. Sidrane, S. Katz, A. Corso, and M. J. Kochenderfer, “Verifying inverse model neural networks,”arXiv preprint arXiv:2202.02429, 2022

2022 arXiv
[19]

Evaluating robustness of neural networks with mixed integer programming,

V . Tjeng, K. Xiao, and R. Tedrake, “Evaluating robustness of neural networks with mixed integer programming,”arXiv preprint arXiv:1711.07356, 2017

2017 arXiv
[20]

S. M. LaValle,Planning algorithms. Cambridge university press, 2006

2006
[21]

Fast and effective robustness certification,

G. Singh, T. Gehr, M. Mirman, M. P ¨uschel, and M. Vechev, “Fast and effective robustness certification,”Advances in neural information processing systems, vol. 31, 2018

2018
[22]

Ttt: A temporal refinement heuristic for tenuously tractable discrete time reachability problems,

C. Sidrane and J. Tumova, “Ttt: A temporal refinement heuristic for tenuously tractable discrete time reachability problems,”arXiv preprint arXiv:2407.14394, 2024

2024 arXiv

Pith tools

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

[1] [14]

Backward reachability analysis of neural feedback loops: Techniques for linear and nonlinear systems,

N. Rober, S. M. Katz, C. Sidrane, E. Yel, M. Everett, M. J. Kochen- derfer, and J. P. How, “Backward reachability analysis of neural feedback loops: Techniques for linear and nonlinear systems,”IEEE Open Journal of Control Systems, vol. 2, pp. 108–124, 2023

work page 2023

[2] [1]

Mpcc++: Model predictive contouring con- trol for time-optimal flight with safety constraints,

M. Krinner, A. Romero, L. Bauersfeld, M. Zeilinger, A. Carron, and D. Scaramuzza, “Mpcc++: Model predictive contouring con- trol for time-optimal flight with safety constraints,”arXiv preprint arXiv:2403.17551, 2024

arXiv 2024

[3] [2]

Scal- able multi-robot cooperation for multi-goal tasks using reinforcement learning,

T. An, J. Lee, M. Bjelonic, F. De Vincenti, and M. Hutter, “Scal- able multi-robot cooperation for multi-goal tasks using reinforcement learning,”IEEE Robotics and Automation Letters, 2024

work page 2024

[4] [3]

Learning robust autonomous navigation and locomotion for wheeled- legged robots,

J. Lee, M. Bjelonic, A. Reske, L. Wellhausen, T. Miki, and M. Hutter, “Learning robust autonomous navigation and locomotion for wheeled- legged robots,”Science Robotics, vol. 9, no. 89, p. eadi9641, 2024

2024

[5] [4]

Reaching the limit in autonomous racing: Optimal control versus reinforcement learning,

Y . Song, A. Romero, M. M ¨uller, V . Koltun, and D. Scaramuzza, “Reaching the limit in autonomous racing: Optimal control versus reinforcement learning,”Science Robotics, vol. 8, no. 82, p. eadg1462, 2023

2023

[6] [5]

Baier and J.-P

C. Baier and J.-P. Katoen,Principles of model checking. MIT press, 2008

2008

[7] [6]

Backward reachability analysis of perturbed continuous-time linear systems using set propagation,

M. Wetzlinger and M. Althoff, “Backward reachability analysis of perturbed continuous-time linear systems using set propagation,”arXiv preprint arXiv:2310.19083, 2023

work page arXiv 2023

[8] [7]

Reachability analysis of multi-affine systems,

M. Kloetzer and C. Belta, “Reachability analysis of multi-affine systems,” inInternational Workshop on Hybrid Systems: Computation and Control. Springer, 2006, pp. 348–362

work page 2006