Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Runtime Safety and Reach-avoid Prediction of Stochastic Systems via Observation-aware Barrier Functions

Shenghua Feng, Jie An, Fanjiang Xu

TL;DR

The paper addresses runtime safety and reach-avoid probability prediction for discrete-time stochastic systems with online observations by introducing observation-aware barrier functions ($OBF$, $OSBF$, $ORBF$). It combines offline barrier synthesis via semidefinite programming and sum-of-squares methods with online backward iteration to update probability bounds as new observations arrive, providing rigorous guarantees for conditional safety and reach-avoid events. The approach yields compositional bounds by bounding the observation-sequence probability and the conditioned safety/RA events, and is validated on nonlinear benchmarks where online updates adaptively refine predictions. This framework enables real-time, data-driven safety assurances and lays groundwork for integrating runtime predictions with responsive control in safety-critical stochastic environments.

Abstract

Stochastic dynamical systems have emerged as fundamental models across numerous application domains, providing powerful mathematical representations for capturing uncertain system behavior. In this paper, we address the problem of runtime safety and reach-avoid probability prediction for discrete-time stochastic systems with online observations, i.e., estimating the probability that the system satisfies a given safety or reach-avoid specification. Unlike traditional approaches that rely solely on offline models, we propose a framework that incorporates real-time observations to dynamically refine probability estimates for safety and reach-avoid events. By introducing observation-aware barrier functions, our method adaptively updates probability bounds as new observations are collected, combining efficient offline computation with online backward iteration. This approach enables rigorous and responsive prediction of safety and reach-avoid probabilities under uncertainty. In addition to the theoretical guarantees, experimental results on benchmark systems demonstrate the practical effectiveness of the proposed method.

Runtime Safety and Reach-avoid Prediction of Stochastic Systems via Observation-aware Barrier Functions

TL;DR

The paper addresses runtime safety and reach-avoid probability prediction for discrete-time stochastic systems with online observations by introducing observation-aware barrier functions (, , ). It combines offline barrier synthesis via semidefinite programming and sum-of-squares methods with online backward iteration to update probability bounds as new observations arrive, providing rigorous guarantees for conditional safety and reach-avoid events. The approach yields compositional bounds by bounding the observation-sequence probability and the conditioned safety/RA events, and is validated on nonlinear benchmarks where online updates adaptively refine predictions. This framework enables real-time, data-driven safety assurances and lays groundwork for integrating runtime predictions with responsive control in safety-critical stochastic environments.

Abstract

Stochastic dynamical systems have emerged as fundamental models across numerous application domains, providing powerful mathematical representations for capturing uncertain system behavior. In this paper, we address the problem of runtime safety and reach-avoid probability prediction for discrete-time stochastic systems with online observations, i.e., estimating the probability that the system satisfies a given safety or reach-avoid specification. Unlike traditional approaches that rely solely on offline models, we propose a framework that incorporates real-time observations to dynamically refine probability estimates for safety and reach-avoid events. By introducing observation-aware barrier functions, our method adaptively updates probability bounds as new observations are collected, combining efficient offline computation with online backward iteration. This approach enables rigorous and responsive prediction of safety and reach-avoid probabilities under uncertainty. In addition to the theoretical guarantees, experimental results on benchmark systems demonstrate the practical effectiveness of the proposed method.

Paper Structure

This paper contains 31 sections, 11 theorems, 44 equations, 1 figure, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Problem Formulation
  4. Safety and Reach-Avoid Probability Estimation.
  5. Runtime Safety and Reach-avoid Prediction.
  6. Theoretical Results: Observation-aware Barrier Functions
  7. Observation-aware Barrier Functions.
  8. Observation-aware Safety Barrier Functions
  9. The Reach-avoid Case.
  10. Algorithm for Runtime Safety and Reach-avoid Prediction
  11. Computing OBF.
  12. Computing OSBF and ORBF.
  13. Experiments
  14. Benchmarks and Experiment Setup.
  15. Experimental Results and Analysis.
  16. ...and 16 more sections

Key Result

Theorem 1

Suppose there exists an observation-aware barrier function $B(t, x)$ for the system with initial set $I$, unsafe set $U$, observation sequence $\{(t_i, O_i)\}_{i=1}^k$, and threshold $q$. Then, for any $x_0 \in I$,

Figures (1)

  • Figure 1: Visualization of the stochastic Van der Pol system (safety) and Equil system (reach-avoid). The red region denotes the unsafe set; the green region denotes the target set.

Theorems & Definitions (37)

  • Remark 1
  • Remark 2
  • Definition 1: Observation barrier functions
  • Remark 3
  • Theorem 1
  • proof : Proof sketch
  • Definition 2: Observation-aware safety barrier functions
  • Remark 4
  • Theorem 2
  • proof : Proof sketch
  • ...and 27 more