Pith. sign in

REVIEW 3 major objections 5 minor 46 references

Controlled Reach-avoid Set Computation for Discrete-time Polynomial Systems via Convex Optimization

T0 review · 3 major / 5 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read Randomizing control inputs turns discrete-time reach-avoid computation into convex optimization.

desk verdict A correct and useful probabilistic reformulation of CRASs, marred by a load-bearing typo in the key appendix equation that needs fixing before the method is reproducible. read the letter →

arxiv 2506.06679 v1 pith:D7UPKUUI submitted 2025-06-07 eess.SY cs.SY

Taoran Wu , Yiling Xue , Dejin Ren , Arvind Easwaran , Martin Fränzle , Bai Xue This is my paper
classification eess.SYcs.SY MSC 93C5590C2293B0393D30
keywords controlledreach-avoidsetsdiscrete-timepolynomialsystemssum-of-squaresoptimizationsemidefiniteprogrammingepsilon-greedy0-reach-avoidsafetyverificationLyapunov-likefunctions
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 aims to show that controlled reach-avoid sets (CRASs) for discrete-time polynomial systems—the initial states from which some control policy can steer the system into a target set without leaving a safe set—can be inner-approximated by solving a convex optimization problem. The idea is to treat the control inputs as random variables drawn from any distribution with full support on the control set. Under that probabilistic lens, the paper proves that a CRAS is exactly a 0-reach-avoid set: a state is in the set precisely when the probability of a safe journey to the target is strictly positive. The Lyapunov-like inequalities that characterize such sets become sum-of-squares constraints after the maximum over controls is replaced by an expectation, which removes the nonlinear coupling that previously blocked convex computation for discrete-time systems. An iterative epsilon-greedy update of the control distribution then expands the certified set.

What carries the argument

The machinery is the probabilistic replacement of the control variable: control inputs $u$ are drawn i.i.d. from a fixed distribution, and the maximum over $u$ in the Lyapunov-like condition is replaced by an expectation $\mathbb{E}[v(f(x,u))]$. This removes the nonlinear composition terms such as $u^2$ and $u^3$ that made discrete-time certificate synthesis non-convex, because the expectation is linear in $v$. The epsilon-greedy refinement replaces the fixed distribution by a state-dependent mixture concentrated on a $\delta$-neighborhood of a fitted approximate optimal controller, with weight $1-\epsilon$, plus a uniform exploration term with weight $\epsilon$; the resulting inequality (12) is still convex in $v$ and can be encoded as the SOS program (17). Together these transformations turn CRAS computation into a sequence of semidefinite programs.

What would settle it

Construct a discrete-time polynomial system with a closed safe set where the only successful control sequence is forced to lie on the boundary of the control set for every step. Under any full-support distribution the probability of drawing exactly that sequence is zero, so the 0-reach-avoid set is empty while the CRAS is nonempty; finding such an example would disprove the claimed equivalence outside the open-set assumption.

Watch

Extended reading notes

Core claim

The central claim is Theorem 1: under Assumption 1, a controlled reach-avoid set $R$ and a probabilistic 0-reach-avoid set $R_0$ coincide. Since the safe and target sets are open and the dynamics are polynomial, hence locally Lipschitz, a successful finite control sequence has an open neighborhood of control perturbations that still succeeds, so any full-support distribution gives the successful event strictly positive probability. Consequently the hard search over control policies can be replaced by the search for a bounded function $v$ satisfying $\mathbb{E}[v(f(x,u))] - \lambda v(x) \geq 0$ on the safe set minus the target and $v(x) \leq 0$ on the boundary region, which is convex in $v$. Encoding $v$ and the multipliers as sum-of-squares polynomials yields the semidefinite program (8), whose region $\{x \in X : v(x) > 0\}$ is an inner approximation of the CRAS. The paper further claims that iterating with a state-dependent epsilon-greedy distribution—mostly concentrating probability near a fitted optimal controller while retaining small exploration weight elsewhere—enlarges the certified set, and that the resulting method verifies a 12-dimensional safety benchmark in seconds.

Load-bearing premise

The proof hinges on the safe and target sets being open, so that around a successful trajectory there is a whole tube of successful control sequences; if those sets are closed or half-open, the equivalence between a CRAS and a 0-reach-avoid set may break.

