On the Construction of Barrier Certificate: A Dynamic Programming Perspective

Shaoyuan Li; Xiang Yin; Yu Chen

REVIEW 1 major objections 6 minor 31 references

On the Construction of Barrier Certificate: A Dynamic Programming Perspective

T0 review · 1 major / 6 minor · reviewed 2026-08-06 · 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-horizon safety barrier certificates can be made strictly less conservative by replacing a global parameter inequality with a single endpoint constraint, and that the same dynamic-programming construction…

desk verdict Sound DP-based relaxation of finite-horizon barrier conditions, but the novelty claim needs a direct comparison with reference [20] before it can be fully assessed. read the letter →

arxiv 2507.17222 v1 pith:DPH57IF5 submitted 2025-07-23 eess.SY cs.SY

Yu Chen , Shaoyuan Li , Xiang Yin This is my paper · ORCID

classification eess.SYcs.SY MSC 93E1593E2093C55

keywords stochasticsystemsbarriercertificatessafetyverificationreach-avoiddynamicprogrammingsum-of-squaresfinitehorizonc-martingale

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 claims that the standard c-martingale conditions for finite-horizon safety certificates are unnecessarily strict on unsafe states, and that replacing one global parameter inequality with a single endpoint constraint gives strictly weaker conditions that still bound the unsafe probability. If true, the same dynamic-programming view lifts to reach-avoid specifications, producing lower-bound certificates for reach-avoid probability, which existing martingale-based methods cannot provide. The payoff is tighter probability bounds in practice and a unified construction that covers two previously separate certificate families. The authors support the claim with sum-of-squares search programs and two numerical examples.

What carries the argument

The machinery is the dynamic-programming operator $T(v)(x) = 1_{X\setminus S}(x) + 1_S(x)\int_X v(x')\,K(dx'\mid x)$, whose iterates starting from $v_T = 1_{X\setminus S}$ are exactly the unsafe probabilities. The certificate is analyzed through the function $\eta^x_t = \alpha^{t-T}v(x) + (\sum_{i=0}^{T-t-1} \alpha^{-i})\beta$; the difference $\eta^x_t - \eta^x_{t+1} = \alpha^{t-T}(v(x) - \alpha v(x) + \alpha\beta)$ has a sign that is constant in $t$, which collapses $T+1$ induction requirements to two endpoint conditions. Monotonicity of the operator and its linearity on the safe region carry each induction step forward.

What would settle it

Enumerate all triples $(v, \alpha, \beta)$ satisfying the DSBC conditions for a small finite Markov chain whose true unsafe probability is computed exactly by dynamic programming, and check whether the inequality in Eq. (14) ever fails; a single violation would refute Theorem 2. The most plausible failure mode would be a certificate for which the quantity $v(x) - \alpha v(x) + \alpha\beta$ changes sign over $t$, which the constant-parameter monotonicity argument explicitly rules out.

Watch

Extended reading notes

Core claim

The central claim is Theorem 2: if a function $v$ satisfies $v \geq 1_{X\setminus S}$, if the one-step conditional expectation on the safe set satisfies $\mathbb{E}[v] \leq v/\alpha + \beta$, and if the endpoint expression $v(x)\alpha^{-T} + (\sum_{i=0}^{T-1} \alpha^{-i}) \beta \geq 1$ holds for every unsafe state $x$, then the unsafe probability over horizon $T$ is at most that same expression. The proof re-derives the existing c-martingale bound by backward induction on the dynamic-programming value functions, and observes that the inequality needed at every intermediate time step is monotone in $t$ for fixed $x$, so only the two endpoints matter. Since the unsafe-state condition already yields the terminal endpoint, only one additional condition is required. Theorem 3 mirrors this construction for reach-avoid, bounding the reach-avoid probability from below.

Load-bearing premise

The relaxation works only because $v$, $\alpha$, and $\beta$ are held constant over the entire horizon, which makes the sign of the step-to-step difference of $\eta^x_t$ independent of $t$; if any of these quantities were allowed to vary with time, all intermediate constraints would be needed again and the endpoint-only relaxation would collapse.

