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

TL;DR

This paper compares various barrier-like methods for verifying reach-avoid properties in stochastic discrete-time systems, analyzing their theoretical and computational aspects through experiments.

Contribution

It provides a comprehensive comparison of barrier-like conditions, highlighting their strengths, limitations, and practical performance in stochastic reach-avoid verification.

Findings

Different methods vary in conservativeness and computational efficiency.

Semidefinite programming and CEGIS are effective tools for practical implementation.

The study guides selecting appropriate verification techniques based on system requirements.

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).