Piecewise Stochastic Barrier Functions

Abstract

Stochastic barrier functions (SBFs) are Lyapunov-like functions that enable safety analysis of stochastic systems. Finding a valid SBF, however, is challenging, as it requires solving a complex functional optimization problem. Existing convex approaches are often limited to low-dimensional systems with simple (polynomial) dynamics, while non-convex approaches lack completeness guarantees. To address these challenges, this paper presents a novel SBF synthesis framework 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. We then introduce three efficient algorithms to solve this problem, each offering distinct trade-offs, all with completeness guarantees. 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 counter-example guided inductive 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.