pith. sign in

arxiv: 2605.03595 · v1 · submitted 2026-05-05 · 📡 eess.SY · cs.SY

Almost Sure Reachability in Continuous-time Stochastic Systems

Arash Bahari Kordabad , Rupak Majumdar , Sadegh Soudjani This is my paper

Pith reviewed 2026-05-07 13:53 UTC · model grok-4.3

classification 📡 eess.SY cs.SY
keywords almost sure reachabilitystochastic differential equationssum-of-squaresdrift functionvariant functioncontinuous-time systemscertificates
0
0 comments X

The pith

A drift function and a variant function together give necessary and sufficient certificates for almost sure reachability in continuous-time stochastic differential equations.

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

The paper shows that standard time-discretization schemes such as Euler-Maruyama can destroy almost sure reachability even when the original continuous-time system possesses the property, using a double-well Langevin example. To address this, it introduces two scalar functions whose Lie derivatives along the SDE satisfy explicit inequalities and boundary conditions. These functions certify that an open bounded target set is reached with probability one from every initial state, and the paper proves both directions of the equivalence. For linear systems the certificates reduce to spectral conditions on the drift and diffusion matrices; for polynomial systems they are encoded as sum-of-squares constraints solved by an alternating scheme that handles the resulting bilinearities.

Core claim

An open bounded set T is almost surely reachable for the continuous-time SDE if and only if there exist a drift function V and a variant function W such that the generator applied to V is non-positive outside T, the generator applied to W is strictly negative outside T, V is zero on T and positive outside, and W is bounded below and tends to infinity at the boundary of the domain.

What carries the argument

The pair consisting of a drift function V and a variant function W; V enforces non-increase of expected value outside the target while W forces strict progress toward the target in finite expected time.

If this is right

  • For linear SDEs almost sure reachability is completely determined by the eigenvalues of the drift matrix and the rank of the diffusion matrix.
  • Polynomial SDEs can be verified automatically by converting the certificate conditions into a sequence of sum-of-squares programs.
  • The certificates remain valid under the original continuous-time dynamics and therefore detect reachability that is lost after Euler-Maruyama discretization.
  • An alternating minimization procedure resolves the bilinear terms that appear when both functions are optimized simultaneously.

Where Pith is reading between the lines

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

  • The same certificate style may extend to almost-sure invariance or finite-time reachability by altering the sign conditions on the generators.
  • Because the certificates are stated directly on the infinitesimal generator, they apply unchanged to Itô processes with non-polynomial coefficients once suitable function templates are chosen.
  • Control synthesis problems could be solved by searching for a feedback law that renders the closed-loop drift and variant functions feasible.

Load-bearing premise

Suitable drift and variant functions exist for the system under study and the chosen function templates are rich enough to find them when they do exist.

What would settle it

A concrete continuous-time SDE for which the target set is reached with probability one, yet no pair of continuously differentiable functions V and W satisfies the four listed inequalities and boundary conditions simultaneously.

Figures

Figures reproduced from arXiv: 2605.03595 by Arash Bahari Kordabad, Rupak Majumdar, Sadegh Soudjani.

Figure 1
Figure 1. Figure 1: Illustration of the layered sets Bn (left) and Gn (right) used in the proof. Left: Bn collects all states from which the process can reach the target set G within time nτ with positive probability. Right: Gn includes Gn−1 and all states that reach Gn−1 within time τ with probability exceeding 2 −n . In both constructions, the layers expand outward until they cover the entire state space. Since (ONM )M≥0 is… view at source ↗
Figure 2
Figure 2. Figure 2: Empirical cumulative distribution function of the view at source ↗
Figure 5
Figure 5. Figure 5: Generator view at source ↗
Figure 6
Figure 6. Figure 6: One-step decrease probability P(U(x(τ )) − U(x) ≤ −δ) over the region {U(x) > 0}. The red marker indicates the minimum probability over {x : U(x) > 0}. trolled SDEs and certificates for safety specifications and quantitative properties. References [1] B. Øksendal, Stochastic differential equations, in: Stochastic differential equations: an introduction with applications, Springer, 2003, pp. 38–50. [2] M. P… view at source ↗
read the original abstract

