Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Framework for Safe Probabilistic Invariance Verification of Stochastic Dynamical Systems

Taoran Wu, Yiqing Yu, Bican Xia, Ji Wang, Bai Xue

TL;DR

The paper introduces a framework for safe probabilistic invariance verification of stochastic discrete-time and continuous-time systems over an infinite horizon, focusing on computing rigorous lower and upper bounds on liveness probabilities inside a safe set from an initial set. It develops two complementary optimization approaches: (i) barrier-certificate methods based on Doob's nonnegative supermartingale inequality to obtain lower bounds, and (ii) equations-relaxation techniques that characterize exact reach-avoid probabilities and yield both lower and upper bounds via relaxations. The discrete- and continuous-time formulations share auxiliary switched/invariant constructions and culminate in semidefinite programming implementations (SOS, SDP) that are demonstrated on several nonlinear examples, with results aligning with Monte Carlo references as polynomial degree increases. The work extends previous discrete-time methods to continuous-time systems, clarifies equivalences and trade-offs between the two bounding strategies, and provides practical SDP recipes (Op0–Op8) for computing bounds. Overall, the framework offers a scalable, certifiable means to assess and certify safety properties of stochastic dynamical systems under uncertainty, with clear pathways for numerical validation and application to robotics and control contexts.

Abstract

Ensuring safety through set invariance has proven to be a valuable method in various robotics and control applications. This paper introduces a comprehensive framework for the safe probabilistic invariance verification of both discrete- and continuous-time stochastic dynamical systems over an infinite time horizon. The objective is to ascertain the lower and upper bounds of liveness probabilities for a given safe set and set of initial states. The liveness probability signifies the likelihood of the system remaining within the safe set indefinitely, starting from a state in the initial set. To address this problem, we propose optimizations for verifying safe probabilistic invariance in discrete-time and continuous-time stochastic dynamical systems. These optimizations are constructed via either using the Doob's nonnegative supermartingale inequality-based method or relaxing the equations described in [30,32], which can precisely characterize the probability of reaching a target set while avoiding unsafe states. Finally, we demonstrate the effectiveness of these optimizations through several examples using semi-definite programming tools.

A Framework for Safe Probabilistic Invariance Verification of Stochastic Dynamical Systems

TL;DR

The paper introduces a framework for safe probabilistic invariance verification of stochastic discrete-time and continuous-time systems over an infinite horizon, focusing on computing rigorous lower and upper bounds on liveness probabilities inside a safe set from an initial set. It develops two complementary optimization approaches: (i) barrier-certificate methods based on Doob's nonnegative supermartingale inequality to obtain lower bounds, and (ii) equations-relaxation techniques that characterize exact reach-avoid probabilities and yield both lower and upper bounds via relaxations. The discrete- and continuous-time formulations share auxiliary switched/invariant constructions and culminate in semidefinite programming implementations (SOS, SDP) that are demonstrated on several nonlinear examples, with results aligning with Monte Carlo references as polynomial degree increases. The work extends previous discrete-time methods to continuous-time systems, clarifies equivalences and trade-offs between the two bounding strategies, and provides practical SDP recipes (Op0–Op8) for computing bounds. Overall, the framework offers a scalable, certifiable means to assess and certify safety properties of stochastic dynamical systems under uncertainty, with clear pathways for numerical validation and application to robotics and control contexts.

Abstract

Ensuring safety through set invariance has proven to be a valuable method in various robotics and control applications. This paper introduces a comprehensive framework for the safe probabilistic invariance verification of both discrete- and continuous-time stochastic dynamical systems over an infinite time horizon. The objective is to ascertain the lower and upper bounds of liveness probabilities for a given safe set and set of initial states. The liveness probability signifies the likelihood of the system remaining within the safe set indefinitely, starting from a state in the initial set. To address this problem, we propose optimizations for verifying safe probabilistic invariance in discrete-time and continuous-time stochastic dynamical systems. These optimizations are constructed via either using the Doob's nonnegative supermartingale inequality-based method or relaxing the equations described in [30,32], which can precisely characterize the probability of reaching a target set while avoiding unsafe states. Finally, we demonstrate the effectiveness of these optimizations through several examples using semi-definite programming tools.
Paper Structure (23 sections, 19 theorems, 79 equations, 2 figures, 7 tables)

This paper contains 23 sections, 19 theorems, 79 equations, 2 figures, 7 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Stochastic Discrete-time Systems
  4. Stochastic Continuous-time Systems
  5. Preliminaries on Discrete-time systems
  6. Problem Statement
  7. Reachability Probability Characterization in xue2021reach
  8. Safe Probabilistic Invariance Verification for Discrete-time Systems
  9. Doob's Nonnegative Supermartingale Inequality Based Invariance Verification
  10. Equations Relaxation Based Invariance Verification
  11. Preliminaries on Continuous-time systems
  12. Problem Statement
  13. Reachability Probability Characterization in xue2023reach
  14. Safe Probabilistic Invariance Verification for Continuous-time Systems
  15. Doob's Nonnegative Supermartingale Inequality Based Invariance Verification
  16. ...and 8 more sections

Key Result

Proposition 3.4

\newlabeltheorem_reach0 Given a safe set $\mathcal{X}$ and a target set $\mathcal{X}_r$, where $\mathcal{X}_r\subseteq \mathcal{X}$, if there exist bounded functions $v(\bm{x})\colon \widehat{\mathcal{X}}\rightarrow \mathbb{R}$ and $w(\bm{x})\colon \widehat{\mathcal{X}}\rightarrow \mathbb{R}$ such then for $\bm{x}_0\in \mathcal{X}$, where $\widehat{\bm{\phi}}^{\bm{x}_0}_{\pi}(\cdot)\colon \mathb

Figures (2)

  • Figure 1: Illustration of computed $v(\bm{x})$ on $\mathcal{X}$ when $d=18$ in Example \ref{['lvm']}. Red region denotes $v(\bm{x})<0$, while blue region denotes $v(\bm{x})\geq 0$.
  • Figure 2: Illustrations of trajectories for systems (red curve - $\partial \mathcal{X}$; green curve - $\partial \mathcal{X}_0$).

Theorems & Definitions (46)

  • Definition 3.1
  • Definition 3.2
  • Remark 3.3
  • Proposition 3.4: Theorem 1, xue2021reach
  • Corollary 3.5
  • Proposition 4.1
  • Example 1
  • Theorem 4.2
  • Proof 1
  • Example 2
  • ...and 36 more