Editorial extensions

If this is right

  • CRASs for discrete-time polynomial systems can be inner-approximated by a single convex sum-of-squares program, avoiding the non-convex search for feedback controllers.
  • The initial certified set can be enlarged by iteratively updating the control distribution with an epsilon-greedy rule; each iteration solves another convex program.
  • The probabilistic reformulation extends to control barrier certificates for safety verification, and the paper reports successful verification of benchmarks up to 12 dimensions, including one in 4.9 seconds.
  • Because the expectation condition implies the maximum condition, any certificate found by the method is also valid for the original CRAS definition.
  • The method is presented as the first sum-of-squares approach tailored to CRASs for discrete-time polynomial systems.

Reading between the lines

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

  • If the equivalence is right, the hard part of CRAS computation is not the policy search but the choice of the control distribution; tuning the distribution or the epsilon schedule should be as important as raising the polynomial degree of $v$.
  • The open-set assumption suggests a testable boundary case: practical specifications with closed safe sets may need a limiting argument or a modified theorem.
  • The epsilon-greedy iteration resembles a homotopy from the uniform-distribution certificate to a local controller-based certificate; viewed this way, it could be extended to other certificate classes such as control Lyapunov functions for stabilization.
  • The Monte Carlo volume estimates and grid sampling for controller fitting introduce statistical error that the theory does not yet quantify; a falsifier could compare the SOS-certified set against exact dynamic programming on low-dimensional benchmarks.
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.

Referee Report

3 major / 5 minor

Summary. The paper proposes a convex-optimization framework for computing controlled reach-avoid sets (CRASs) of discrete-time polynomial systems. The central idea is to view control inputs as i.i.d. random variables with a distribution satisfying Assumption 1 and to prove (Theorem 1) that a CRAS is equivalent to a 0-reach-avoid set in this probabilistic sense. Based on this equivalence, the paper formulates an SOS program (8) that inner-approximates a CRAS by searching for a polynomial Lyapunov-like function. It then proposes an iterative algorithm (Algorithm 1), inspired by the epsilon-greedy strategy from reinforcement learning, that updates the control distribution to enlarge the certified set; the iterative condition is stated as Proposition 3 and encoded as the SOS program (17) in Appendix A. The paper reports experiments on several benchmarks, including safety verification comparisons with Fossil and DeepICBC.

Significance. If the central equivalence and the SOS relaxations are correct, the paper makes a valuable contribution: it gives a convex (SOS) route to CRAS computation for discrete-time polynomial systems, a problem where the standard Lyapunov-like conditions are non-convex due to composition with the control input. Theorem 1 is a genuine equivalence result and its proof is essentially sound under the stated open-set assumptions. The SOS program (8) correctly implements Proposition 2 via Putinar-type arguments, and the reported results, including a 12-dimensional safety verification in 4.9 seconds, are impressive. The main weakness is that the iterative expansion step, which is a primary contribution, is documented incorrectly: the SOS encoding (17) does not match the condition (12), so Algorithm 1 as published is not a sound implementation of the paper's own Proposition 3. The paper also relies on Proposition 1 without proof and makes an empirical, rather than proven, claim of iterative enlargement.

major comments (3)
  1. [Appendix A, Eq. (17); Section IV, Proposition 3] The SOS program (17) is not a relaxation of the constraint (12) stated in Proposition 3. As printed, (17) contains a minus sign before the term (ε/Z)∫_U v(f(x,u)) du, whereas (12) requires a plus sign; (17) uses ε as the box half-width, whereas (12) uses δ; and both (12) and (17) display reversed integration limits (ũ0(x)+ε to ũ0(x)−ε instead of ũ0(x)−δ to ũ0(x)+δ). The normalization check in the proof of Proposition 3 confirms that the intended limits are ũ0(x)−δ to ũ0(x)+δ. Because Algorithm 1, line 5, instructs the solver to use (17), the published algorithm does not correctly encode the proposed epsilon-greedy condition. This is a load-bearing error: it must be corrected, and the experiments should be re-run or explicitly confirmed to have used the corrected formula.
  2. [Section II-B, Proposition 1] Proposition 1 is stated without proof and without a precise reference to a theorem in [44]. Since Proposition 3 and hence the iterative expansion step reduce the new condition to Proposition 1, the correctness of the expansion phase rests on a result that the reader cannot verify from the manuscript. Please either include a proof of Proposition 1 or cite an exact theorem statement from [44] that covers this discrete-time controlled setting.
  3. [Section IV, Algorithm 1] The paper claims that Algorithm 1 'computes larger CRASs' and that the epsilon-greedy strategy 'expands' the CRAS, but no monotonicity or convergence theorem is provided for the sequence of sets {x∈X | v_k(x)>0}. The final output is the union of per-iteration CRASs, which is itself a CRAS provided each iterate v_k satisfies the certified condition; however, the paper does not state this union property, and the empirical volume growth is not guaranteed by any proved result. Moreover, line 6 of Algorithm 1 simply says 'update ε' without specifying the update rule, while the examples use different schedules (ε_{t+1}=0.8ε_t, ε_{t+1}=0.5ε_t, etc.). Please state precisely what guarantee is claimed and specify or parameterize the update rule.
