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

TL;DR

This paper introduces a novel barrier certificate framework for quantitatively verifying the probability of repeated visits to a target set in stochastic discrete-time systems, crucial for applications like surveillance.

Contribution

It presents the first barrier certificate method capable of certifying cumulative visitation behaviors in stochastic systems using multiplicative stochastic barrier functions.

Findings

The framework provides rigorous probabilistic bounds for visitation counts over finite and infinite horizons.

Dissipative barriers ensure exponential decay bounds for frequent visits.

Attractive barriers establish lower bounds on visitation probabilities.

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.