Refined Barrier Conditions for Finite-Time Safety and Reach-Avoid Guarantees in Stochastic Systems

Bai Xue; Dominik Wagner; Luke Ong; Peixin Wang

arxiv: 2509.18518 · v2 · submitted 2025-09-23 · 📡 eess.SY · cs.SY

Refined Barrier Conditions for Finite-Time Safety and Reach-Avoid Guarantees in Stochastic Systems

Bai Xue , Luke Ong , Dominik Wagner , Peixin Wang This is my paper

Pith reviewed 2026-05-18 15:12 UTC · model grok-4.3

classification 📡 eess.SY cs.SY

keywords stochastic systemsbarrier conditionsfinite-time safetyreach-avoidprobabilistic verificationunbounded statesoptimization

0 comments

The pith

Refined barrier conditions remove the boundedness requirement for verifying finite-time safety and reach-avoid in stochastic systems.

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

This paper seeks to establish refined conditions using barrier functions that allow computation of probability bounds for systems to remain safe or to reach targets while avoiding danger over a finite time period. The key change is dropping the assumption that the auxiliary functions in these conditions must be bounded, which previously restricted the method to certain systems. A reader would care if true because it opens the door to proving safety for a larger set of stochastic systems, including those whose states can become arbitrarily large without bound, using standard optimization tools.

Core claim

The authors establish that refined barrier conditions without a boundedness assumption on the auxiliary functions suffice to derive upper bounds on the finite-time safety probability for discrete-time stochastic systems and lower bounds on the finite-time reach-avoid probability for continuous-time stochastic systems. These conditions expand the applicability to systems with unbounded state spaces and support the use of polynomial functions in semi-definite programming for certification.

What carries the argument

The refined barrier conditions, which are inequalities involving auxiliary functions that need not be bounded, serving to bound the probabilities of safety and reach-avoid events.

If this is right

Finite-time safety probabilities in discrete-time stochastic systems can be upper-bounded using the refined conditions.
Finite-time reach-avoid probabilities in continuous-time stochastic systems can be lower-bounded using the refined conditions.
Systems with unbounded state spaces become verifiable under these conditions.
Polynomial auxiliary functions and semi-definite programming can be employed to find or certify the conditions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The approach may enable formal safety proofs for models involving unbounded noise or open physical spaces that were previously out of reach.
Researchers could test the conditions on additional system classes to see how much the verifiable set expands in practice.

Load-bearing premise

Suitable auxiliary functions exist that satisfy the refined barrier inequalities for the stochastic system being analyzed.

What would settle it

A numerical example or simulation where the refined barrier conditions are satisfied yet the actual finite-time safety or reach-avoid probability falls outside the derived bound would disprove the claim.

read the original abstract

Providing finite-time probabilistic safety and reach-avoid guarantees is crucial for safety-critical stochastic systems. Existing state-of-the-art barrier methods often rely on a restrictive boundedness assumption for auxiliary functions, limiting their applicability. This paper presents refined barrier conditions that remove this assumption. Specifically, we establish conditions for deriving upper bounds on finite-time safety probabilities in discrete-time systems and lower bounds on finite-time reach-avoid probabilities in continuous-time systems. This relaxation expands the class of verifiable systems, especially those with unbounded state spaces, and facilitates the use of advanced optimization techniques, such as semi-definite programming with polynomial functions. Numerical examples demonstrate the effectiveness of the approach.

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note private letter to a colleague

The paper drops the boundedness requirement on auxiliary functions for finite-time stochastic safety and reach-avoid bounds, but the gain still depends on existence of suitable (unbounded) functions shown only in examples.

read the letter

The main point is that this work removes the boundedness assumption on the auxiliary function V in barrier conditions for stochastic systems. They give explicit inequalities that yield upper bounds on finite-time safety violation probabilities for discrete-time systems and lower bounds on reach-avoid probabilities for continuous-time systems, without requiring V to be bounded. This is positioned as a direct fix for systems with unbounded states, and they note it allows polynomial candidates with semidefinite programming. The numerical examples appear to run cleanly on the chosen polynomial systems via SDP, which is a practical plus for verification workflows that already use these tools. The derivations seem to follow by adjusting the one-step expectation or generator conditions to handle the unbounded case, and the abstract claims this expands the verifiable class. That part looks like a genuine relaxation relative to the cited prior barrier results. The soft spot is that the probability bounds hold only if a suitable V exists and can be found or certified. The paper provides no general existence theorem showing the relaxation is non-vacuous for systems where every bounded V fails, nor a constructive synthesis method beyond optimizing over specific polynomial degrees in the examples. If most systems of interest still lack such a V, the practical expansion is narrower than the headline suggests. This is for researchers already working on barrier certificates and stochastic safety verification in control theory. A reader familiar with the existing literature on finite-time probabilistic guarantees would see the value in the refined conditions and the SDP examples. It deserves a serious referee to verify the proof details and assess how much larger the set of certifiable systems actually becomes.