minor comments (5)
  1. [Section V] The Monte Carlo volume estimates γ = N/10^6 are point estimates without confidence intervals; reporting values such as 0.9070 to four decimals overstates the precision of a random sample. Please include standard errors or confidence intervals.
  2. [Section II-A] The equivalence in Theorem 1 relies on the safe and target sets being open (strict inequalities h(x)<0, g(x)<0). It would be helpful to state explicitly that closed or half-open specifications require a different argument or an additional assumption, since many practical reach-avoid specifications use closed sets.
  3. [Definition 2] The definition is titled 'p-reach-void sets' but the intended term is 'p-reach-avoid sets'; please fix this typo.
  4. [Example 5] The sentence 'the MOSEK solver fails when a higher-order polynomial is used as controller templates' is unclear: it should specify which scenario failed (e.g., which degree and sampling setup) and whether the reported results were obtained despite this failure.
  5. [Theorem 1 proof] The notation for the perturbed policy is inconsistent: the text introduces π'_0 but later writes ϕ^{π'}_{x0}(t); please unify the notation.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: the CRAS/0-reach-avoid equivalence is a theorem with a constructive tube argument, and the SOS conditions are sufficient relaxations; only minor same-group citations appear.

full rationale

The paper's central derivation is not circular. Theorem 1 proves CRAS iff 0-reach-avoid under Assumption 1 by an open-tube argument: a successful finite control sequence is surrounded by an epsilon-tube of trajectories because X and T are open, and Assumption 1 gives every delta-neighborhood of each control input positive probability, so the product event has positive probability. The converse uses the immediate fact that positive probability entails the existence of a realizing control policy; this is a logical implication, not a definitional identification. The SOS program (8) is derived from Proposition 2, which scales a bounded v to satisfy Lemma 1, itself cited as Theorem 5 of [37] with assumptions that do not include the target result. Under the review rules, that citation is independent support even though it is a same-group reference, so it does not constitute load-bearing circularity. Proposition 3's epsilon-greedy constraint is explicitly a convex relaxation: the proof observes that the weighted average is bounded above by the maximum over U, so any v satisfying (12) satisfies the previously established sufficient condition (3). This is a sound relaxation rather than a fitted prediction renamed as a first-principles result. The appendix's Eq. (17) appears to contain a sign, limit, and epsilon/delta mismatch relative to Proposition 3, and the openness of X and T is a genuine limitation, but these are correctness and modeling concerns, not circularity. The paper contains minor self-citations, but none of them carries the central derivation by itself.

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

The method's soundness rests on standard SOS and Positivstellensatz reasoning, on the open-set and full-support-distribution assumptions that make the CRAS/0-reach-avoid equivalence hold, and on the availability of an over-approximating \hat X. The free parameters are user-chosen tuning values (lambda, epsilon schedule, delta, polynomial degrees, sampling counts) that affect conservatism but not the soundness guarantee.

