pith. sign in

arxiv: 2604.19014 · v1 · submitted 2026-04-21 · 📡 eess.SY · cs.SY

Quantitative Verification of Finite-Time Constrained Occupation Measures for Continuous-time Stochastic Systems

Bai Xue , C.-H. Luke Ong This is my paper

Pith reviewed 2026-05-10 02:32 UTC · model grok-4.3

classification 📡 eess.SY cs.SY
keywords barrier certificatesstochastic differential equationsoccupation measuresquantitative verificationfinite-time analysissafety constraintsstopped processes
0
0 comments X

The pith

A stopped-process barrier certificate method provides upper and lower bounds on finite-time constrained occupation probabilities for SDEs.

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

The paper aims to verify whether stochastic continuous-time systems governed by SDEs can satisfy requirements to accumulate a prescribed duration inside a safe target region without exiting it, over a finite time horizon. Unlike standard reachability that checks single events, this targets cumulative specifications needed for tasks such as surveillance or chemical mixing. It develops a barrier-certificate framework that introduces a stopped process freezing the dynamics at the safe-set boundary. This construction yields one class of certificates for upper bounds and two for lower bounds on the probability of satisfying the full specification. The bounds are obtained by solving semidefinite programs, with validation on numerical examples.

Core claim

By introducing a stopped process that freezes the system once it reaches the boundary of the safe set, three classes of certificates are derived: one for upper bounds and two for lower bounds on the probability that the cumulative occupation specification is satisfied over a finite time horizon while maintaining safety constraints.

What carries the argument

The stopped process that halts system evolution at the safe-set boundary, allowing barrier certificates to bound occupation measures through the infinitesimal generator of the underlying SDE.

If this is right

  • Rigorous upper and lower probability bounds become computable for finite-time occupation under safety constraints via semidefinite programming.
  • The framework directly applies to continuous-time stochastic systems modeled by SDEs.
  • Numerical examples confirm that the derived certificates can be solved efficiently and provide nontrivial bounds.

Where Pith is reading between the lines

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

  • The method could support controller synthesis by optimizing over the certificates to maximize the guaranteed probability.
  • Extensions to hybrid systems or infinite-horizon specifications may follow by adapting the stopped-process construction.

Load-bearing premise

The stopped-process construction preserves the martingale or generator properties so that the barrier certificates correctly bound the occupation probability.

What would settle it

Monte Carlo simulation of a concrete SDE example yielding an empirical probability lying strictly outside the interval given by the computed upper and lower certificate bounds.

Figures

Figures reproduced from arXiv: 2604.19014 by Bai Xue, C.-H. Luke Ong.

Figure 1
Figure 1. Figure 1: Sample trajectories (H = 10) of the system starting from x0 = 0.5. Green paths successfully accumulate K = 2.0 in the target region (shaded green) within the horizon H = 10. Red paths fail by exiting the safe set (shaded gray) prematurely. Example 2: We analyze the system: dXt = (X3 t − 5Xt)dt + XtdWt. (10) Trajectories start at x0 = 0.9, and we bound the probability of accumulating at least K = 0.1 second… view at source ↗
Figure 2
Figure 2. Figure 2: Sample trajectories (H = 5) of the system starting at x0 = 0.9. The paths are driven rapidly towards the origin by the drift and then linger within T = [0.1, 0.5] (green shaded region) due to the vanishing diffusion term, illustrating the high probability of satisfying the occupation time constraint. V. CONCLUSION This paper presented a unified barrier certificate frame￾work for the quantitative verificati… view at source ↗
read the original abstract

This paper addresses the quantitative verification of finite-time constrained occupation time for stochastic continuous-time systems governed by stochastic differential equations (SDEs). Unlike classical reachability analysis, which focuses on single-event properties such as entering a target set, many autonomous tasks-including surveillance, wireless charging, and chemical mixing-require a system to accumulate a prescribed duration within a target region while strictly maintaining safety constraints. We propose a barrier-certificate framework to compute rigorous upper and lower bounds on the probability that such cumulative specifications are satisfied over a finite time horizon. By introducing a stopped process that freezes the system once it reaches the boundary of the safe set, we derive three classes of certificates: one for upper bounds and two for lower bounds. The proposed approaches are validated through numerical examples implemented using semidefinite programming.

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 develops a barrier-certificate framework for quantitative verification of finite-time constrained occupation measures in continuous-time SDEs. It introduces a stopped process that freezes the state upon hitting the safe-set boundary to derive one class of certificates for upper bounds and two classes for lower bounds on the probability that the system accumulates a prescribed duration in the safe set. These certificates are encoded as SDPs and validated on numerical examples.