We provide certificates for almost sure reachability of continuous-time stochastic systems governed by stochastic differential equations (SDEs). We first show that a standard Euler-Maruyama discretization may fail to preserve almost sure reachability property of the system using a double-well Langevin system. This observation motivates us to develop certificates for almost sure reachability directly on the continuous-time system. We introduce a pair of certificates, a drift function and a variant function, and prove necessity and sufficiency for almost sure reachability of an open bounded target set. Using these certificates, for linear SDEs, we give a characterization of almost sure reachability in terms of the spectral structure of the system matrices. For polynomial SDEs, we fix a polynomial template for the drift function and choose the variant function template as an exponential function composed with a polynomial. This allows us to translate the conditions in the certificates into sum-of-squares (SOS) constraints. We then propose an alternating scheme to resolve bilinearities. We illustrate the approach on the double-well Langevin example, showing that continuous-time SOS certificates recover almost sure reachability that is lost under time discretization. Moreover, we verify the SOS approach on a polynomial system.

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.

Referee Report

2 major / 2 minor

Summary. The paper claims to provide certificates for almost sure reachability of open bounded target sets in continuous-time SDEs via a pair of drift and variant functions, proving these are necessary and sufficient. It shows via a double-well Langevin example that Euler-Maruyama discretization can fail to preserve the property. For linear SDEs a spectral characterization of the system matrices is given; for polynomial SDEs the certificates are translated to SOS constraints using a polynomial template for the drift function and an exponential-of-polynomial template for the variant function, with an alternating solver to handle the resulting bilinearities. The SOS method is demonstrated on the motivating example and another polynomial system.

Significance. If the necessity and sufficiency proofs for the certificates hold, the work supplies a direct continuous-time tool for certifying almost sure reachability that sidesteps discretization artifacts, which is valuable for stochastic verification and control. The concrete counterexample to discretization is useful, and the SOS procedure offers a computable route for polynomial systems when the templates succeed. The spectral result for linear systems is a clean specialization.

major comments (2)
  1. [section on polynomial SDEs] In the section on polynomial SDEs (where the SOS constraints are derived from the generator inequalities): necessity and sufficiency are established for arbitrary (sufficiently regular) drift and variant functions, yet the computational method restricts to a fixed polynomial template for the drift and an exponential-of-polynomial template for the variant. No density, completeness, or expressiveness argument is supplied showing that these templates can represent all required certificates; consequently the SOS program (even with alternation) can return infeasible for systems that satisfy almost sure reachability, producing false negatives that the necessity direction does not preclude. This is load-bearing for the practical claims of the SOS approach.
  2. [linear SDEs section] In the linear SDEs section (spectral characterization): the equivalence between the spectral conditions on the system matrices and the existence of the drift/variant certificates is asserted, but the derivation should explicitly confirm that the spectral criteria are both necessary and sufficient without hidden regularity assumptions on the diffusion term or the target set.
minor comments (2)
  1. Clarify in the preliminaries or certificate section the precise regularity conditions (e.g., on the SDE coefficients and the functions themselves) under which the necessity and sufficiency statements hold.
  2. The alternating solver for the bilinear SOS constraints lacks any convergence analysis or termination criterion; a brief remark on practical behavior or a reference to related bilinear SOS solvers would improve reproducibility.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed comments on our manuscript. We address each major comment point by point below. Where revisions are needed to clarify limitations or make derivations explicit, we will incorporate them in the revised version.

