Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Piecewise Stochastic Barrier Functions

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

TL;DR

It is proved that synthesis of PWC-SBFs reduces to a minimax optimization problem, and 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.

Abstract

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.

Piecewise Stochastic Barrier Functions

TL;DR

It is proved that synthesis of PWC-SBFs reduces to a minimax optimization problem, and 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.

Abstract

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.
Paper Structure (19 sections, 10 theorems, 51 equations, 4 figures, 1 table, 4 algorithms)

This paper contains 19 sections, 10 theorems, 51 equations, 4 figures, 1 table, 4 algorithms.

Table of Contents

  1. Related Work
  2. Problem Formulation
  3. Stochastic Barrier Functions
  4. Piecewise Stochastic Barrier Functions
  5. Piecewise Constant SBF Synthesis
  6. PWC-SBF Synthesis
  7. Computation of PWC-SBFs
  8. Dual Linear Program
  9. Counter-Example Guided Synthesis
  10. Projected Gradient Descent
  11. Evaluations
  12. 2D Linear System
  13. 2D Pendulum NNDMs
  14. 4D Unicycle
  15. 6D and 8D Quadcopter Systems
  16. ...and 4 more sections

Key Result

Theorem 1

If there exists function $B$ that satisfies Conditions eq:barrier_ss-eq:barrier_expectation, then for a horizon $N\in \mathbb{N}$, it follows that

Figures (4)

  • Figure 2: SBF plots for the pendulum NNDM case study.
  • Figure 3: Monte Carlo simulation ($10^{5}$ instances) for the unicycle model with $t = 10 s$.
  • Figure 4: Monte Carlo simulations ($10^5$ instances) for the 6D quadcopter model with lateral-vertical dynamics for $10s$. Trajectories are visualized in (a) state vs. time plot, (b) $y$-$z$ Plane, and (c) 3D workspace. The red boxes in (c) are the obstacles. The control laws stabilize the quadrotor around the equilibrium point $x_{\text{eq}} = (1, 0, 0, 0, 2, 0)$.
  • Figure A.1: This table provides extensive results pertaining to the case studies for safety verification based on piecewise constant and continuous stochastic barriers, as briefly established in Table \ref{['table:results']}.

Theorems & Definitions (11)

  • Definition 1: Probabilistic Safety
  • Theorem 1: laurenti2023unifying
  • Corollary 1: Piecewise SBF
  • Theorem 2: PWC-SBF Synthesis
  • Proposition 1
  • Theorem 3: PWC-SBF Dual LP
  • Lemma 1: Zero Duality Gap
  • Theorem 4: for PWC-SBF
  • Theorem 5: Convexity of $\mathcal{L}(b)$
  • Corollary 2
  • ...and 1 more