Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis

Rayan Mazouz, Frederik Baymler Mathiesen, Luca Laurenti, Morteza Lahijanian

TL;DR

An open-source Julia-based toolbox for generating Stochastic Barrier Functions (SBFs) for safety verification of discrete-time stochastic systems with additive Gaussian noise is presented, which outperforms existing tools in computation time, safety probability bounds, and scalability.

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.

StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis

TL;DR

An open-source Julia-based toolbox for generating Stochastic Barrier Functions (SBFs) for safety verification of discrete-time stochastic systems with additive Gaussian noise is presented, which outperforms existing tools in computation time, safety probability bounds, and scalability.

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.
Paper Structure (39 sections, 3 theorems, 19 equations, 3 figures, 4 tables)

This paper contains 39 sections, 3 theorems, 19 equations, 3 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Theoretical Framework
  3. Problem
  4. Implemented SBF Methods
  5. Sum-of-Squares (SOS)
  6. PWA Inclusion Dynamics
  7. PWC Method
  8. Overview of StochasticBarrier.jl
  9. System Setup
  10. Linear Dynamics Example
  11. SOS-SBF
  12. PWC-SBF
  13. Polynomial Dynamics Example
  14. PWA Inclusion Dynamics Example
  15. SOS-SBF
  16. ...and 24 more sections

Key Result

theorem 1

Let the safe set $X_\mathrm{s} = \{ x \in \mathbb{R}^{n} \mid h_{\mathrm{s}}(x) \geq 0\}$, initial set $X_{\mathrm{0}} = \{ x \in \mathbb{R}^{n} \mid h_{\mathrm{0}}(x) \geq 0\}$, and unsafe set $X_{\mathrm{u}} = \mathbb{R}^n \setminus X_\mathrm{s} = \{ x \in \mathbb{R}^{n} \mid h_{\mathrm{u}}(x) where $\mathcal{L}_{0}$, $\mathcal{L}_{h}$, and $\mathcal{L}_{s}$ are vectors of SOS polynomials of

Figures (3)

  • Figure 1: Polynomial systems benchmarking of StochasticBarrier.jlvs StochasticBarrierFunctions SANTOYO2021109439 and PRoTECT wooding2024protect. Plots depict optimization time $\tau (s)$ and probability of safety $P_s$. If data points are not plotted beyond a certain barrier degree, it means the algorithm ran out of memory.
  • Figure 2: Benchmark plots for the three PWC-SBF methods. For the pendulum and unicycle, the SOS results are also depicted for comparison. Plots depict total optimization time $\tau (s)$ and probability of safety $P_s$.
  • Figure 3: Input-output overview of StochasticBarrier.jl.

Theorems & Definitions (3)

  • theorem 1: SOS-SBF for Polynomial Systems SANTOYO2021109439
  • theorem 2: SOS-SBF for PWA Inclusion Systems mazouz2022safety
  • theorem 3: PWC-SBF mazouz2024piecewise