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

TL;DR

This paper develops a barrier-certificate framework to rigorously verify the probability that continuous-time stochastic systems satisfy finite-time occupation constraints, extending reachability analysis to cumulative safety and performance specifications.

Contribution

It introduces a stopped process approach and three classes of certificates to compute bounds on occupation probabilities for stochastic systems over finite horizons.

Findings

Validated methods through numerical examples using semidefinite programming.

Provided rigorous upper and lower bounds on occupation probabilities.

Extended classical reachability analysis to cumulative occupation constraints.

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.