Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Time-Varying Reach-Avoid Control Certificates for Stochastic Systems

Rayan Mazouz, Luca Laurenti, Morteza Lahijanian

Abstract

Reach-avoid analysis is fundamental to reasoning about the safety and goal-reaching behavior of dynamical systems, and serves as a foundation for specifying and verifying more complex control objectives. This paper introduces a reach-avoid certificate framework for discrete-time, continuous-space stochastic systems over both finite- and infinite-horizon settings. We propose two formulations: time-varying and time-invariant certificates. We also show how these certificates can be synthesized using sum-of-squares (SOS) optimization, providing a convex formulation for verifying a given controller. Furthermore, we present an SOS-based method for the joint synthesis of an optimal feedback controller and its corresponding reach-avoid certificate, enabling the maximization of the probability of reaching the target set while avoiding unsafe regions. Case studies and benchmark results demonstrate the efficacy of the proposed framework in certifying and controlling stochastic systems with continuous state and action spaces.

Time-Varying Reach-Avoid Control Certificates for Stochastic Systems

Abstract

Reach-avoid analysis is fundamental to reasoning about the safety and goal-reaching behavior of dynamical systems, and serves as a foundation for specifying and verifying more complex control objectives. This paper introduces a reach-avoid certificate framework for discrete-time, continuous-space stochastic systems over both finite- and infinite-horizon settings. We propose two formulations: time-varying and time-invariant certificates. We also show how these certificates can be synthesized using sum-of-squares (SOS) optimization, providing a convex formulation for verifying a given controller. Furthermore, we present an SOS-based method for the joint synthesis of an optimal feedback controller and its corresponding reach-avoid certificate, enabling the maximization of the probability of reaching the target set while avoiding unsafe regions. Case studies and benchmark results demonstrate the efficacy of the proposed framework in certifying and controlling stochastic systems with continuous state and action spaces.

Paper Structure

This paper contains 26 sections, 10 theorems, 45 equations, 4 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Problem Formulation
  3. Preliminaries: Non-negative Polynomials
  4. Reach-Avoid Certificates
  5. Sum-of-Squares Functional Optimization
  6. Certificate Synthesis via SOS Polynomials
  7. Computational Complexity
  8. Time-varying certificate in Theorem \ref{['th:one-shot-certificate']}
  9. Time-invariant certificate in Corollary \ref{['col:one-shot-certificate-ti']}
  10. Comparison
  11. Joint synthesis of Controller and Certificate
  12. Experiments
  13. Benchmark Systems
  14. 1D Linear Systems
  15. 2D Contraction Maps
  16. ...and 11 more sections

Key Result

Proposition 1

Let $X \subset \mathbb{R}^n$ be a compact basic semi-algebraic set defined as $X = \{ x \in \mathbb{R}^n \mid h_i(x) \geq 0 \; \forall i \in \{1, \ldots, l\} \},$ where $h_i(x)$ is a polynomial. Then, polynomial $\gamma(x)$ is non-negative on $X$ if, for some $\lambda_{0}(x), \lambda_{i}(x) \in \L

Figures (4)

  • Figure 1: Monte Carlo simulations for different linear and polynomial verification systems.
  • Figure 2: Monte Carlo simulations under synthesized controllers.
  • Figure 3: Reach-avoid certificate for Contraction Map 1.
  • Figure 4: Time-varying certificate plots for horizon $H=10$. Certificate evolution over time: initially below $\alpha_0$ in both safe and unsafe sets, then by horizon $H$, low values in the unsafe set, and high near the initial set where $\gamma$ is maximized.

Theorems & Definitions (23)

  • Definition 1: Probabilistic Reach-Avoid
  • Remark 1
  • Definition 2: SOS Polynomial
  • Proposition 1: Stengle1974
  • Corollary 2
  • Theorem 3: Time-Varying, Bounded-Horizon Reach-Avoid Certificate
  • proof
  • Corollary 4: Time-Varying, Unbounded-Horizon Reach-Avoid Certificate
  • Corollary 5: Time-Invariant Reach-Avoid Certificate
  • proof
  • ...and 13 more