Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A data-driven approach for safety quantification of non-linear stochastic systems with unknown additive noise distribution

Frederik Baymler Mathiesen, Licio Romao, Simeon C. Calvert, Luca Laurenti, Alessandro Abate

TL;DR

A novel data-driven approach to quantify safety for non-linear, discrete-time stochastic systems with unknown noise distribution and introduces an inner approximation of the stochastic program to design a SBF in terms of a chance-constrained optimisation problem.

Abstract

In this paper, we present a novel data-driven approach to quantify safety for non-linear, discrete-time stochastic systems with unknown noise distribution. We define safety as the probability that the system remains in a given region of the state space for a given time horizon and, to quantify it, we present an approach based on Stochastic Barrier Functions (SBFs). In particular, we introduce an inner approximation of the stochastic program to design a SBF in terms of a chance-constrained optimisation problem, which allows us to leverage the scenario approach theory to design a SBF from samples of the system with Probably Approximately Correct (PAC) guarantees. Our approach leads to tractable, robust linear programs, which enable us to assert safety for non-linear models that were otherwise deemed infeasible with existing methods. To further mitigate the computational complexity of our approach, we exploit the structure of the system dynamics and rely on spatial data structures to accelerate the construction and solution of the underlying optimisation problem. We show the efficacy and validity of our framework in several benchmarks, showing that our approach can obtain substantially tighter certificates compared to state-of-the-art with a confidence that is several orders of magnitude higher.

A data-driven approach for safety quantification of non-linear stochastic systems with unknown additive noise distribution

TL;DR

A novel data-driven approach to quantify safety for non-linear, discrete-time stochastic systems with unknown noise distribution and introduces an inner approximation of the stochastic program to design a SBF in terms of a chance-constrained optimisation problem.

Abstract

In this paper, we present a novel data-driven approach to quantify safety for non-linear, discrete-time stochastic systems with unknown noise distribution. We define safety as the probability that the system remains in a given region of the state space for a given time horizon and, to quantify it, we present an approach based on Stochastic Barrier Functions (SBFs). In particular, we introduce an inner approximation of the stochastic program to design a SBF in terms of a chance-constrained optimisation problem, which allows us to leverage the scenario approach theory to design a SBF from samples of the system with Probably Approximately Correct (PAC) guarantees. Our approach leads to tractable, robust linear programs, which enable us to assert safety for non-linear models that were otherwise deemed infeasible with existing methods. To further mitigate the computational complexity of our approach, we exploit the structure of the system dynamics and rely on spatial data structures to accelerate the construction and solution of the underlying optimisation problem. We show the efficacy and validity of our framework in several benchmarks, showing that our approach can obtain substantially tighter certificates compared to state-of-the-art with a confidence that is several orders of magnitude higher.

Paper Structure

This paper contains 26 sections, 5 theorems, 52 equations, 7 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Problem formulation
  3. Notation
  4. Problem formulation
  5. Preliminaries
  6. Convex analysis and linear programming
  7. Scenario optimisation
  8. Uncertain piece-wise affine relaxations
  9. Stochastic barrier functions
  10. An inner chance-constrained approximation of Problem \ref{['eq:infinite-dim-BP']}
  11. Over-approximating general non-linear systems with uncertain PWA dynamics
  12. Data-driven approximation of \ref{['eq:uncertain_ccp_opt_pro']} for the class of uncertain dynamical systems
  13. Algorithms for program construction
  14. Over-approximation of $Q_{ij}(\omega)$
  15. Convex hull over the sample set
  16. ...and 11 more sections

Key Result

Lemma 1

For $B \in \mathcal{M}$ with $\lVert B \rVert_{\infty} = M$, let $c$ and $\eta$ be as in eq:infinite-dim-BP. Define the set for some constant ${ \xi} \geq 0$. If there exists an $\epsilon \in (0,1)$ such that ${ \xi} \geq M \frac{\epsilon}{1-\epsilon}$ and $\mathbb{P}\{E^c \} \leq \epsilon$, then we have $\mathbb{E}\{B(f(x) + \eta(\omega))\} \leq B(x) + c$ for all $x \in X_s$.

