pith. sign in

arxiv: 2604.17902 · v1 · submitted 2026-04-20 · 📡 eess.SY · cs.SY

Quantitative Verification of Constrained Occupation Time for Stochastic Discrete-time Systems

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

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

classification 📡 eess.SY cs.SY
keywords barrier certificatesstochastic systemsoccupation timequantitative verificationswitched systemsprobabilistic boundsdiscrete-time systemssafety verification
0
0 comments X

The pith

Multiplicative stochastic barrier functions certify the probability of visiting a target set at least k times while preserving safety in discrete stochastic systems.

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

The paper develops a barrier certificate method to verify constrained occupation times, which measure how often a stochastic discrete-time system visits a target region without leaving a safe set. It introduces multiplicative stochastic barrier functions whose algebraic form implicitly tracks visit counts, avoiding separate state augmentation for the counter. A switched-system reformulation separates the safety constraint, allowing derivation of explicit probabilistic upper and lower bounds on occupation times for both finite and infinite horizons. Dissipative barriers yield exponential decay bounds on excessive visits, while attractive barriers supply lower bounds through submartingale properties. The resulting framework supplies the first general certificate approach for certifying repeated behaviors such as surveillance or periodic charging under uncertainty.

Core claim

We present the first barrier certificate framework capable of certifying these behaviors. We introduce multiplicative stochastic barrier functions that encode visitation counts implicitly within the algebraic structure of a scalar barrier. By adopting a switched-system reformulation to handle safety, we derive rigorous probabilistic bounds for both finite and infinite horizons. Specifically, we show that dissipative barriers establish upper bounds ensuring the exponential decay of frequent visits, while attractive barriers provide lower bounds via submartingale analysis.

What carries the argument

multiplicative stochastic barrier functions that encode visitation counts implicitly within the algebraic structure of a scalar barrier, combined with a switched-system reformulation for safety

If this is right

  • Dissipative barriers give exponential upper bounds on the probability of visiting the target too frequently.
  • Attractive barriers give lower bounds on the probability of visiting the target sufficiently often via submartingale analysis.
  • The bounds hold for both finite-horizon and infinite-horizon occupation times.
  • The switched reformulation preserves the original transition probabilities while enforcing safety.
  • Numerical examples confirm that the framework can be instantiated on concrete control problems.

Where Pith is reading between the lines

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

  • The same multiplicative structure might be adapted to synthesize controllers that enforce occupation-time specifications rather than only verify them.
  • Extension to continuous-time or hybrid stochastic systems would require defining analogous multiplicative barriers under different dynamics.
  • The approach could be paired with existing reachability tools to automate barrier search for larger state spaces.

Load-bearing premise

That multiplicative stochastic barrier functions exist and can be found for the systems under consideration, and that the switched-system reformulation does not alter the probabilistic properties of the original system.

What would settle it

A discrete stochastic system where the occupation-time probability lies outside the bounds computed from any candidate multiplicative barrier, or a system satisfying the desired occupation-time property for which no multiplicative stochastic barrier function can be constructed.

Figures

Figures reproduced from arXiv: 2604.17902 by Bai Xue, C.-H. Luke Ong, Peixin Wang.

Figure 1
Figure 1. Figure 1: Numerical illustration for constrained occupation time. [PITH_FULL_IMAGE:figures/full_fig_p021_1.png] view at source ↗
read the original abstract

This paper addresses the quantitative verification of constrained occupation time in stochastic discrete-time systems, focusing on the probability of visiting a target set at least $k$ times while maintaining safety. Such cumulative properties are essential for certifying repeated behaviors like surveillance and periodic charging. To address this, we present the first barrier certificate framework capable of certifying these behaviors. We introduce multiplicative stochastic barrier functions that encode visitation counts implicitly within the algebraic structure of a scalar barrier. By adopting a switched-system reformulation to handle safety, we derive rigorous probabilistic bounds for both finite and infinite horizons. Specifically, we show that dissipative barriers establish upper bounds ensuring the exponential decay of frequent visits, while attractive barriers provide lower bounds via submartingale analysis. The efficacy of the proposed framework is demonstrated through numerical examples.

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 introduces a barrier-certificate method for quantitative verification of constrained occupation time in stochastic discrete-time systems. It claims to be the first such framework, using newly defined multiplicative stochastic barrier functions that implicitly encode the number of visits to a target set inside a scalar function. A switched-system reformulation is adopted to enforce safety constraints, from which the authors derive exponential-decay upper bounds (via dissipative barriers) and lower bounds (via attractive barriers and submartingale analysis) on the probability of visiting the target at least k times, for both finite and infinite horizons. The approach is illustrated on numerical examples.