Referee Report

1 major / 2 minor

Summary. The paper proposes refined barrier conditions for stochastic systems that remove the standard boundedness assumption on auxiliary functions. For discrete-time systems, it derives conditions yielding upper bounds on finite-time safety probabilities; for continuous-time systems, it provides conditions for lower bounds on finite-time reach-avoid probabilities. The relaxation is claimed to expand the class of verifiable systems, especially those with unbounded state spaces, and is illustrated via numerical examples using semi-definite programming with polynomial functions.

Significance. If the derivations hold and the relaxation proves non-vacuous, the work could meaningfully broaden the applicability of barrier certificates to safety-critical stochastic systems with unbounded domains, where bounded auxiliary functions are often infeasible. The explicit use of polynomial candidates and SDP solvers in the examples is a practical strength that aligns with existing verification toolchains.

major comments (1)

[Abstract and main theoretical results] The central claim that the refined conditions expand the verifiable class (Abstract) rests on the existence of suitable, possibly unbounded auxiliary functions V satisfying the new inequalities, such as the one-step expectation condition for discrete-time safety or the generator-based inequalities for continuous-time reach-avoid. The proofs establish the probability bounds conditional on such a V existing and being found, but provide no general existence theorem or constructive synthesis procedure beyond the specific numerical SDP examples with polynomial candidates. This leaves the expansion claim conditional rather than unconditional.

minor comments (2)

Notation for the refined barrier inequalities could be clarified with explicit comparison to the standard bounded versions to highlight the precise relaxation.
The numerical examples section would benefit from a brief discussion of how the polynomial degree and SDP solver tolerances were chosen to ensure the reported bounds are tight.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their constructive review and for highlighting an important aspect of our theoretical claims. We address the major comment below and have incorporated clarifications into the revised manuscript.

read point-by-point responses

Referee: [Abstract and main theoretical results] The central claim that the refined conditions expand the verifiable class (Abstract) rests on the existence of suitable, possibly unbounded auxiliary functions V satisfying the new inequalities, such as the one-step expectation condition for discrete-time safety or the generator-based inequalities for continuous-time reach-avoid. The proofs establish the probability bounds conditional on such a V existing and being found, but provide no general existence theorem or constructive synthesis procedure beyond the specific numerical SDP examples with polynomial candidates. This leaves the expansion claim conditional rather than unconditional.

Authors: We agree that the theorems provide sufficient conditions: if a function V (possibly unbounded) satisfying the refined inequalities exists, then the stated probability bounds follow. This structure is standard for barrier-certificate results. The contribution of the paper lies in showing that the boundedness assumption can be removed without invalidating the proofs, thereby strictly enlarging the set of systems for which a certificate may exist. In particular, for systems defined on unbounded domains, bounded auxiliary functions are often infeasible, whereas unbounded polynomial candidates can satisfy the new conditions, as demonstrated by the SDP-synthesized examples. We do not claim a general existence result, which would constitute a separate and typically undecidable question; our focus is on the relaxed sufficient conditions and on practical synthesis via existing optimization tools. To make this distinction explicit, we will revise the abstract and the opening of Section 3 to state that the expansion concerns the class of systems admitting (possibly unbounded) certificates rather than an unconditional guarantee of existence for every system. revision: partial

Circularity Check

0 steps flagged

No circularity: refined barrier conditions derive probability bounds from auxiliary-function inequalities without self-referential reduction.

full rationale