Editorial extensions

If this is right

A barrier certificate satisfying the new DSBC conditions yields a valid upper bound on the unsafe probability without requiring the global condition $\gamma = \alpha\beta - \alpha + 1 \geq 0$.
The new endpoint condition is weaker than enforcing the bound at every intermediate time step, so the sum-of-squares search program has one fewer constraint and succeeds for a wider range of the parameter $\alpha$.
The reach-avoid barrier certificate (RABC) provides a lower bound on the reach-avoid probability, something standard c-martingale certificates cannot do directly because they only give upper bounds on unsafe probability.
In the two numerical examples, the DSBC found valid bounds for all tested values of $\alpha$, whereas the existing MSBC and SSBC methods failed for many values, and the DSBC produced tighter bounds whenever the old $\gamma \geq 0$ condition would have been active.
The SOS programs require only the value of $\alpha$ to be fixed in advance, whereas the comparable reach-avoid method fixes both $\alpha$ and $\beta$; the proposed relaxation has one fewer user-chosen parameter.

Reading between the lines

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

The same endpoint-compression argument should apply to any DP-based certificate problem where the analogous $\eta$ sequence is monotone in $t$; temporal-logic specifications whose satisfaction probabilities are computed by layered DP operators could inherit the same relaxation.
Because the DSBC unifies the existing MSBC and SSBC families, any future improvement obtained by tuning either of those certificate classes is subsumed by choosing the corresponding parameters in the DSBC, so effort is best spent on selecting $\alpha$ well.
The dual structure of Theorems 2 and 3 suggests that a pair of certificates could sandwich the true satisfaction probability from above and below, giving an interval estimate rather than a one-sided bound.
A natural testable extension is to let $\alpha$ vary over a discrete grid and solve one SOS program per value; the examples indicate that the optimal $\alpha$ is not always 1, so a principled selection rule would directly improve the reported bounds.

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

The core of this paper is a clean, DP-based relaxation of finite-horizon safety barrier conditions and a first real extension to reach-avoid verification. Theorem 2's endpoint constraint is genuinely less conservative than the old gamma >= 0 condition, and the proof is a straightforward backward induction that checks out. Theorem 3's reach-avoid version is a natural dual construction and the monotonicity argument for reducing T+1 constraints down to two endpoints is valid for time-invariant certificates. The SOS programs are standard but correctly encode the conditions, and the two examples at least show the DSBC succeeds where the older certificates fail for some alpha values. This is a genuine improvement over the c-martingale approach, even if the gain is modest.

The soft spots are mostly about scope and comparison. The proof only covers time-invariant certificates; the authors do not claim otherwise, but the limitation is real if one wants to use time-varying alphas or betas. The gamma < 0 transformation is only sketched, though it looks sound. The bigger issue is reference [20], which by title addresses the same safety and reach-avoid verification with sufficient-and-necessary conditions. The paper cites it in a group and never discusses it individually. If that earlier work subsumes Theorems 2 and 3 for constant certificates, the claimed novelty is weakened even if the derivations are correct. This is an addressable omission, not a demonstrated flaw, but it needs fixing before publication. The numerical comparison also leans heavily on two examples; the claim of 'strictly less conservative' is supported but not broadly demonstrated. Noise: the tables show the DSBC and SSBC bounds differ in the fourth decimal for Example 1, which is fine but not a dramatic win.

Would I bring this to reading group? Maybe, for the DP-unification idea and the endpoint monotonicity trick. Would I cite it? Not yet, not until the comparison with [20] is resolved. But this deserves a serious referee: the math is sound, the relaxation is useful, and the reach-avoid extension fills a real gap. My recommendation: send it to review, with the expectation that the authors will need to engage directly with [20] and expand the experiments slightly. A desk rejection would be too harsh for a paper with this much correct content.

Referee Report

1 major / 6 minor