read point-by-point responses

  1. Referee: [section on polynomial SDEs] In the section on polynomial SDEs (where the SOS constraints are derived from the generator inequalities): necessity and sufficiency are established for arbitrary (sufficiently regular) drift and variant functions, yet the computational method restricts to a fixed polynomial template for the drift and an exponential-of-polynomial template for the variant. No density, completeness, or expressiveness argument is supplied showing that these templates can represent all required certificates; consequently the SOS program (even with alternation) can return infeasible for systems that satisfy almost sure reachability, producing false negatives that the necessity direction does not preclude. This is load-bearing for the practical claims of the SOS approach.

    Authors: We agree that the specific polynomial and exponential-of-polynomial templates used for the SOS formulation lack a completeness or density argument. While the general drift and variant certificates are proven necessary and sufficient for arbitrary sufficiently regular functions, the computational procedure is not guaranteed to recover a certificate even when one exists. This can indeed lead to false negatives in practice. In the revision we will add an explicit discussion of this limitation, clarifying that the SOS method yields a sufficient condition for certifying almost sure reachability when a solution to the template-based program is found, but does not claim to be complete. We will also note that the templates were chosen for computational tractability and have succeeded on the examples considered, while acknowledging that broader expressiveness results remain open. revision: yes

  2. Referee: [linear SDEs section] In the linear SDEs section (spectral characterization): the equivalence between the spectral conditions on the system matrices and the existence of the drift/variant certificates is asserted, but the derivation should explicitly confirm that the spectral criteria are both necessary and sufficient without hidden regularity assumptions on the diffusion term or the target set.

    Authors: The spectral characterization is obtained by direct specialization of the general necessary-and-sufficient drift/variant conditions to the linear case, using the same standing assumptions (open bounded target set and standard Lipschitz/linear-growth conditions on the coefficients). No additional regularity is imposed on the diffusion term. In the revised manuscript we will expand the derivation to explicitly trace each step from the general theorems to the spectral criteria, confirming necessity and sufficiency at every stage and reiterating the precise assumptions carried over from the general setting. revision: yes

Circularity Check

0 steps flagged

No circularity: certificates and proofs are self-contained from the generator

full rationale

The derivation begins by defining the drift and variant functions directly via the infinitesimal generator of the SDE (standard Itô calculus). Necessity and sufficiency are proved mathematically for almost-sure reachability of an open bounded set without reference to fitted data or the target reachability property itself. The linear-system spectral characterization follows from applying the same generator-based conditions to the matrix form and is independent of the reachability claim. The polynomial case selects explicit templates (polynomial drift, exp-polynomial variant) and converts the inequalities to SOS constraints solved by alternation; this is an algorithmic restriction on the search space, not a redefinition or fitting of the certificates to the reachability outcome. No self-citation is load-bearing, no parameter is fitted to a subset and then called a prediction, and no step equates the claimed result to its own inputs by construction. The paper remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on standard SDE existence and uniqueness assumptions plus the existence of the new certificate functions; no free parameters are fitted to data in the abstract description.

axioms (1)
  • domain assumption The SDE admits unique strong solutions under standard Lipschitz and linear-growth conditions on the drift and diffusion coefficients.
    Invoked implicitly when defining the stochastic process and its infinitesimal generator.
invented entities (1)
  • Drift function and variant function pair no independent evidence
    purpose: To serve as certificates that are necessary and sufficient for almost sure reachability.
    These functions are newly introduced in the paper; no independent evidence outside the certificates themselves is provided.