Figures (7)

  • Figure 1: Summary of the proposed framework for safety verification of nonlinear systems. Theorem \ref{['theorem:barrier-ccp']} (Section \ref{['sec:chance-constrained-apprx']}) guarantees that the associated stochastic program to find a can be solved as a chance-constrained program via constraint tightening. Non-linearities can be dealt with by means of a abstraction as in Theorem \ref{['theorem:uncertain_barrier-ccp']} (Section \ref{['sec:uncertain_dynamics_safety_and_ccbp']}). The scenario approach is applied to use available data for high-confidence certificates; strong duality is essential to relax the problem to lp in Corollary \ref{['corollary:scenario-barrier-design']} (in Section \ref{['sec:data_driven_uncertain_stochastic_barriers']}).
  • Figure 2: Computation graph for the function $f(x) = x^3 + x$ with lbp annotation for the input regions $[-1, 0]$ and $[0, 1]$. lbp operates by propagating backward linear bounds on the computation graph.
  • Figure 3: The figure is borrowed from Mathiesen2013. A $B(x)$ is a non-negative function that is greater than $1$ in an unsafe region ${ X_u}$, which is the complement of the safe set ${ X_s}$. The variable $\gamma$ is an upper bound for $B(x)$ over an initial region ${ X_0}$. The upper bound for the expected increase in $B(x)$ after one step of \ref{['eq:system']} over the safe set ${ X_s}$ is denoted ${ c}$. Proposition \ref{['prop:barrier_prob_safety']} shows that $\zeta({ X_s}, T) \geq 1 - (\gamma + { c} T)$.
  • Figure 4: Given two regions ${ Q}_i, { Q}_j$ and a realisation of the noise $\omega$, the set $Q_{ij}(\omega)$ represents the subset of $x\in { Q}_i$ such that $\hat{f}(x, \alpha) + \eta(\omega) \in { Q}_j$ for some $\alpha \in [0, 1]$. In other words, $Q_{ij}(\omega)$ is the subset of ${ Q}_i$ that can reach ${ Q}_j$ given the realisation of the noise $\omega$. Unfortunately, $Q_{ij}(\omega)$ is not easily computed (the example above is an exception, see Fig. \ref{['fig:non-convex_preimage']}) and thus in Section \ref{['subsec:over-approximate_preimage']}, we will compute an over-approximation $\hbox{$\m@th Q$}{ \hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}} _{ij}(\omega)$.
  • Figure 5: A pictorial example that $Q_{ij}(\omega)$ is not necessarily convex. In this example, we have $\underline{A_i} = -I$, $\hbox{$\m@th A_i$}{ \hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}} = I$, and $\underline{b_i} = \hbox{$\m@th b_i$}{ \hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}} = 0$, which is a valid uncertain affine relaxation of the trivial function $f(x) = 0$ in the non-negative orthant. We consider the region ${ Q}_j = [2, 3]^2$ and plot $A_i(\alpha)^{-1}{ Q}_j$ for 10 different values of $\alpha \in [0, 1]$. Note that in this case $\hbox{$\m@th A_i$}{ \hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}} = I$, hence ${ Q}_j = A_i(1)^{-1}{ Q}_j$ and ${ Q}_j$ (blue) is contained in the convex hull (pink). $Q_{ij}(\omega)$ can take on complex shapes and no method exists for exactly computing $Q_{ij}(\omega)$. Therefore, we compute a sound over-approximation $\hbox{$\m@th Q$}{ \hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{\hbox{$\m@th\overline{}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}}$}} _{ij}(\omega) \subset Q_{ij}(\omega)$.
  • ...and 2 more figures

Theorems & Definitions (15)

  • Definition 1: Probabilistic safety Abate2008
  • Definition 2: sbf
  • Lemma 1
  • proof
  • Theorem 1
  • proof
  • Theorem 2
  • proof
  • Lemma 2
  • Remark 1
  • ...and 5 more