Summary. This paper studies finite-horizon safety and reach-avoid verification of discrete-time stochastic systems using barrier certificates. The authors reinterpret existing c-martingale barrier certificates as upper bounds on the dynamic programming value function and observe that the standard condition γ = αβ − α + 1 ≥ 0 is used only to control the induction step on the unsafe set. They introduce a dynamic-programming-based safety barrier certificate (DSBC, Theorem 2) that drops γ ≥ 0 and adds a single endpoint constraint on X \ S, and a reach-avoid barrier certificate (RABC, Theorem 3) with analogous endpoint constraints. Backward-induction proofs establish probability bounds in both cases, sum-of-squares programs are provided to synthesize the certificates (Theorems 4 and 5), and two numerical examples with exhaustive-computation ground truth demonstrate the improvements over existing methods.

Significance. The dynamic-programming perspective is clear, and the proofs of Theorems 1–3 are elementary, self-contained, and internally consistent; the endpoint-monotonicity argument is valid. The relaxed safety condition is a genuine weakening of the existing c-martingale conditions, and the numerical evidence confirms the tightening. The reach-avoid extension is a useful contribution in a less explored area. The SOS formulations are concrete and the comparison with independent ground truth is a strength. However, the significance of the claimed novelty is conditional on the relationship with reference [20], which is never individually discussed; if [20] already implies the proposed conditions in the finite-horizon setting, the contribution is substantially reduced. The paper does not ship code or machine-checked proofs, but the proof detail is sufficient for hand verification.

major comments (1)

[Section I (Related Works), reference [20]] Reference [20] (B. Xue, arXiv:2408.15572) is cited only in the grouped sentence 'many existing works focus on constructing barrier certificates for infinite-horizon reach-avoid specifications in stochastic systems [18]–[23]'. Its title announces sufficient and necessary barrier-like conditions for safety and reach-avoid verification of stochastic discrete-time systems, without any stated restriction to the infinite-horizon case. Since Theorem 2 and Theorem 3 give sufficient conditions for exactly these finite-horizon problems, the claim that the proposed conditions are new and that [14] is the only related finite-horizon reach-avoid method is not substantiated unless the authors either clarify why [20] falls outside the finite-horizon scope or compare its conditions with DSBC/RABC explicitly. This issue is load-bearing for the contribution claim and should be addressed head-on.

minor comments (6)

[Section V.A, proof of Theorem 2] The text writes 'η_x_t − η_x_{n+1}' but should be 'η_x_t − η_x_{t+1}'; the same typo appears in the proof of Theorem 3 in Section V.B.
[Section V.B, proof of Theorem 3, Cases 2 and 3] The indexing 't = 1, 2, ..., T' should be 't = 0, 1, ..., T−1' for the induction step, since the inequalities (18) and (19) hold for all t and the induction step needs t = n for n = 0, ..., T−1.
[Section VI, SOS program (21)-(26)] Constraint (22) enforces ṽ ≥ 0 on S, which is not required by Theorem 2 and may exclude some DSBCs; the paper should state whether this is a deliberate restriction or an accident.
[Related Works / Section V] The claim that the DSBC is 'strictly less conservative' would be more precise if the authors explicitly noted that every MSBC/SSBC (after the parameter transformation discussed after Theorem 1) satisfies the DSBC conditions, so the DSBC condition set is at least as permissive; the numerical tables illustrate but do not prove the inclusion.
[Section VII (numerical experiments)] The experiments do not report the SOS solver or numerical tolerance used; adding this information would improve reproducibility. Also, 'DBC' and 'DSBC' are used interchangeably; please unify the abbreviation.
[Section II.B and Section VII] Minor typos: 'compute precisely' should be 'computed precisely'; 'Staring from' should be 'Starting from'; and in Section VII, 'the only related method is [14]' is vague and should be rephrased.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the DSBC/RABC bounds follow from a self-contained backward induction; the only self-citation is contextual and not load-bearing.

full rationale

