Tolerant Barrier Certificates for Stochastic Systems

Abstract

We study stochastic verification under tolerant specifications, where unsafe behavior is allowed as long as the total unsafe exposure remains below a prescribed budget with high probability. In discrete time, unsafe exposure is the number of visits to an unsafe set; in continuous time, it is the occupation time spent there. We introduce tolerant barrier certificates, whose key idea is to force the barrier to decrease more aggressively whenever the state is unsafe, so that the barrier compensates for the unsafe exposure accumulated along the trajectory. This construction yields supermartingale-based upper bounds on the probability that the unsafe-exposure budget is exceeded, for both tolerant safety and tolerant reach-avoid properties. We investigate both discrete-time stochastic systems and stochastic differential dynamics, and demonstrate the effectiveness of our approach on a collection of benchmarks.