free parameters (5)
  • lambda (lambda) = 1.01 in Example 1; user-specified in general
    Multiplicative growth factor in the Lyapunov-like conditions (3), (6), (7), (12); larger values tighten the constraint and change the computed set; chosen by hand per example.
  • epsilon initial value and decay schedule = 0.5 with factor 0.8 (Example 3); 0.3 with factor 0.5 (Examples 4-6)
    Exploration weight in the epsilon-greedy distribution update; tuning it changes the final CRAS, as shown in Figure 3.
  • delta (delta) = 0.1 (Examples 1-3), 0.25 (Example 4), 0.01 (Example 5)
    Radius of the exploitation neighborhood around the fitted controller; must be inside U; user-specified.
  • polynomial degrees d_v and d_u = e.g., d_v=4, d_u=6 in Example 2; d_u=2 or 4 in Example 5
    Templates for the Lyapunov-like function and the fitted controller; higher degrees give less conservative sets at higher computational cost.
  • sampling counts N and M = e.g., 50 states and 5 control inputs in Example 2; 10x10 or 20x20 grid and 10 or 20 control inputs in Example 5
    Number of sampled states for controller fitting and number of discretized control candidates in Eq. (10); affects fit quality and runtime.
assumptions (5)
  • domain assumption Safe set X and target set T are open and defined by strict polynomial inequalities h(x)<0 and g(x)<0, with h and g radially unbounded.
    Used to define X and T in Section II-A and in the tube argument of Theorem 1; if the sets were closed, the positive-measure neighborhood argument could fail.
  • standard math The dynamics f is continuous (polynomial) and Lipschitz in x and u on the relevant compact sets.
    Theorem 1's proof uses Lipschitz constants L_x and L_u to bound trajectory perturbations for nearby control sequences.
  • domain assumption Control input set U is a compact interval box, and the chosen probability measure satisfies Assumption 1 (full support on nonempty open subsets).
    Required for the equivalence R = R0 and for the uniform and epsilon-greedy distributions; box form is used throughout the SOS encodings.
  • domain assumption An over-approximating set \hat X satisfying condition (4) can be computed, via the SDP method of [40].
    The SOS programs (8) and (17) use the polynomial \hat h defining \hat X to encode the boundary condition v<=0 on \hat X \ X.
  • standard math Putinar's Positivstellensatz and SOS decomposition yield exact representations of nonnegativity on the relevant semialgebraic sets.
    The SDPs are derived by requiring polynomial expressions to be SOS with multipliers; this is the standard SOS relaxation, not proved in the paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Controlled Reach-avoid Set Computation for Discrete-time Polynomial Systems via Convex Optimization." pith.science (2026). https://pith.science/paper/D7UPKUUI

@misc{pith2026250606679,
  author       = {Pith},
  title        = {Pith review of: Controlled Reach-avoid Set Computation for Discrete-time Polynomial Systems via Convex Optimization},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/D7UPKUUI}},
  note         = {Machine review of arXiv:2506.06679}
}
abstract

This paper addresses the computation of controlled reach-avoid sets (CRASs) for discrete-time polynomial systems subject to control inputs. A CRAS is a set encompassing initial states from which there exist control inputs driving the system into a target set while avoiding unsafe sets. However, efficiently computing CRASs remains an open problem, especially for discrete-time systems. In this paper, we propose a novel framework for computing CRASs which takes advantage of a probabilistic perspective. This framework transforms the fundamentally nonlinear problem of computing CRASs into a computationally tractable convex optimization problem. By regarding control inputs as disturbances obeying certain probability distributions, a CRAS can be equivalently treated as a 0-reach-avoid set in the probabilistic sense, which consists of initial states from which the probability of eventually entering the target set while remaining within the safe set is greater than zero. Thus, we can employ the convex optimization method of computing 0-reach-avoid sets to estimate CRASs. Furthermore, inspired by the $\epsilon$-greedy strategy widely used in reinforcement learning, we propose an approach that iteratively updates the aforementioned probability distributions imposed on control inputs to compute larger CRASs. We demonstrate the effectiveness of the proposed method on extensive examples.

Figures

Figures reproduced from arXiv: 2506.06679 by the authors.