The derivation chain is self-contained. Theorem 1 reproves the existing MSBC bound by backward induction using monotonicity and linearity of the DP operator T, with the gamma >= 0 condition used only to propagate the bound through X\S. Theorem 2 replaces gamma >= 0 by endpoint constraints; the monotonicity of eta_t is proven, so checking the two endpoints suffices for the induction. The bound in Theorem 2 is not an input: condition 3 is a lower bound on the RHS at unsafe states, where the unsafe probability is 1 by definition, and the safety bound at safe states is obtained by induction. Theorem 3 applies the same argument to the lower-bound operator and is again an induction from the terminal condition. The SOS programs implement the certificate conditions and optimize a bound; no ground-truth exhaustive probability is used in the search, and the comparison values in Section VII are computed independently. The only self-reference is [17], a contextual citation on distributionally robust settings; it does not supply any theorem used in the paper. Reference [20] is grouped with infinite-horizon works and never used as a premise, so its relation to the finite-horizon claim is a novelty/comparison concern, not a circularity.

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

The central claim relies on standard dynamic programming results for stochastic systems, on the Markov and autonomous system model, and on polynomial and closed-form moment assumptions for SOS synthesis. alpha, beta, and delta are certificate synthesis variables, not data-fitted physical constants, so they do not introduce circularity.

free parameters (3)

alpha (scaling parameter) = Example 1: 0.99 to 1.01; Example 2: 0.9 to 1.1; Reach-avoid Example 1: 1.06
User-chosen positive scalar that must be fixed before the SOS search; the certificate conditions and the final bound depend on it. It is not fitted to the target probability.
beta (offset parameter) = Optimized by SOS per alpha; reported indirectly through gamma in Table III
Decision variable in the certificate conditions, for example constraint (25) and constraint (26); it affects the bound and feasibility.
delta (upper bound of v on X0) = Optimized in SOS program (21) and constraint (24)
Auxiliary variable introduced to turn the pointwise initial-state bound into a uniform bound; it enters the bound linearly.

assumptions (4)

standard math DP value functions characterize exact safety and reach-avoid probabilities (Lemmas 1 and 2, adopted from [4] and [26]).
The entire barrier certificate argument uses these characterizations as ground truth; the paper does not reprove them.
domain assumption The transition kernel K is a Borel measurable Markov kernel and the system is autonomous with static safe and target sets.
Used to define the operators T and T-hat and to justify the backward induction; time-varying sets or non-Markov noise would break the DP recursion.
domain assumption Assumption 1: polynomial dynamics, super-level set representations, and distributions with closed-form moments for SOS integration.
Needed for the SOS programs (21)-(26) and (28)-(34) to be tractable; the numerical examples satisfy it.
standard math For the MSBC and SSBC comparison, the gamma < 0 case can be transformed to gamma = 0 without loss of generality.
Proven via the parameter change alpha' = (1-beta)^{-1} in Section IV; it relies on beta in [0,1) for the MSBC case.

how reviews work

0 comments

Cite this review

Pith. "Pith review of On the Construction of Barrier Certificate: A Dynamic Programming Perspective." pith.science (2026). https://pith.science/paper/DPH57IF5

@misc{pith2026250717222,
  author       = {Pith},
  title        = {Pith review of: On the Construction of Barrier Certificate: A Dynamic Programming Perspective},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DPH57IF5}},
  note         = {Machine review of arXiv:2507.17222}
}

abstract

In this paper, we revisit the formal verification problem for stochastic dynamical systems over finite horizon using barrier certificates. Most existing work on this topic focuses on safety properties by constructing barrier certificates based on the notion of $c$-martingales. In this work, we first provide a new insight into the conditions of existing martingale-based barrier certificates from the perspective of dynamic programming operators. Specifically, we show that the existing conditions essentially provide a bound on the dynamic programming solution, which exactly characterizes the safety probability. Based on this new perspective, we demonstrate that the barrier conditions in existing approaches are unnecessarily conservative over unsafe states. To address this, we propose a new set of safety barrier certificate conditions that are strictly less conservative than existing ones, thereby providing tighter probability bounds for safety verification. We further extend our approach to the case of reach-avoid specifications by providing a set of new barrier certificate conditions. We also illustrate how to search for these new barrier certificates using sum-of-squares (SOS) programming. Finally, we use two numerical examples to demonstrate the advantages of our method compared to existing approaches.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