The paper presents theorems establishing that if an auxiliary function V (possibly unbounded) satisfies certain refined inequalities involving one-step expectations (discrete-time) or the infinitesimal generator (continuous-time), then finite-time safety or reach-avoid probability bounds follow. These implications are proved directly from the definitions of the stochastic processes and the inequalities; the bounds are not obtained by fitting parameters to data or by renaming the input conditions. No load-bearing step reduces to a self-citation chain, an ansatz smuggled from prior work, or a uniqueness theorem imported from the authors themselves. The existence of suitable V is treated as an assumption to be verified per system (via SDP in the examples), but the derivation of the bounds conditional on that assumption is logically independent of the assumption itself. The work therefore remains self-contained against external benchmarks and does not exhibit any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on standard assumptions from stochastic processes and control theory plus the existence of auxiliary functions satisfying the new inequalities. No free parameters or invented entities are introduced in the abstract.

axioms (1)

domain assumption Standard assumptions on the stochastic system dynamics (Markov property, existence of transition kernels) as background for discrete- and continuous-time models.
Invoked implicitly when stating finite-time safety and reach-avoid probabilities.

pith-pipeline@v0.9.0 · 5640 in / 1161 out tokens · 31829 ms · 2026-05-18T15:12:31.887831+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

32 extracted references · 32 canonical work pages

[1]

Abate, M

A. Abate, M. Giacobbe, and D. Roy. Stochastic omega-regular verifica- tion and control with supermartingales. InInternational Conference on Computer Aided Verification, pages 395–419. Springer, 2024

work page 2024
[2]

Alur.Principles of cyber-physical systems

R. Alur.Principles of cyber-physical systems. MIT press, 2015

work page 2015
[3]

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

work page 2019
[4]

Baier and J.-P

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

work page 2008
[5]

Chakarov and S

A. Chakarov and S. Sankaranarayanan. Probabilistic program analysis with martingales. InComputer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25, pages 511–526. Springer, 2013

work page 2013
[6]

Chatterjee, A

K. Chatterjee, A. K. Goharshady, T. Meggendorfer, and Ð. Žikeli ´c. Quantitative bounds on resource usage of probabilistic programs.Pro- ceedings of the ACM on Programming Languages, 8(OOPSLA1):362– 391, 2024

work page 2024
[7]

Y . Chen, S. Li, and X. Yin. On the construction of barrier certificate: A dynamic programming perspective.arXiv preprint arXiv:2507.17222, 2025. (9) withα= 1.1 d 2 4 6 8 10 12 ϵ1 0.9997 0.9986 0.9983 0.9886 0.9103 0.8202 (4) withα= 1.1,β= 0, and ˜X={(x, y) ⊤ |x 2 +y 2 ≤30} d 2 4 6 8 10 12 ϵ1 1.0000 1.0000 1.0000 1.0000 0.9790 0.9445 TABLE II: Computed up...

work page arXiv 2025
[8]

Ghanbarpour and S

M. Ghanbarpour and S. Sankaranarayanan. Characterization of safety in stochastic difference inclusions using barrier functions.arXiv preprint arXiv:2508.20204, 2025

work page arXiv 2025
[9]

Jagtap, S

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

work page 2018
[10]

Jagtap, S

P. Jagtap, S. Soudjani, and M. Zamani. Formal synthesis of stochastic systems via control barrier certificates.IEEE Transactions on Automatic Control, 66(7):3097–3110, 2020

work page 2020
[11]

Kenyon-Roberts and C.-H

A. Kenyon-Roberts and C.-H. L. Ong. Supermartingales, ranking functions and probabilistic lambda calculus. In2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13. IEEE, 2021

work page 2021
[12]

P. R. Kumar and P. Varaiya.Stochastic systems: Estimation, identifica- tion, and adaptive control. SIAM, 2015

work page 2015
[13]

S. Kura, N. Urabe, and I. Hasuo. Tail probabilities for randomized program runtimes via martingales for higher moments. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 135–153. Springer, 2019

work page 2019
[14]

H. J. Kushner.Stochastic stability and control. New York: Academic, 1967

work page 1967
[15]

F. B. Mathiesen, S. C. Calvert, and L. Laurenti. Safety certification for stochastic systems via neural barrier functions.IEEE Control Systems Letters, 7:973–978, 2022

work page 2022
[16]

McIver, C

A. McIver, C. Morgan, B. L. Kaminski, and J.-P. Katoen. A new proof rule for almost-sure termination.Proceedings of the ACM on Programming Languages, 2(POPL):1–28, 2017

work page 2017
[17]

Oksendal.Stochastic differential equations: an introduction with applications