Significance. If the stopped-process argument is rigorously established, the work extends barrier-certificate methods from reachability to cumulative occupation-time specifications, providing a practical SDP-based route to rigorous probability bounds for safety-critical tasks such as surveillance and charging. The three-certificate structure and stopped-process construction are technically interesting and could generalize to other path-dependent properties.

major comments (2)
  1. [§3] Stopped-process construction (likely §3): The central claim that the stopped process X^τ preserves the generator properties (or supermartingale property) of the original SDE so that Dynkin's formula or the optional sampling theorem directly yields the occupation-probability bounds is load-bearing. The manuscript must explicitly state the regularity conditions on the SDE coefficients (e.g., local Lipschitz continuity) and boundary regularity required to avoid an extra local-time term or loss of the strong Markov property; without this verification the inequalities used to bound P(∫_0^T 1_safe(X_t) dt ≥ τ) may not hold.
  2. [§4] Lower-bound certificates (likely §4): The two distinct classes of lower-bound certificates are presented without a clear comparison of their relative tightness or the conditions under which one dominates the other. Because the lower-bound claim is part of the main contribution, the paper should include either a theoretical dominance result or numerical evidence showing when each class is preferable.
minor comments (2)
  1. [§2] Notation: The finite-time constrained occupation measure should be defined formally (with the indicator function and time horizon) in the problem-statement section rather than only in the abstract.
  2. [§5] Numerical examples: Report the SDP solver, solver tolerances, and wall-clock times for each example to allow reproducibility assessment.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed review. We address each major comment below and will revise the manuscript accordingly to strengthen the presentation.

read point-by-point responses

  1. Referee: [§3] Stopped-process construction (likely §3): The central claim that the stopped process X^τ preserves the generator properties (or supermartingale property) of the original SDE so that Dynkin's formula or the optional sampling theorem directly yields the occupation-probability bounds is load-bearing. The manuscript must explicitly state the regularity conditions on the SDE coefficients (e.g., local Lipschitz continuity) and boundary regularity required to avoid an extra local-time term or loss of the strong Markov property; without this verification the inequalities used to bound P(∫_0^T 1_safe(X_t) dt ≥ τ) may not hold.

    Authors: We agree that the regularity conditions must be stated explicitly for the stopped-process argument to be rigorous. In the revised manuscript we will add a dedicated paragraph at the start of §3 listing the standing assumptions: the drift f and diffusion σ are locally Lipschitz continuous with at most linear growth, the safe set D is bounded with C² boundary, and the diffusion matrix is uniformly elliptic on the closure of D. Under these conditions the first-exit time τ is a stopping time with respect to the natural filtration, the stopped process X^τ is strong Markov, and Dynkin’s formula applies directly to the stopped process without an additional local-time term because the process is stopped upon hitting the boundary. We will also include a short verification that the constructed barrier functions remain supermartingales for the stopped process, thereby justifying the occupation-probability bounds. revision: yes

  2. Referee: [§4] Lower-bound certificates (likely §4): The two distinct classes of lower-bound certificates are presented without a clear comparison of their relative tightness or the conditions under which one dominates the other. Because the lower-bound claim is part of the main contribution, the paper should include either a theoretical dominance result or numerical evidence showing when each class is preferable.

    Authors: We acknowledge the absence of a direct comparison between the two lower-bound certificate families. In the revised version we will extend the numerical examples section by evaluating both classes on the same benchmark systems (linear SDE and nonlinear oscillator) under identical horizons and occupation thresholds, reporting the resulting lower bounds side-by-side in a new table. We will also add a concise discussion noting that the first class uses a single time-independent barrier while the second employs a family of time-dependent barriers; the latter can be tighter when the occupation threshold is large relative to the horizon, at the cost of higher SDP dimension. These additions will provide both empirical guidance and qualitative insight into when each class is preferable. revision: yes