31 extracted references · 25 canonical work pages

[20]

Sufficient and necessary barrier-like conditions for safety and reach-avoid verification of stochastic discrete-time systems,

B. Xue, “Sufficient and necessary barrier-like conditions for safety and reach-avoid verification of stochastic discrete-time systems,” arXiv preprint arXiv:2408.15572, 2024

arXiv 2024
[18]

K-inductive barrier certificates for stochastic systems,

M. Anand, V . Murali, A. Trivedi, and M. Zamani, “K-inductive barrier certificates for stochastic systems,” in Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control , pp. 1–11, 2022

work page 2022
[23]

Supermartingale certificates for quantitative omega-regular verification and control,

T. A. Henzinger, K. Mallik, P. Sadeghi, and D. Zikelic, “Supermartingale certificates for quantitative omega-regular verification and control,” in International Conference on Computer Aided Verification , Springer, 2025

work page 2025
[14]

Finite-time safety and reach-avoid verification of stochastic discrete-time systems,

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

arXiv 2024
[1]

Formal Methods for Control Synthesis: An Optimization Perspective,

C. Belta and S. Sadraddini, “Formal Methods for Control Synthesis: An Optimization Perspective,” Annual Review of Control, Robotics, and Autonomous Systems, vol. 2, no. 1, pp. 115–140, 2019

work page 2019
[2]

Automated verifica- tion and synthesis of stochastic hybrid systems: A survey,

A. Lavaei, S. Soudjani, A. Abate, and M. Zamani, “Automated verifica- tion and synthesis of stochastic hybrid systems: A survey,” Automatica, vol. 146, p. 110617, 2022

work page 2022
[3]

Formal synthesis of controllers for safety- critical autonomous systems: Developments and challenges,

X. Yin, B. Gao, and X. Yu, “Formal synthesis of controllers for safety- critical autonomous systems: Developments and challenges,” Annual Reviews in Control, vol. 57, p. 100940, 2024

work page 2024
[4]

Probabilistic reacha- bility and safety for controlled discrete time stochastic hybrid systems,

A. Abate, M. Prandini, J. Lygeros, and S. Sastry, “Probabilistic reacha- bility and safety for controlled discrete time stochastic hybrid systems,” Automatica, vol. 44, no. 11, pp. 2724–2734, 2008. 9 TABLE I UPPER BOUND OF UNSAFE PROBABILITY 1 − SAx0 (S) BY DIFFERENT BARRIER CERTIFICATES UNDER DIFFERENT α IN EXAMPLE 1 α value 0.99 0 .992 0 .994 0 .996 0 ....

work page 2008

Show all 31 references

[5]

Precise approximations of the probability distribution of a markov process in time: an application to probabilistic invariance,

S. Esmaeil Zadeh Soudjani and A. Abate, “Precise approximations of the probability distribution of a markov process in time: an application to probabilistic invariance,” in 20th International Conference, TACAS , pp. 547–561, Springer, 2014

2014
[6]

Automata-based controller synthesis for stochastic systems: A game framework via approximate probabilistic relations,

B. Zhong, A. Lavaei, M. Zamani, and M. Caccamo, “Automata-based controller synthesis for stochastic systems: A game framework via approximate probabilistic relations,” Automatica, vol. 147, p. 110696, 2023

2023
[7]

A framework for worst- case and stochastic safety verification using barrier certificates,

S. Prajna, A. Jadbabaie, and G. J. Pappas, “A framework for worst- case and stochastic safety verification using barrier certificates,” IEEE Transactions on Automatic Control, vol. 52, no. 8, pp. 1415–1428, 2007

2007
[8]

Data-driven safety verification of stochas- tic systems via barrier certificates: A wait-and-judge approach,

