This paper presents a novel stochastic barrier function (SBF) framework for safety analysis of stochastic systems based on piecewise (PW) functions. We first outline a general formulation of PW-SBFs. Then, we focus on PW-Constant (PWC) SBFs and show how their simplicity yields computational advantages for general stochastic systems. Specifically, we prove that synthesis of PWC-SBFs reduces to a minimax optimization problem. Then, we introduce three efficient algorithms to solve this problem, each offering distinct advantages and disadvantages. The first algorithm is based on dual linear programming (LP), which provides an exact solution to the minimax optimization problem. The second is a more scalable algorithm based on iterative counter-example guided synthesis, which involves solving two smaller LPs. The third algorithm solves the minimax problem using gradient descent, which admits even better scalability. We provide an extensive evaluation of these methods on various case studies, including neural network dynamic models, nonlinear switched systems, and high-dimensional linear systems. Our benchmarks demonstrate that PWC-SBFs outperform state-of-the-art methods, namely sum-of-squares and neural barrier functions, and can scale to eight dimensional systems.

翻译：本文提出一种基于分段（PW）函数的随机障碍函数（SBF）框架，用于随机系统的安全性分析。我们首先概述了分段随机障碍函数的一般性公式，随后聚焦于分段常数随机障碍函数（PWC-SBF），并展示其简洁性如何为一般随机系统带来计算优势。具体而言，我们证明了PWC-SBF的综合可转化为极小极大优化问题。进而提出三种高效算法求解该问题，每种算法各有优劣：第一种基于对偶线性规划，能精确求解极小极大优化问题；第二种采用反例引导的迭代综合算法，通过求解两个较小规模的线性规划实现更高可扩展性；第三种利用梯度下降法求解极小极大问题，进一步提升了可扩展性。我们通过神经网络动态模型、非线性切换系统和高维线性系统等多类案例进行广泛评估，实验表明PWC-SBF在性能上优于当前最先进方法（如平方和障碍函数与神经网络障碍函数），并可扩展至八维系统。