Significance. If the central technical claims hold, the work would provide a useful new tool for certifying repeated behaviors (e.g., surveillance or periodic charging) under probabilistic safety constraints in stochastic systems. The multiplicative encoding of visitation counts and the switched reformulation are novel extensions of classical barrier-certificate and martingale techniques; the paper would receive credit for attempting to handle both upper and lower bounds on occupation measures within a single scalar-function framework.

major comments (2)
  1. [Abstract and the definition of multiplicative stochastic barrier functions] The abstract asserts that multiplicative stochastic barrier functions encode visitation counts 'implicitly within the algebraic structure of a scalar barrier' and that the switched-system reformulation leaves the original transition kernel unchanged. No explicit proof or lemma is referenced showing that the multiplicative update rule maps exactly onto the occupation counting process once auxiliary safety modes are active; any measure distortion induced by switching would invalidate both the supermartingale upper bound and the submartingale lower bound.
  2. [Switched-system reformulation section] The derivation of the finite- and infinite-horizon probabilistic bounds relies on the switched reformulation preserving the original occupation measure. The manuscript must supply a formal statement (with proof) that the auxiliary modes do not alter the probability of k-visits to the target set; without it, the claimed exponential decay and submartingale bounds rest on an unverified equivalence.
minor comments (2)
  1. [Numerical examples] The abstract mentions 'numerical examples' but does not indicate whether the examples include explicit computation of the barrier functions or comparison against Monte-Carlo estimates of the true occupation probabilities.
  2. [Preliminaries] Notation for the multiplicative update and the precise definition of 'dissipative' versus 'attractive' barriers should be introduced with a short table or boxed definition to improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and constructive comments on our manuscript. The feedback correctly identifies the need for greater explicitness regarding the equivalence between the switched-system reformulation and the original occupation measure. We address each major comment below and will make the indicated revisions to improve rigor and clarity.

read point-by-point responses

  1. Referee: [Abstract and the definition of multiplicative stochastic barrier functions] The abstract asserts that multiplicative stochastic barrier functions encode visitation counts 'implicitly within the algebraic structure of a scalar barrier' and that the switched-system reformulation leaves the original transition kernel unchanged. No explicit proof or lemma is referenced showing that the multiplicative update rule maps exactly onto the occupation counting process once auxiliary safety modes are active; any measure distortion induced by switching would invalidate both the supermartingale upper bound and the submartingale lower bound.

    Authors: We appreciate the referee highlighting this point. The manuscript derives the probabilistic bounds from the multiplicative update rule and the switched dynamics, but we agree that an explicit lemma is needed to formally establish the exact correspondence with the occupation counting process and to confirm that auxiliary safety modes introduce no measure distortion. In the revised manuscript we will insert a new lemma immediately following the definition of multiplicative stochastic barrier functions. The lemma will state that the multiplicative update, when combined with the switched reformulation, preserves the probability of at least k visits to the target set. Its proof will proceed by induction on the number of steps, showing that the auxiliary modes only activate on safety violations and that, on all paths that remain safe, the transition kernel and the visitation counter evolve identically to the original system. This will directly support the validity of both the supermartingale upper bounds and the submartingale lower bounds. revision: yes

  2. Referee: [Switched-system reformulation section] The derivation of the finite- and infinite-horizon probabilistic bounds relies on the switched reformulation preserving the original occupation measure. The manuscript must supply a formal statement (with proof) that the auxiliary modes do not alter the probability of k-visits to the target set; without it, the claimed exponential decay and submartingale bounds rest on an unverified equivalence.

    Authors: We acknowledge that the current exposition presents the switched reformulation and then proceeds directly to the bound derivations without a standalone preservation statement. We will revise the switched-system reformulation section to include a formal proposition (Proposition 4.1) together with its complete proof. The proposition asserts that, for any initial state in the safe set, the probability that the number of visits to the target set is at least k is identical under the original dynamics and under the switched dynamics. The proof will rely on the fact that the switching logic only redirects trajectories that would otherwise violate safety constraints, while leaving all safe trajectories and their associated transition probabilities unchanged; consequently, the induced measure on the sequences of target visits coincides exactly. With this addition the exponential-decay upper bounds and the submartingale lower bounds will rest on a rigorously verified equivalence. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation applies standard martingale methods to newly introduced barrier functions