A. Salamati and M. Zamani, “Data-driven safety verification of stochas- tic systems via barrier certificates: A wait-and-judge approach,” in Learning for Dynamics and Control Conference , pp. 441–452, PMLR, 2022

2022
[9]

Formal verification of unknown discrete-and continuous-time systems: A data- driven approach,

A. Nejati, A. Lavaei, P. Jagtap, S. Soudjani, and M. Zamani, “Formal verification of unknown discrete-and continuous-time systems: A data- driven approach,” IEEE Transactions on Automatic Control , vol. 68, no. 5, pp. 3011–3024, 2023

2023
[10]

Stochastic safety analysis of stochastic hybrid systems,

R. Wisniewski and M. L. Bujorianu, “Stochastic safety analysis of stochastic hybrid systems,” in 2017 IEEE 56th Annual Conference on Decision and Control (CDC) , pp. 2390–2395, 2017

2017
[11]

Probabilistic safety verification of stochastic hybrid systems using barrier certificates,

C. Huang, X. Chen, W. Lin, Z. Yang, and X. Li, “Probabilistic safety verification of stochastic hybrid systems using barrier certificates,” ACM Trans. Embed. Comput. Syst. , vol. 16, no. 5s, 2017

2017
[12]

Finite-time regional verification of stochastic non-linear systems,

J. Steinhardt and R. Tedrake, “Finite-time regional verification of stochastic non-linear systems,” The International Journal of Robotics Research, vol. 31, no. 7, pp. 901–923, 2012

2012
[13]

A barrier function approach to finite-time stochastic system verification and control,

C. Santoyo, M. Dutreix, and S. Coogan, “A barrier function approach to finite-time stochastic system verification and control,” Automatica, vol. 125, p. 109439, 2021

2021
[15]

Temporal logic verification of stochastic systems using barrier certificates,

P. Jagtap, S. Soudjani, and M. Zamani, “Temporal logic verification of stochastic systems using barrier certificates,” in International Symposium on Automated Technology for Verification and Analysis , pp. 177–193, Springer, 2018

2018
[16]

Data-driven distributionally robust safety verification using barrier certificates and conditional mean embeddings,

O. Sch ¨on, Z. Zhong, and S. Soudjani, “Data-driven distributionally robust safety verification using barrier certificates and conditional mean embeddings,” in 2024 American Control Conference (ACC) , pp. 3417– 3423, IEEE, 2024

2024
[17]

Distributionally robust control syn- thesis for stochastic systems with safety and reach-avoid specifications,

Y . Chen, Y . Li, S. Li, and X. Yin, “Distributionally robust control syn- thesis for stochastic systems with safety and reach-avoid specifications,” arXiv preprint arXiv:2501.03137 , 2025

2025
[19]

Learning control policies for stochastic systems with reach-avoid guarantees,

D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “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

2023
[21]

Stochastic lyapunov-barrier functions for robust probabilistic reach-avoid-stay specifications,

Y . Meng and J. Liu, “Stochastic lyapunov-barrier functions for robust probabilistic reach-avoid-stay specifications,” IEEE Transactions on Automatic Control, vol. 69, no. 8, pp. 5470–5477, 2024

2024
[22]

Quantitative supermartingale cer- tificates,

A. Abate, M. Giacobbe, and D. Roy, “Quantitative supermartingale cer- tificates,” in International Conference on Computer Aided Verification , Springer, 2025

2025
[24]

Unifying safety approaches for stochas- tic systems: From barrier functions to uncertain abstractions via dynamic programming,

L. Laurenti and M. Lahijanian, “Unifying safety approaches for stochas- tic systems: From barrier functions to uncertain abstractions via dynamic programming,” arXiv preprint arXiv:2310.01802 , 2024

2024 arXiv
[25]

Bertsekas and S

D. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, vol. 5. Athena Scientific, 1996

1996
[26]

Verification of discrete time stochastic 10 hybrid systems: A stochastic reach-avoid decision problem,