B. Oksendal.Stochastic differential equations: an introduction with applications. Springer Science & Business Media, 2013

work page 2013
[18]

Prajna and A

S. Prajna and A. Jadbabaie. Safety verification of hybrid systems using barrier certificates. InInternational Workshop on Hybrid Systems: Computation and Control, pages 477–492. Springer, 2004

work page 2004
[19]

Prajna, A

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, 52(8):1415–1428, 2007

work page 2007
[20]

Prajna and A

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

work page 2007
[21]

Santoyo, M

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

work page 2021
[22]

Steinhardt and R

J. Steinhardt and R. Tedrake. Finite-time regional verification of stochastic non-linear systems.The International Journal of Robotics Research, 31(7):901–923, 2012

work page 2012
[23]

C. Wang, Y . Meng, S. L. Smith, and J. Liu. Safety-critical control of stochastic systems using stochastic control barrier functions. In2021 60th IEEE Conference on Decision and Control (CDC), pages 5924–

work page
[24]

P. Wang, J. Bai, D. Zhi, M. Zhang, and L. Ong. Verifying omega-regular properties of neural network-controlled systems via proof certificates. In ICLR 2025 Workshop: VerifAI: AI Verification in the Wild

work page 2025
[25]

B. Xue. A new framework for bounding reachability probabilities of continuous-time stochastic systems.arXiv preprint arXiv:2312.15843, 2023

work page arXiv 2023
[26]

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

work page arXiv 2024
[27]

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

work page arXiv 2024
[28]

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

work page 2021
[29]

B. Xue, N. Zhan, and M. Fränzle. Reach-avoid analysis for polynomial stochastic differential equations.IEEE Transactions on Automatic Control, 69(3):1882–1889, 2024

work page 2024
[30]

Y . Yu, T. Wu, B. Xia, J. Wang, and B. Xue. Safe probabilistic invariance verification for stochastic discrete-time dynamical systems. In2023 62nd IEEE Conference on Decision and Control (CDC), pages 5804–5811. IEEE, 2023

work page 2023
[31]

D. Zhi, P. Wang, S. Liu, C.-H. L. Ong, and M. Zhang. Unifying qualitative and quantitative safety verification of dnn-controlled systems. InInternational Conference on Computer Aided Verification, pages 401–

work page
[32]

Žikeli ´c, M

Ð. Žikeli ´c, 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- ume 37, pages 11926–11935, 2023. VI. APPENDIX Proposition 5.Suppose there exist a barrier function v(t,x): [0, T]×R n →Rand a functionw(t): [0, T]...

work page 2023

[1] [1]

Abate, M

A. Abate, M. Giacobbe, and D. Roy. Stochastic omega-regular verifica- tion and control with supermartingales. InInternational Conference on Computer Aided Verification, pages 395–419. Springer, 2024

work page 2024

[2] [2]

Alur.Principles of cyber-physical systems

R. Alur.Principles of cyber-physical systems. MIT press, 2015

work page 2015

[3] [3]

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

work page 2019

[4] [4]

Baier and J.-P

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

work page 2008

[5] [5]

Chakarov and S

A. Chakarov and S. Sankaranarayanan. Probabilistic program analysis with martingales. InComputer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25, pages 511–526. Springer, 2013

work page 2013

[6] [6]

Chatterjee, A

K. Chatterjee, A. K. Goharshady, T. Meggendorfer, and Ð. Žikeli ´c. Quantitative bounds on resource usage of probabilistic programs.Pro- ceedings of the ACM on Programming Languages, 8(OOPSLA1):362– 391, 2024

work page 2024

[7] [7]

Y . Chen, S. Li, and X. Yin. On the construction of barrier certificate: A dynamic programming perspective.arXiv preprint arXiv:2507.17222, 2025. (9) withα= 1.1 d 2 4 6 8 10 12 ϵ1 0.9997 0.9986 0.9983 0.9886 0.9103 0.8202 (4) withα= 1.1,β= 0, and ˜X={(x, y) ⊤ |x 2 +y 2 ≤30} d 2 4 6 8 10 12 ϵ1 1.0000 1.0000 1.0000 1.0000 0.9790 0.9445 TABLE II: Computed up...

work page arXiv 2025

[8] [8]

Ghanbarpour and S

M. Ghanbarpour and S. Sankaranarayanan. Characterization of safety in stochastic difference inclusions using barrier functions.arXiv preprint arXiv:2508.20204, 2025