full rationale

The paper defines multiplicative stochastic barrier functions to implicitly encode visitation counts and adopts a switched-system reformulation for safety. It then derives finite- and infinite-horizon probabilistic bounds by applying dissipative (supermartingale) and attractive (submartingale) properties to these barriers. These steps rely on established probabilistic inequalities once the barrier functions are posited to exist; no equation or claim reduces the final bounds to a fitted parameter, self-citation chain, or definitional renaming of the inputs. The framework is therefore self-contained against external benchmarks such as martingale theory and does not exhibit any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The framework builds on standard stochastic processes theory and introduces a new class of barrier functions. No free parameters are mentioned in the abstract.

axioms (2)
  • standard math Submartingale and supermartingale properties for probability bounds
    Used to derive lower and upper bounds on visitation probabilities.
  • domain assumption Switched-system reformulation preserves the original system's dynamics and safety properties
    Adopted to handle safety constraints separately.
invented entities (1)
  • multiplicative stochastic barrier functions no independent evidence
    purpose: To implicitly encode the number of visits to a target set in a scalar barrier function for certification
    Newly proposed in this work to address the occupation time problem.

pith-pipeline@v0.9.0 · 5428 in / 1317 out tokens · 69124 ms · 2026-05-10T04:32:00.192345+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

38 extracted references · 38 canonical work pages

  1. [1]

    In: International Conference on Computer Aided Verifica- tion

    Abate,A.,Giacobbe,M.,Roy,D.:Stochasticomega-regularverificationandcontrol with supermartingales. In: International Conference on Computer Aided Verifica- tion. pp. 395–419. Springer (2024)

    work page 2024

  2. [2]

    In: In- ternational Conference on Computer Aided Verification

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

    work page 2025

  3. [3]

    Automatica44(11), 2724–2734 (2008)

    Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica44(11), 2724–2734 (2008)

    work page 2008

  4. [4]

    MIT press (2008)

    Baier, C., Katoen, J.P.: Principles of model checking. MIT press (2008)

    work page 2008

  5. [5]

    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ć, Ð., 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

  6. [6]

    In: Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013

    Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martin- gales. In: Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25. pp. 511–526. Springer (2013)

    work page 2013

  7. [7]

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

    Chakarov, A., Voronin, Y.L., Sankaranarayanan, S.: Deductive proofs of almost sure persistence and recurrence properties. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 260–279. Springer (2016)

    work page 2016

  8. [8]

    In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

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

    work page 2017

  9. [9]

    In: Foundations of Software Technology and The- oretical Computer Science: 17th Conference Kharagpur, India, December 18–20, 1997 Proceedings 17

    Clarke, E.M.: Model checking. In: Foundations of Software Technology and The- oretical Computer Science: 17th Conference Kharagpur, India, December 18–20, 1997 Proceedings 17. pp. 54–56. Springer (1997)

    work page 1997

  10. [10]

    In: International symposium on automated technology for verification and analysis

    Clarke, E.M., Zuliani, P.: Statistical model checking for cyber-physical systems. In: International symposium on automated technology for verification and analysis. pp. 1–12. Springer (2011)

    work page 2011

  11. [11]

    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

  12. [12]

    Journal of Statistical Physics104(3), 489–524 (2001)

    Godreche, C., Luck, J.: Statistics of the occupation time of renewal processes. Journal of Statistical Physics104(3), 489–524 (2001)

    work page 2001

  13. [13]

    In: Future of software engineering proceedings, pp

    Gordon, A.D., Henzinger, T.A., Nori, A.V., Rajamani, S.K.: Probabilistic pro- gramming. In: Future of software engineering proceedings, pp. 167–181 (2014)

    work page 2014

  14. [14]

    Oxford university press (2020)

    Grimmett, G., Stirzaker, D.: Probability and random processes. Oxford university press (2020)

    work page 2020

  15. [15]

    In: International Confer- ence on Computer Aided Verification

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

    work page 2025

  16. [16]

    In: International Symposium on Automated Tech- nology for Verification and Analysis

    Jagtap, P., Soudjani, S., Zamani, M.: Temporal logic verification of stochastic sys- tems using barrier certificates. In: International Symposium on Automated Tech- nology for Verification and Analysis. pp. 177–193. Springer (2018)

    work page 2018

  17. [17]

    In: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

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

    work page 2021

  18. [18]

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

    work page 1967

  19. [19]

    Springer Science & Business Media (2012)

    Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety. Springer Science & Business Media (2012)

    work page 2012

  20. [20]

    IEEE Control Systems Letters7, 973–978 (2022)

    Mathiesen, F.B., Calvert, S.C., Laurenti, L.: Safety certification for stochastic sys- tems via neural barrier functions. IEEE Control Systems Letters7, 973–978 (2022)

    work page 2022

  21. [21]

    In: Proceedings of the 27th international conference on machine learning (ICML-10)

    Nair, V., Hinton, G.E.: Rectified linear units improve restricted boltzmann ma- chines. In: Proceedings of the 27th international conference on machine learning (ICML-10). pp. 807–814 (2010)

    work page 2010

  22. [22]

    In: 18th annual symposium on foun- dations of computer science (sfcs 1977)

    Pnueli, A.: The temporal logic of programs. In: 18th annual symposium on foun- dations of computer science (sfcs 1977). pp. 46–57. ieee (1977)

    work page 1977

  23. [23]

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

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

    work page 2007

  24. [24]

    SIAM Journal on Control and Optimization46(3), 999–1021 (2007)

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

    work page 2007

  25. [25]

    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

  26. [26]

    Springer Science & Business Media (2012)

    Söderström, T.: Discrete-time stochastic systems: estimation and control. Springer Science & Business Media (2012)

    work page 2012

  27. [27]

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

    Steinhardt,J.,Tedrake,R.:Finite-timeregionalverificationofstochasticnon-linear systems. The International Journal of Robotics Research31(7), 901–923 (2012)

    work page 2012

  28. [28]

    Automatica46(12), 1951–1961 (2010)

    Summers, S., Lygeros, J.: Verification of discrete time stochastic hybrid systems: A stochastic reach-avoid decision problem. Automatica46(12), 1951–1961 (2010)

    work page 1951

  29. [29]

    Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartin- galesforreachabilityinrandomizedprograms.ACMTransactionsonProgramming Languages and Systems (TOPLAS)43(2), 1–46 (2021)

    work page 2021

  30. [30]

    arXiv preprint arXiv:2512.21596 (2025)

    Wang, P., Bai, J., Zhang, M., Ong, C.H.L.: Quantitative verification of omega- regular properties in probabilistic programming. arXiv preprint arXiv:2512.21596 (2025)

    work page arXiv 2025

  31. [31]

    Cambridge university press (1991)

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

    work page 1991

  32. [32]

    Information and Computation307, 105368 (2025)

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

    work page 2025

  33. [33]

    Automatica187, 112919 (2026)

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

    work page 2026

  34. [34]

    In: 2021 American Control Conference (ACC)

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

    work page 2021

  35. [35]

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

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

    work page 2024

  36. [36]

    In: 2023 62nd IEEE Conference on Decision and Control (CDC)

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

    work page 2023

  37. [37]

    In: International Conference on Computer Aided Verification

    Zhi, D., Wang, P., Liu, S., Ong, C.H.L., Zhang, M.: Unifying qualitative and quan- titative safety verification of dnn-controlled systems. In: International Conference on Computer Aided Verification. pp. 401–426. Springer (2024)

    work page 2024

  38. [38]

    Advances in Neural Information Processing Systems36, 47849–47873 (2023) Appendix Corollary 1 (Infinite-Horizon Lower Bounds).Consider the setup of Theorem 2 withα >1

    Žikelić, Ð., Lechner, M., Verma, A., Chatterjee, K., Henzinger, T.: Compositional policy learning in stochastic control systems with formal guarantees. Advances in Neural Information Processing Systems36, 47849–47873 (2023) Appendix Corollary 1 (Infinite-Horizon Lower Bounds).Consider the setup of Theorem 2 withα >1. To obtain a non-trivial bound asN→ ∞, ...

    work page 2023