S. Summers and J. Lygeros, “Verification of discrete time stochastic 10 hybrid systems: A stochastic reach-avoid decision problem,”Automatica, vol. 46, no. 12, pp. 1951–1961, 2010

1951
[27]

H. J. Kushner, Stochastic stability and control . ACADEMIC PRESS, INC., 1967

1967
[28]

Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones,

J. F. Sturm, “Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones,” Optimization Methods and Software , vol. 11, no. 1-4, pp. 625–653, 1999

1999
[29]

Introducing SOS- TOOLS: A general purpose sum of squares programming solver,

S. Prajna, A. Papachristodoulou, and P. A. Parrilo, “Introducing SOS- TOOLS: A general purpose sum of squares programming solver,” in 41st IEEE Conference on Decision and Control , pp. 741–746, IEEE, 2002

2002
[30]

Formal synthesis of stochastic systems via control barrier certificates,

P. Jagtap, S. Soudjani, and M. Zamani, “Formal synthesis of stochastic systems via control barrier certificates,” IEEE Transactions on Automatic Control, vol. 66, no. 7, pp. 3097–3110, 2020

2020
[31]

Secure-by-construction synthesis for control systems,

B. Zhong, S. Liu, M. Caccamo, and M. Zamani, “Secure-by-construction synthesis for control systems,” IEEE Transactions on Automatic Control, 2025

2025

Pith tools

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

[1] [20]

Sufficient and necessary barrier-like conditions for safety and reach-avoid verification of stochastic discrete-time systems,

B. Xue, “Sufficient and necessary barrier-like conditions for safety and reach-avoid verification of stochastic discrete-time systems,” arXiv preprint arXiv:2408.15572, 2024

arXiv 2024

[2] [18]

K-inductive barrier certificates for stochastic systems,

M. Anand, V . Murali, A. Trivedi, and M. Zamani, “K-inductive barrier certificates for stochastic systems,” in Proceedings of the 25th ACM International Conference on Hybrid Systems: Computation and Control , pp. 1–11, 2022

work page 2022

[3] [23]

Supermartingale certificates for quantitative omega-regular verification and control,

T. A. Henzinger, K. Mallik, P. Sadeghi, and D. Zikelic, “Supermartingale certificates for quantitative omega-regular verification and control,” in International Conference on Computer Aided Verification , Springer, 2025

work page 2025

[4] [14]

Finite-time safety and reach-avoid verification of stochastic discrete-time systems,

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

arXiv 2024

[5] [1]

Formal Methods for Control Synthesis: An Optimization Perspective,

C. Belta and S. Sadraddini, “Formal Methods for Control Synthesis: An Optimization Perspective,” Annual Review of Control, Robotics, and Autonomous Systems, vol. 2, no. 1, pp. 115–140, 2019

work page 2019

[6] [2]

Automated verifica- tion and synthesis of stochastic hybrid systems: A survey,

A. Lavaei, S. Soudjani, A. Abate, and M. Zamani, “Automated verifica- tion and synthesis of stochastic hybrid systems: A survey,” Automatica, vol. 146, p. 110617, 2022

work page 2022

[7] [3]

Formal synthesis of controllers for safety- critical autonomous systems: Developments and challenges,

X. Yin, B. Gao, and X. Yu, “Formal synthesis of controllers for safety- critical autonomous systems: Developments and challenges,” Annual Reviews in Control, vol. 57, p. 100940, 2024

work page 2024

[8] [4]

Probabilistic reacha- bility and safety for controlled discrete time stochastic hybrid systems,

A. Abate, M. Prandini, J. Lygeros, and S. Sastry, “Probabilistic reacha- bility and safety for controlled discrete time stochastic hybrid systems,” Automatica, vol. 44, no. 11, pp. 2724–2734, 2008. 9 TABLE I UPPER BOUND OF UNSAFE PROBABILITY 1 − SAx0 (S) BY DIFFERENT BARRIER CERTIFICATES UNDER DIFFERENT α IN EXAMPLE 1 α value 0.99 0 .992 0 .994 0 .996 0 ....

work page 2008