Safety Verification of Stochastic Systems: A Set-Erosion Approach

TL;DR

This paper introduces a set-erosion approach for safety verification of discrete-time stochastic systems, leveraging probabilistic bounds to adapt deterministic safety methods for stochastic contexts.

Contribution

The paper presents a novel set-erosion strategy that combines probabilistic bounds with deterministic safety verification, enabling tighter safety certificates for stochastic systems.

Findings

The method provides tighter barrier certificates than existing approaches.

Numerical experiments demonstrate the effectiveness and superiority of the proposed approach.

The approach is flexible and compatible with various deterministic safety verification techniques.

Abstract

We study the safety verification problem for discrete-time stochastic systems. We propose an approach for safety verification termed set-erosion strategy that verifies the safety of a stochastic system on a safe set through the safety of its associated deterministic system on an eroded subset. The amount of erosion is captured by the probabilistic bound on the distance between stochastic trajectories and their associated deterministic counterpart. Building on our recent work [1], we establish a sharp probabilistic bound on this distance. Combining this bound with the set-erosion strategy, we establish a general framework for the safety verification of stochastic systems. Our method is flexible and can work effectively with any deterministic safety verification techniques. We exemplify our method by incorporating barrier functions designed for deterministic safety verification, obtaining barrier certificates much tighter than existing results. Numerical experiments are conducted to demonstrate the efficacy and superiority of our method.