StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis

TL;DR

StochasticBarrier.jl is an open-source Julia toolbox that efficiently generates stochastic barrier functions for safety verification of diverse discrete-time stochastic systems, outperforming existing tools in speed and scalability.

Contribution

It introduces a versatile toolbox that combines SOS and PWC methods for SBF synthesis, enabling verification of complex nonlinear systems with improved performance.

Findings

Outperforms existing tools in computation time and safety bounds

Supports high-dimensional and nonlinear systems

Achieves up to four orders of magnitude speedup

Abstract

We present StochasticBarrier.jl, an open-source Julia-based toolbox for generating Stochastic Barrier Functions (SBFs) for safety verification of discrete-time stochastic systems with additive Gaussian noise. StochasticBarrier.jl certifies linear, polynomial, and piecewise affine (PWA) systems. The latter enables verification for a wide range of system dynamics, including general nonlinear types. The toolbox implements a Sum-of-Squares (SOS) optimization approach, as well as methods based on piecewise constant (PWC) functions. For SOS-based SBFs, StochasticBarrier.jl leverages semi-definite programming solvers, while for PWC SBFs, it offers three engines: two using linear programming (LP) and one based on gradient descent (GD). Benchmarking StochasticBarrier.jl against the state-of-the-art shows that the tool outperforms existing tools in computation time, safety probability bounds, and scalability across over 30 case studies. Compared to its closest competitor, StochasticBarrier.jl is up to four orders of magnitude faster, achieves significant safety probability improvements, and supports higher-dimensional systems.