Circularity Check

0 steps flagged

No circularity: stopped-process construction yields independent barrier-certificate bounds

full rationale

The derivation begins from the SDE, applies a standard stopped-process construction at the safe-set boundary, and obtains three classes of certificates via the generator or martingale properties. No equation reduces to a fitted parameter renamed as a prediction, no load-bearing uniqueness theorem is imported from self-citation, and the abstract supplies no self-referential definitions. The central claim therefore rests on the preservation of Dynkin-type inequalities under stopping, which is an external property of the SDE rather than a tautology internal to the paper.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard SDE existence assumptions plus the novel stopped-process construction and the existence of computable barrier certificates; no free parameters or invented physical entities are introduced.

axioms (2)
  • domain assumption The continuous-time system is governed by a stochastic differential equation with sufficiently regular coefficients.
    Stated directly in the abstract as the class of systems under consideration.
  • ad hoc to paper A stopped process obtained by freezing the state at the safe-set boundary preserves the generator properties needed for the barrier certificates to bound occupation probabilities.
    This is the key technical step introduced in the abstract; its validity is not demonstrated here.

pith-pipeline@v0.9.0 · 5430 in / 1356 out tokens · 39609 ms · 2026-05-10T02:32:10.968181+00:00 · methodology

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

27 extracted references · 27 canonical work pages

  1. [1]

    In: International Conference on Computer Aided Verification

    Abate, A., Giacobbe, M., Roy, D.: Quantitative supermartingale cer- tificates. In: International Conference on Computer Aided Verification. pp. 3–28. Springer (2025)

    work page 2025

  2. [2]

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

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

    work page 2019

  3. [3]

    Comparative analysis of barrier-like function methods for reach-avoid verification in stochastic discrete-time systems.arXiv preprint arXiv:2512.05348,

    Cao, Z., Wang, P., Ong, L., Žikeli ´c, Ð., Wagner, D., Xue, B.: Comparative analysis of barrier-like function methods for reach- avoid verification in stochastic discrete-time systems. arXiv preprint arXiv:2512.05348 (2025)

    work page arXiv 2025

  4. [4]

    In: CA V’13

    Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: CA V’13. pp. 511–526. Springer (2013)

    work page 2013

  5. [5]

    Transactions of the American Mathematical Society84(2), 444–458 (1957)

    Darling, D.A., Kac, M.: On occupation times for markoff processes. Transactions of the American Mathematical Society84(2), 444–458 (1957)

    work page 1957

  6. [6]

    In: International Conference on Computer Aided Verification (CA V)

    Feng, S., Chen, M., Xue, B., Sankaranarayanan, S., Zhan, N.: Unbounded-time safety verification of stochastic differential dynamics. In: International Conference on Computer Aided Verification (CA V). pp. 327–348. Springer (2020)

    work page 2020

  7. [7]

    In: International Conference on Computer Aided Verification

    Henzinger, T.A., Mallik, K., Sadeghi, P., Žikeli ´c, Ð.: Supermartingale certificates for quantitative omega-regular verification and control. In: International Conference on Computer Aided Verification. pp. 29–55. Springer (2025)

    work page 2025

  8. [8]

    IEEE Transactions on Automatic Control (2025)

    Jafarpour, S., Liu, Z., Chen, Y .: Probabilistic reachability analysis of stochastic control systems. IEEE Transactions on Automatic Control (2025)

    work page 2025

  9. [9]

    In: International Sympo- sium on Automated Technology for Verification and Analysis (ATV A)

    Jagtap, P., Soudjani, S., Zamani, M.: Temporal logic verification of stochastic systems using barrier certificates. In: International Sympo- sium on Automated Technology for Verification and Analysis (ATV A). pp. 177–193. Springer (2018)

    work page 2018

  10. [10]

    IEEE Transactions on Auto- matic Control66(7), 3097–3110 (2020)

    Jagtap, P., Soudjani, S., Zamani, M.: Formal synthesis of stochastic systems via control barrier certificates. IEEE Transactions on Auto- matic Control66(7), 3097–3110 (2020)

    work page 2020

  11. [11]

    New York: Academic (1967)

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

    work page 1967

  12. [12]

    In: 2020 American Control Conference (ACC)

    Nilsson, P., Ames, A.D.: Lyapunov-like conditions for tight exit probability bounds through comparison theorems for sdes. In: 2020 American Control Conference (ACC). pp. 5175–5181. IEEE (2020)

    work page 2020

  13. [13]

    In: Stochastic differen- tial equations: an introduction with applications, pp

    Øksendal, B.: Stochastic differential equations. In: Stochastic differen- tial equations: an introduction with applications, pp. 38–50. Springer (2003)

    work page 2003

  14. [14]

    IEEE Transactions on Automatic Control52(8), 1415–1428 (2007)

    Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst- case and stochastic safety verification using barrier certificates. IEEE Transactions on Automatic Control52(8), 1415–1428 (2007)

    work page 2007

  15. [15]

    Automatica125, 109439 (2021)

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

    work page 2021

  16. [16]

    The International Journal of Robotics Research 31(7), 901–923 (2012)

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

    work page 2012

  17. [17]

    In: Proceedings of the AAAI Conference on Artificial Intelligence

    Žikeli ´c, D., 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)

    work page 2023

  18. [18]

    In: ICLR 2025 Workshop: VerifAI: AI Verification in the Wild (2025)

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

    work page 2025

  19. [19]

    Cambridge university press (1991)

    Williams, D.: Probability with martingales. Cambridge university press (1991)

    work page 1991

  20. [20]

    In: 2024 63rd IEEE Conference on Decision and Control (CDC)

    Xue, B.: Safe exit controllers synthesis for continuous-time stochastic systems. In: 2024 63rd IEEE Conference on Decision and Control (CDC). IEEE (2024)

    work page 2024

  21. [21]

    Information and Computation p

    Xue, B.: Finite-time safety and reach-avoid verification of stochastic discrete-time systems. Information and Computation p. 105368 (2025)

    work page 2025

  22. [22]

    Nonlinear Analysis: Hybrid Systems60, 101670 (2026)

    Xue, B.: A new framework for bounding reachability probabilities of continuous-time stochastic systems. Nonlinear Analysis: Hybrid Systems60, 101670 (2026)

    work page 2026

  23. [23]

    To appear in Automatica (2026)

    Xue, B.: Sufficient and necessary barrier-like conditions for safety and reach-avoid verification of stochastic discrete-time systems. To appear in Automatica (2026)

    work page 2026

  24. [24]

    In: 2021 American Control Confer- ence (ACC)

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

    work page 2021

  25. [25]

    IEEE Transactions on Automatic Control69(3), 1882–1889 (2023)

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

    work page 2023

  26. [26]

    In: International Conference on Computer Aided Verification (CA V)

    Zhi, D., Wang, P., Liu, S., Ong, C.H.L., Zhang, M.: Unifying qualita- tive and quantitative safety verification of dnn-controlled systems. In: International Conference on Computer Aided Verification (CA V). pp. 401–426. Springer (2024) APPENDIX a)The proof of Theorem 1: Proof:We analyze the stopped process ˜Xt =X t∧τsaf e and its corresponding occupation ...

    work page 2024

  27. [27]

    Thus, µZ(t) =e −λIout(t)Lv( ˜Xt)

    The dynamics follow the original SDE. Thus, µZ(t) =e −λIout(t)Lv( ˜Xt). By the Attractive Drift Condition,Lv(x)≥β. Thus,µ Z(t)≥βe −λIout(t). •Case 2 (Interior, Outside Targetx∈ X \ T):Here 1X \T = 1. The dynamics follow the original SDE, i.e.,µ Z(t) =e −λIout(t)(Lv( ˜Xt)−λv( ˜Xt)). By the conditionLv(x)≥λv(x)+β, we haveLv(x)−λv(x)≥ β. Thus,µ Z(t)≥βe −λIou...

    work page