Quantitative Verification of Finite-Time Constrained Occupation Measures for Continuous-time Stochastic Systems
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913050822443008 |
|---|---|
| author | Xue, Bai Ong, C. -H. Luke |
| author_facet | Xue, Bai Ong, C. -H. Luke |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_19014 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Quantitative Verification of Finite-Time Constrained Occupation Measures for Continuous-time Stochastic Systems Xue, Bai Ong, C. -H. Luke Systems and Control 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. |
| title | Quantitative Verification of Finite-Time Constrained Occupation Measures for Continuous-time Stochastic Systems |
| topic | Systems and Control |
| url | https://arxiv.org/abs/2604.19014 |