work page arXiv 2025

[9] [9]

Jagtap, S

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

work page 2018

[10] [10]

Jagtap, S

P. Jagtap, S. Soudjani, and M. Zamani. Formal synthesis of stochastic systems via control barrier certificates.IEEE Transactions on Automatic Control, 66(7):3097–3110, 2020

work page 2020

[11] [11]

Kenyon-Roberts and C.-H

A. Kenyon-Roberts and C.-H. L. Ong. Supermartingales, ranking functions and probabilistic lambda calculus. In2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13. IEEE, 2021

work page 2021

[12] [12]

P. R. Kumar and P. Varaiya.Stochastic systems: Estimation, identifica- tion, and adaptive control. SIAM, 2015

work page 2015

[13] [13]

S. Kura, N. Urabe, and I. Hasuo. Tail probabilities for randomized program runtimes via martingales for higher moments. InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 135–153. Springer, 2019

work page 2019

[14] [14]

H. J. Kushner.Stochastic stability and control. New York: Academic, 1967

work page 1967

[15] [15]

F. B. Mathiesen, S. C. Calvert, and L. Laurenti. Safety certification for stochastic systems via neural barrier functions.IEEE Control Systems Letters, 7:973–978, 2022

work page 2022

[16] [16]

McIver, C

A. McIver, C. Morgan, B. L. Kaminski, and J.-P. Katoen. A new proof rule for almost-sure termination.Proceedings of the ACM on Programming Languages, 2(POPL):1–28, 2017

work page 2017

[17] [17]

Oksendal.Stochastic differential equations: an introduction with applications

B. Oksendal.Stochastic differential equations: an introduction with applications. Springer Science & Business Media, 2013

work page 2013

[18] [18]

Prajna and A

S. Prajna and A. Jadbabaie. Safety verification of hybrid systems using barrier certificates. InInternational Workshop on Hybrid Systems: Computation and Control, pages 477–492. Springer, 2004

work page 2004

[19] [19]

Prajna, A

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, 52(8):1415–1428, 2007

work page 2007

[20] [20]

Prajna and A

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

work page 2007

[21] [21]

Santoyo, M

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

work page 2021

[22] [22]

Steinhardt and R

J. Steinhardt and R. Tedrake. Finite-time regional verification of stochastic non-linear systems.The International Journal of Robotics Research, 31(7):901–923, 2012

work page 2012

[23] [23]

C. Wang, Y . Meng, S. L. Smith, and J. Liu. Safety-critical control of stochastic systems using stochastic control barrier functions. In2021 60th IEEE Conference on Decision and Control (CDC), pages 5924–

work page

[24] [24]

P. Wang, J. Bai, D. Zhi, M. Zhang, and L. Ong. Verifying omega-regular properties of neural network-controlled systems via proof certificates. In ICLR 2025 Workshop: VerifAI: AI Verification in the Wild

work page 2025

[25] [25]

B. Xue. A new framework for bounding reachability probabilities of continuous-time stochastic systems.arXiv preprint arXiv:2312.15843, 2023

work page arXiv 2023

[26] [26]

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

work page arXiv 2024

[27] [27]

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

work page arXiv 2024

[28] [28]

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

work page 2021

[29] [29]

B. Xue, N. Zhan, and M. Fränzle. Reach-avoid analysis for polynomial stochastic differential equations.IEEE Transactions on Automatic Control, 69(3):1882–1889, 2024

work page 2024

[30] [30]

Y . Yu, T. Wu, B. Xia, J. Wang, and B. Xue. Safe probabilistic invariance verification for stochastic discrete-time dynamical systems. In2023 62nd IEEE Conference on Decision and Control (CDC), pages 5804–5811. IEEE, 2023

work page 2023

[31] [31]

D. Zhi, P. Wang, S. Liu, C.-H. L. Ong, and M. Zhang. Unifying qualitative and quantitative safety verification of dnn-controlled systems. InInternational Conference on Computer Aided Verification, pages 401–

work page

[32] [32]

Žikeli ´c, M

Ð. Žikeli ´c, 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- ume 37, pages 11926–11935, 2023. VI. APPENDIX Proposition 5.Suppose there exist a barrier function v(t,x): [0, T]×R n →Rand a functionw(t): [0, T]...

work page 2023