Figure 1
Figure 1. The controller obtained by solving (11). [PITH_FULL_IMAGE:figures/full_fig_p009_1.png] view at source ↗
Figure 2
Figure 2. Black and green curves represent the boundaries of X and T , respectively. Blue and red curves illustrate the CRAS calculated using SOS (8) and Alg. 1, respectively. In [PITH_FULL_IMAGE:figures/full_fig_p011_2.png] view at source ↗
Figure 3
Figure 3. Results of Alg. 1 under different ϵ settings in Example 4, where γ denotes an estimate of the CRAS volume via random sampling. Additionally, we evaluate the impact of different ϵ settings on Alg. 1, as summarized in [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

46 extracted references · 39 canonical work pages

  1. [44]

    IEEE Transactions on Automatic Control68(8), 4682–4694 (2022)

    Zhao, C., Zhang, S., Wang, L., Xue, B.: Inner approximating robust reach-avoid sets for discrete-time polynomial dynamical systems. IEEE Transactions on Automatic Control68(8), 4682–4694 (2022)

    work page 2022

  2. [1]

    IEEE Control Systems Letters5(3), 773–778 (2020)

    Abate, A., Ahmed, D., Giacobbe, M., Peruffo, A.: Formal synthesis of lyapunov neural networks. IEEE Control Systems Letters5(3), 773–778 (2020)

    work page 2020

  3. [2]

    IEEE Transactions on Automatic Control62(10), 5269–5274 (2017)

    Ahmadi, A.A., Parrilo, P.A.: Sum of squares certificates for stability of planar, homogeneous, and switched systems. IEEE Transactions on Automatic Control62(10), 5269–5274 (2017)

    work page 2017

  4. [3]

    The MIT Press (2015)

    Alur, R.: Principles of Cyber-Physical Systems. The MIT Press (2015)

    work page 2015

  5. [4]

    In: 2019 18th European control conference (ECC)

    Ames, A.D., Coogan, S., Egerstedt, M., Notomista, G., Sreenath, K., Tabuada, P.: Control barrier functions: Theory and applications. In: 2019 18th European control conference (ECC). pp. 3420–3431. IEEE (2019)

    2019

  6. [5]

    User’s Guide and Reference Manual, Version4(2019)

    ApS, M.: Mosek optimization toolbox for matlab. User’s Guide and Reference Manual, Version4(2019)

    work page 2019

  7. [6]

    Automatica44(8), 2163–2170 (2008)

    Aylward, E.M., Parrilo, P.A., Slotine, J.J.E.: Stability and robustness analysis of nonlinear systems via contraction metrics and sos programming. Automatica44(8), 2163–2170 (2008)

    work page 2008

  8. [7]

    Advances in neural information processing systems32(2019)

    Chang, Y .C., Roohi, N., Gao, S.: Neural lyapunov control. Advances in neural information processing systems32(2019)

    work page 2019

Show all 46 references
  1. [8]

    In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems

    Chatterjee, K., Henzinger, T.A., Lechner, M., Žikeli ´c, Ð.: A learner-verifier framework for neural network controllers and certificates of stochastic systems. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 3–25. Springer (2023)

    2023

  2. [9]

    In: 2021 60th IEEE Conference on Decision and Control (CDC)

    Clark, A.: Verification and synthesis of control barrier functions. In: 2021 60th IEEE Conference on Decision and Control (CDC). pp. 6105–6112. IEEE (2021)

    2021

  3. [10]

    arXiv preprint arXiv:2209.00081 (2022)

    Clark, A.: A semi-algebraic framework for verification and synthesis of control barrier functions. arXiv preprint arXiv:2209.00081 (2022)

    2022 arXiv

  4. [11]

    Journal of Symbolic Computation5(1-2), 29–35 (1988)

    Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. Journal of Symbolic Computation5(1-2), 29–35 (1988)

    1988

  5. [12]

    Available at SSRN 4880686 (2023)

    Edwards, A., Peruffo, A., Abate, A.: A general framework for verification and control of dynamical models via certificate synthesis. Available at SSRN 4880686 (2023)

    2023

  6. [13]

    In: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control

    Edwards, A., Peruffo, A., Abate, A.: Fossil 2.0: Formal certificate synthesis for the verification and control of dynamical models. In: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control. pp. 1–10 (2024)

    2024

  7. [14]

    IEEE Transactions on Automatic Control66(7), 3138–3151 (2020)

    Gao, Y ., Johansson, K.H., Xie, L.: Computing probabilistic controlled invariant sets. IEEE Transactions on Automatic Control66(7), 3138–3151 (2020)

    2020

  8. [15]

    CRC Press (2000)

    Halanay, A., Rasvan, V .: Stability and stable oscillations in discrete time systems. CRC Press (2000)

    2000

  9. [16]

    In: 2018 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)

    Han, W., Tedrake, R.: Controller synthesis for discrete-time polynomial systems via occupation measures. In: 2018 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). pp. 6911–6918. IEEE (2018)

    2018

  10. [17]

    IEEE Transactions on Automatic Control59(2), 297–312 (2013)

    Henrion, D., Korda, M.: Convex computation of the region of attraction of polynomial control systems. IEEE Transactions on Automatic Control59(2), 297–312 (2013)

    2013

  11. [18]

    Journal of Symbolic Computation24(2), 137–152 (1997)

    Jirstrand, M.: Nonlinear control system design by quantifier elimination. Journal of Symbolic Computation24(2), 137–152 (1997)

    1997

  12. [19]

    IFAC Proceedings V olumes 47(3), 2310–2316 (2014)

    Korda, M., Henrion, D., Jones, C.N.: Controller design and region of attraction estimation for nonlinear dynamical systems. IFAC Proceedings V olumes 47(3), 2310–2316 (2014)

    2014

  13. [20]

    In: 2004 IEEE international conference on robotics and automation (IEEE Cat

    Lofberg, J.: Yalmip: A toolbox for modeling and optimization in matlab. In: 2004 IEEE international conference on robotics and automation (IEEE Cat. No. 04CH37508). pp. 284–289. IEEE (2004)

    2004

  14. [21]

    In: Proc

    Lorenz, E.N.: Predictability: A problem partly solved. In: Proc. Seminar on predictability. vol. 1. Reading (1996)

    1996

  15. [22]

    IEEE Transactions on automatic control56(8), 1849–1861 (2011)

    Margellos, K., Lygeros, J.: Hamilton–jacobi formulation for reach–avoid differential games. IEEE Transactions on automatic control56(8), 1849–1861 (2011)

    2011

  16. [23]

    California Institute of Technology (2000) 14

    Parrilo, P.A.: Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. California Institute of Technology (2000) 14

    2000

  17. [24]

    In: International conference on tools and algorithms for the construction and analysis of systems

    Peruffo, A., Ahmed, D., Abate, A.: Automated and formal synthesis of neural barrier certificates for dynamical models. In: International conference on tools and algorithms for the construction and analysis of systems. pp. 370–388. Springer (2021)

    2021

  18. [25]

    Autonomous Robots43, 275–307 (2019)

    Ravanbakhsh, H., Sankaranarayanan, S.: Learning control lyapunov functions from counterexamples and demonstrations. Autonomous Robots43, 275–307 (2019)

    2019

  19. [26]

    In: 2024 American Control Conference (ACC)

    Ren, D., Wu, T., Xue, B.: An iterative method for computing controlled reach-avoid sets. In: 2024 American Control Conference (ACC). pp. 3590–3597. IEEE (2024)

    2024

  20. [27]

    IEEE Transactions on Reliability (2024)

    Ren, T., Lin, W., Ding, Z.: Formal synthesis of safety controllers viak-inductive control barrier certificates. IEEE Transactions on Reliability (2024)

    2024

  21. [28]

    IFAC Proceedings V olumes46(23), 576–581 (2013)

    Sankaranarayanan, S., Chen, X., et al.: Lyapunov function synthesis using handelman representations. IFAC Proceedings V olumes46(23), 576–581 (2013)

    2013

  22. [29]

    IEEE Transactions on Automatic Control 69(2), 755–770 (2023)

    Schäfer, L., Gruber, F., Althoff, M.: Scalable computation of robust control invariant sets of nonlinear systems. IEEE Transactions on Automatic Control 69(2), 755–770 (2023)

    2023

  23. [30]

    ProQuest (2006)

    Tan, W.: Nonlinear control analysis and synthesis using sum-of-squares programming. ProQuest (2006)

    2006

  24. [31]

    IEEE Transactions on Automatic Control53(2), 565–571 (2008)

    Tan, W., Packard, A.: Stability region analysis using polynomial and composite polynomial lyapunov functions and sum-of-squares programming. IEEE Transactions on Automatic Control53(2), 565–571 (2008)

    2008

  25. [32]

    arXiv preprint arXiv:2411.07640 (2024)

    Toulkani, N.E., Ghabcheloo, R.: Reducing conservativeness of controlled-invariant safe sets by introducing a novel synthesis of control barrier certificates. arXiv preprint arXiv:2411.07640 (2024)

    2024 arXiv

  26. [33]

    IFAC-PapersOnLine 56(2), 1698–1703 (2023)

    Wang, H., Margellos, K., Papachristodoulou, A.: Safety verification and controller synthesis for systems with input constraints. IFAC-PapersOnLine 56(2), 1698–1703 (2023)

    2023

  27. [34]

    In: 2018 Annual American Control Conference (ACC)

    Wang, L., Han, D., Egerstedt, M.: Permissive barrier certificates for safe stabilization using sum-of-squares. In: 2018 Annual American Control Conference (ACC). pp. 585–590. IEEE (2018)

    2018

  28. [35]

    In: 2024 European Control Conference (ECC)

    Wang, X., Knoedler, L., Mathiesen, F.B., Alonso-Mora, J.: Simultaneous synthesis and verification of neural control barrier functions through branch- and-bound verification-in-the-loop training. In: 2024 European Control Conference (ECC). pp. 571–578. IEEE (2024)

    2024

  29. [36]

    Advances in neural information processing systems 36, 2939–2955 (2023)

    Wu, J., Clark, A., Kantaros, Y ., V orobeychik, Y .: Neural lyapunov control for discrete-time systems. Advances in neural information processing systems 36, 2939–2955 (2023)

    2023

  30. [37]

    arXiv preprint arXiv:2404.18118 (2024)

    Xue, B.: Finite-time safety and reach-avoid verification of stochastic discrete-time systems. arXiv preprint arXiv:2404.18118 (2024)

    2024

  31. [38]

    IEEE Transactions on Automatic Control69(12), 8892–8899 (2024)

    Xue, B.: Reach-avoid controllers synthesis for safety critical systems. IEEE Transactions on Automatic Control69(12), 8892–8899 (2024)

    2024

  32. [39]

    In: 2021 American Control Conference (ACC)

    Xue, B., Li, R., Zhan, N., Fränzle, M.: Reach-avoid analysis for stochastic discrete-time systems. In: 2021 American Control Conference (ACC). pp. 4879–4885. IEEE (2021)

    2021

  33. [40]

    In: 2020 59th IEEE Conference on Decision and Control (CDC)

    Xue, B., Zhan, N., Fränzle, M.: Inner-approximating reach-avoid sets for discrete-time polynomial systems. In: 2020 59th IEEE Conference on Decision and Control (CDC). pp. 867–873. IEEE (2020)

    2020

  34. [41]

    In: International Conference on Computer Aided Verification

    Yang, Z., Zhang, L., Zeng, X., Tang, X., Peng, C., Zeng, Z.: Hybrid controller synthesis for nonlinear systems subject to reach-avoid constraints. In: International Conference on Computer Aided Verification. pp. 304–325. Springer (2023)

    2023

  35. [42]

    Advances in Neural Information Processing Systems36(2024)

    Zhang, S., Li, H., Wang, M., Liu, M., Chen, P.Y ., Lu, S., Liu, S., Murugesan, K., Chaudhury, S.: On the convergence and sample complexity analysis of deep q-networks withϵ-greedy exploration. Advances in Neural Information Processing Systems36(2024)

    2024

  36. [43]

    In: 2022 IEEE 61st Conference on Decision and Control (CDC)

    Zhao, C., Fan, C., Xue, B.: Outer-approximating controlled reach-avoid sets for polynomial systems. In: 2022 IEEE 61st Conference on Decision and Control (CDC). pp. 3839–3845. IEEE (2022)

    2022

  37. [45]

    Formal Aspects of Computing 33, 437–455 (2021)

    Zhao, H., Zeng, X., Chen, T., Liu, Z., Woodcock, J.: Learning safe neural network controllers with barrier certificates. Formal Aspects of Computing 33, 437–455 (2021)

    2021

  38. [46]

    In: Proceedings of the AAAI Conference on Artificial Intelligence

    Žikeli ´c, Ð., Lechner, M., Henzinger, T.A., Chatterjee, K.: Learning control policies for stochastic systems with reach-avoid guarantees. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol. 37, pp. 11926–11935 (2023) APPENDIX A. SOS Programming Implementat...

    2023

Pith tools

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