Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Comparative Analysis of Barrier-like Function Methods for Reach-Avoid Verification in Stochastic Discrete-Time Systems

Zhipeng Cao, Peixin Wang, Luke Ong, Đorđe Žikelić, Dominik Wagner, Bai Xue

TL;DR

The paper tackles infinite-horizon reach-avoid verification in stochastic discrete-time systems by comparing barrier-like conditions I–IV from the literature. It analyzes their theoretical properties, including invariance assumptions and drift conditions, and assesses computational tractability through convexity and domain constraints. The authors provide a unified framework and demonstrate practical performance via semidefinite programming (SDP) and counterexample-guided inductive synthesis (CEGIS) on polynomial and nonlinear systems. Key findings indicate that barrier-like Conditions III and IV generally offer broader applicability and can attain tight guarantees using either SDP or CEGIS, while SDP is particularly effective for polynomial dynamics and CEGIS extends to nonpolynomial cases at the cost of iteration and variability. Overall, the work clarifies relationships among barrier conditions and highlights the trade-offs between tractability, conservativeness, and completeness for reach-avoid verification in stochastic settings.

Abstract

In this paper, we compare several representative barrier-like conditions from the literature for infinite-horizon reach-avoid verification of stochastic discrete-time systems. Our comparison examines both their theoretical properties and computational tractability, highlighting each condition's strengths and limitations that affect applicability and conservativeness. Finally, we illustrate their practical performance through computational experiments using semidefinite programming (SDP) and counterexample-guided inductive synthesis (CEGIS).

Comparative Analysis of Barrier-like Function Methods for Reach-Avoid Verification in Stochastic Discrete-Time Systems

TL;DR

The paper tackles infinite-horizon reach-avoid verification in stochastic discrete-time systems by comparing barrier-like conditions I–IV from the literature. It analyzes their theoretical properties, including invariance assumptions and drift conditions, and assesses computational tractability through convexity and domain constraints. The authors provide a unified framework and demonstrate practical performance via semidefinite programming (SDP) and counterexample-guided inductive synthesis (CEGIS) on polynomial and nonlinear systems. Key findings indicate that barrier-like Conditions III and IV generally offer broader applicability and can attain tight guarantees using either SDP or CEGIS, while SDP is particularly effective for polynomial dynamics and CEGIS extends to nonpolynomial cases at the cost of iteration and variability. Overall, the work clarifies relationships among barrier conditions and highlights the trade-offs between tractability, conservativeness, and completeness for reach-avoid verification in stochastic settings.

Abstract

In this paper, we compare several representative barrier-like conditions from the literature for infinite-horizon reach-avoid verification of stochastic discrete-time systems. Our comparison examines both their theoretical properties and computational tractability, highlighting each condition's strengths and limitations that affect applicability and conservativeness. Finally, we illustrate their practical performance through computational experiments using semidefinite programming (SDP) and counterexample-guided inductive synthesis (CEGIS).

Paper Structure

This paper contains 10 sections, 9 theorems, 11 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Problem Statement
  4. Comparative Analysis
  5. Barrier-like Conditions I
  6. Barrier-like Conditions II
  7. Barrier-like Conditions III
  8. Barrier-like Conditions IV
  9. Examples and Discussions
  10. Examples

Key Result

theorem thmcountertheorem

If there exist two functions $h_1 :\mathbb{R}^n \rightarrow \mathbb{R}$ and $h_2 : \mathbb{R}^n \rightarrow \mathbb{R}$, and a positive value $\epsilon>0$, such that the following constraints are satisfied: then for every $\bm{x}_0\in \mathcal{X}_0$, $\mathbb{P}_{\pi}(RA_{\bm{x}_0})\geq 1-h_1(\bm{x}_0)\geq p$.

Theorems & Definitions (12)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition: Reach-avoid Verification
  • theorem thmcountertheorem
  • corollary thmcountercorollary
  • proposition thmcounterproposition: Theorem 2, xue2024sufficient
  • theorem thmcountertheorem: vzikelic2023learning
  • theorem thmcountertheorem: Theorem 1, vzikelic2023compositional
  • theorem thmcountertheorem: xue2024sufficient
  • corollary thmcountercorollary
  • ...and 2 more