Table of Contents
Fetching ...

Unsafe Probabilities and Risk Contours for Stochastic Processes using Convex Optimization

Jared Miller, Matteo Tacchi, Didier Henrion, Mario Sznaier

TL;DR

The paper tackles certifiable risk analysis for stochastic trajectories by formulating the worst-case probability of entering an unsafe set $X_u$ as an infinite-dimensional convex LP in occupation measures and a dual continuous-function program. It then shows that, under compactness and regularity, these relaxations are nonconservative and converge to the true risk map via the moment-SOS hierarchy, with strong duality linking the measure and function formulations. A novel risk-contour framework is introduced by modifying the objective to obtain upper bounds on $P^*(t_0,x_0)$ that converge in $L_1$ to the true risk, providing interpretable visualizations for test initial conditions. The approach yields tractable SDP relaxations and is demonstrated on polynomial dynamics, including a 2D cubic SDE and a discrete-time example, highlighting practical computability for stochastic safety verification and trajectory planning.

Abstract

This paper proposes an algorithm to calculate the maximal probability of unsafety with respect to trajectories of a stochastic process and a hazard set. The unsafe probability estimation problem is cast as a primal-dual pair of infinite-dimensional linear programs in occupation measures and continuous functions. This convex relaxation is nonconservative (to the true probability of unsafety) under compactness and regularity conditions in dynamics. The continuous-function linear program is linked to existing probability-certifying barrier certificates of safety. Risk contours for initial conditions of the stochastic process may be generated by suitably modifying the objective of the continuous-function program, forming an interpretable and visual representation of stochastic safety for test initial conditions. All infinite-dimensional linear programs are truncated to finite dimension by the Moment-Sum-of-Squares hierarchy of semidefinite programs. Unsafe-probability estimation and risk contours are generated for example stochastic processes.

Unsafe Probabilities and Risk Contours for Stochastic Processes using Convex Optimization

TL;DR

The paper tackles certifiable risk analysis for stochastic trajectories by formulating the worst-case probability of entering an unsafe set as an infinite-dimensional convex LP in occupation measures and a dual continuous-function program. It then shows that, under compactness and regularity, these relaxations are nonconservative and converge to the true risk map via the moment-SOS hierarchy, with strong duality linking the measure and function formulations. A novel risk-contour framework is introduced by modifying the objective to obtain upper bounds on that converge in to the true risk, providing interpretable visualizations for test initial conditions. The approach yields tractable SDP relaxations and is demonstrated on polynomial dynamics, including a 2D cubic SDE and a discrete-time example, highlighting practical computability for stochastic safety verification and trajectory planning.

Abstract

This paper proposes an algorithm to calculate the maximal probability of unsafety with respect to trajectories of a stochastic process and a hazard set. The unsafe probability estimation problem is cast as a primal-dual pair of infinite-dimensional linear programs in occupation measures and continuous functions. This convex relaxation is nonconservative (to the true probability of unsafety) under compactness and regularity conditions in dynamics. The continuous-function linear program is linked to existing probability-certifying barrier certificates of safety. Risk contours for initial conditions of the stochastic process may be generated by suitably modifying the objective of the continuous-function program, forming an interpretable and visual representation of stochastic safety for test initial conditions. All infinite-dimensional linear programs are truncated to finite dimension by the Moment-Sum-of-Squares hierarchy of semidefinite programs. Unsafe-probability estimation and risk contours are generated for example stochastic processes.
Paper Structure (25 sections, 16 theorems, 41 equations, 5 figures, 2 tables)

This paper contains 25 sections, 16 theorems, 41 equations, 5 figures, 2 tables.

Key Result

Theorem 3.1

The following LP will upper-bound eq:unsafe_prob_single with $p^*(t_0, X_0) \geq P^*(t_0, X_0)$ for each $X_0 \subseteq X$

Figures (5)

  • Figure 1: Trajectories of SDE \ref{['eq:flow_sde']} (cyan) initialized in a disk $X_0$ (purple boundary), hitting an unsafe region $X_u$ (red moon).
  • Figure 2: Risk levels of the unsafety upper-bound function $v(0, x)$ at $t=T=5$ and order $k=$6 for SDE \ref{['eq:flow_sde']} initialized in a disk $X_0$ (purple boundary) with unsafe region $X_u$ (red moon).
  • Figure 3: Risk contours for the linear SDE in \ref{['eq:linear_sde']} in increasing time horizon $T$ w.r.t. unsafe region $X_u$ (red half-disk)
  • Figure 4: Trajectories of discrete-time \ref{['eq:scatter_discrete']} (cyan) initialized in a disk $X_0$ (purple boundary), hitting an unsafe region $X_u$ (red half disk).
  • Figure 5: Risk levels of unsafety upper-bound function $v(0, x)$ at $t=T=10$ and order $k=$6 for SDE \ref{['eq:scatter_discrete']} initialized in a disk $X_0$ (purple boundary) with unsafe region $X_u$ (red moon).

Theorems & Definitions (35)

  • Theorem 3.1
  • proof
  • Lemma 3.2: Theorem 3.1 of henrion2009approximate
  • Theorem 3.3
  • proof
  • Theorem 3.4
  • proof
  • Theorem 3.5
  • proof
  • Remark 1
  • ...and 25 more