pith-pipeline@v0.9.0 · 5511 in / 1407 out tokens · 52093 ms · 2026-05-07T13:53:42.366536+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

  1. [1]

    Øksendal, Stochastic differential equations, in: Stochastic differential equations: an introduction with applications, Springer, 2003, pp

    B. Øksendal, Stochastic differential equations, in: Stochastic differential equations: an introduction with applications, Springer, 2003, pp. 38–50

    work page 2003

  2. [2]

    Prandini, J

    M. Prandini, J. Hu, C. Cassandras, J. Lygeros, Stochastic reachability: Theory and numerical approximation, Stochastic hybrid systems, Automation and Control Engineering Series 24 (2006) 107–138

    work page 2006

  3. [3]

    Aristoff, J

    D. Aristoff, J. Copperman, G. Simpson, R. J. Webber, D. M. Zuckerman, Weighted ensemble: Recent mathematical developments, The Journal of chemical physics 158 (1) (2023)

    work page 2023

  4. [4]

    Majumdar, V

    R. Majumdar, V. Sathiyanarayana, S. Soudjani, Necessary and sufficient certificates for almost sure reachability, IEEE Control Systems Letters (2024)

    work page 2024

  5. [5]

    A. B. Kordabad, R. Majumdar, S. Soudjani, Sum-of- squares certificates for almost-sure reachability of stochastic polynomial systems, arXiv preprint arXiv:2510.25513 (2025). 15

    work page arXiv 2025

  6. [6]

    Ardourel, J

    V. Ardourel, J. Jebeile, Numerical instability and dynamical systems, European Journal for Philosophy of Science 11 (2) (2021) 49

    work page 2021

  7. [7]

    S. P. Meyn, R. L. Tweedie, Markov chains and stochastic stability, Springer Science & Business Media, 2012

    work page 2012

  8. [8]

    A. B. Kordabad, M. Charitidou, D. V. Dimarogonas, S. Soudjani, Control barrier functions for stochastic systems under signal temporal logic tasks, in: 2024 European Control Conference (ECC), IEEE, 2024, pp. 3213–3219

    work page 2024

  9. [9]

    Santoyo, M

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

    work page 2021

  10. [10]

    Clark, Control barrier functions for stochastic systems, Automatica 130 (2021) 109688

    A. Clark, Control barrier functions for stochastic systems, Automatica 130 (2021) 109688

    work page 2021

  11. [11]

    O. So, A. Clark, C. Fan, Almost-sure safety guarantees of stochastic zero-control barrier functions do not hold, arXiv preprint arXiv:2312.02430 (2023)

    work page arXiv 2023

  12. [12]

    Nishimura, K

    Y. Nishimura, K. Hoshino, Control barrier functions for stochastic systems and safety-critical control designs, IEEE Transactions on Automatic Control 69 (11) (2024) 8088– 8095

    work page 2024

  13. [13]

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

    work page 2021

  14. [14]

    Stochastic neural control barrier functions,

    H. Zhang, M. Tayal, J. Cox, P. Jagtap, S. Kolathaya, A. Clark, Stochastic neural control barrier functions, arXiv preprint arXiv:2506.21697 (2025)

    work page arXiv 2025

  15. [15]

    1783–1801

    M.Pereira,Z.Wang,I.Exarchos,E.Theodorou,Safeoptimal control using stochastic barrier functions and deep forward- backward SDEs, in: Conference on Robot Learning, PMLR, 2021, pp. 1783–1801

    work page 2021

  16. [16]

    Prajna, A

    S. Prajna, A. Rantzer, On the necessity of barrier certificates, IFAC Proceedings Volumes 38 (1) (2005) 526–531

    work page 2005

  17. [17]

    Ratschan, Converse theorems for safety and barrier certificates, IEEE Transactions on Automatic Control 63 (8) (2018) 2628–2632

    S. Ratschan, Converse theorems for safety and barrier certificates, IEEE Transactions on Automatic Control 63 (8) (2018) 2628–2632

    work page 2018

  18. [18]

    Z. Lyu, X. Xu, Y. Hong, L. Xie, On converse zeroing barrier functions, Automatica 172 (2025) 112011

    work page 2025

  19. [19]

    Chatterjee, P

    K. Chatterjee, P. Novotn` y, Ð. Žikelić, Stochastic invariants for probabilistic termination, in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017, pp. 145–160

    work page 2017

  20. [20]

    Chatterjee, A

    K. Chatterjee, A. K. Goharshady, T. Meggendorfer, Ð. Žikelić, Sound and complete certificates for quantitative termination analysis of probabilistic programs, in: International Conference on Computer Aided Verification, Springer, 2022, pp. 55–78

    work page 2022

  21. [21]

    Abate, M

    A. Abate, M. Giacobbe, D. Roy, Stochastic omega- regular verification and control with supermartingales, in: International Conference on Computer Aided Verification, Springer, 2024, pp. 395–419

    work page 2024

  22. [22]

    Anand, V

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

    work page 2022

  23. [23]

    Majumdar, V

    R. Majumdar, V. Sathiyanarayana, Sound and complete proof rules for probabilistic termination, Proceedings of the ACM on Programming Languages 9 (POPL) (2025) 1871– 1902

    work page 2025

  24. [24]

    A. B. Kordabad, R. Majumdar, H. J. Motwani, S. Soudjani, On certificates for almost sure reachability in stochastic systems, arXiv preprint arXiv:2507.20194 (2025)

    work page arXiv 2025

  25. [25]

    Bovier, F

    A. Bovier, F. Den Hollander, Metastability: a potential- theoretic approach, Springer, 2016

    work page 2016

  26. [26]

    Zhang, S

    H. Zhang, S. Gan, L. Hu, The split-step backward Euler method for linear stochastic delay differential equations, Journal of Computational and Applied Mathematics 225 (2) (2009) 558–568

    work page 2009

  27. [27]

    C.-E.Bréhier,Approximationoftheinvariantdistributionfor a class of ergodic SDEs with one-sided lipschitz continuous drift coefficient using an explicit tamed Euler scheme, ESAIM: Probability and Statistics 27 (2023) 841–866

    work page 2023

  28. [28]

    Xiang, Measure-valued flows given consistent exchangeable families, Acta applicandae mathematicae 105 (1) (2009) 1–44

    K.-N. Xiang, Measure-valued flows given consistent exchangeable families, Acta applicandae mathematicae 105 (1) (2009) 1–44

    work page 2009

  29. [29]

    H. D. Kwon, J. Palczewski, Exit game with private information, Mathematics of Operations Research 50 (4) (2025) 2433–2469

    work page 2025

  30. [30]

    S. P. Meyn, R. L. Tweedie, Stability of Markovian processes iii: Foster–Lyapunov criteria for continuous-time processes, Advances in Applied Probability 25 (3) (1993) 518–548

    work page 1993

  31. [31]

    D. Down, S. P. Meyn, R. L. Tweedie, Exponential and uniform ergodicity of Markov processes, The Annals of Probability 23 (4) (1995) 1671–1691

    work page 1995

  32. [32]

    J. L. Kelley, General topology, Courier Dover Publications, 2017

    work page 2017

  33. [33]

    B. K. Ghosh, Probability inequalities related to Markov’s theorem, The American Statistician 56 (3) (2002) 186–190

    work page 2002

  34. [34]

    Lindquist, G

    A. Lindquist, G. Picci, Linear stochastic systems, Series in Contemporary Mathematics 1 (2015) 26

    work page 2015

  35. [35]

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

    work page 2000

  36. [36]

    A. A. Ahmadi, P. A. Parrilo, A convex polynomial that is not SOS-convex, Mathematical Programming 135 (1) (2012) 275–292

    work page 2012

  37. [37]

    Zhang, C

    X.-J. Zhang, C. Shang, Z.-P. Liu, Double-ended surface walking method for pathway building and transition state location of complex reactions, Journal of Chemical Theory and Computation 9 (12) (2013) 5745–5753

    work page 2013

  38. [38]

    Aguilar-Mogas, X

    A. Aguilar-Mogas, X. Giménez, J. M. Bofill, Implementation of an algorithm based on the Runge-Kutta-Fehlberg technique and the potential energy as a reaction coordinate to locate intrinsic reaction paths, Journal of Computational Chemistry 31 (13) (2010) 2510–2525. 16

    work page 2010