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

2025/12/05 by Cao, Zhipeng, Wang, Peixin, Ong, Luke +3
#FOS: Electrical engineering #Systems and Control (eess.SY) #electronic engineering #information engineering

paper · doi:10.48550/arxiv.2512.05348

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

Citations

• Runtime Safety and Reach-avoid Prediction of Stochastic Systems via Observation-aware Barrier Functions
• Refined Barrier Conditions for Finite-Time Safety and Reach-Avoid Guarantees in Stochastic Systems
• Counterexample-Guided Synthesis of Robust Discrete-Time Control Barrier Functions
• Supermartingale Certificates for Quantitative Omega-regular Verification and Control
• Neural Continuous-Time Supermartingale Certificates
• Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
• Sound and Complete Proof Rules for Probabilistic Termination
• Finite-time Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
• Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
• A New Framework for Bounding Reachability Probabilities of Continuous-time Stochastic Systems
• Robustness Verification of Deep Reinforcement Learning Based Control Systems using Reward Martingales
• Compositional Policy Learning in Stochastic Control Systems with Formal Guarantees
• Reach-avoid Controllers Synthesis for Safety Critical Systems
• Reachability Verification for Stochastic Discrete-time Dynamical Systems
• Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees
• Reach-Avoid Analysis for Polynomial Stochastic Differential Equations
• Reach-avoid Verification Based on Convex Optimization
• Safety Guarantees for Neural Network Dynamic Systems via Stochastic Barrier Functions
• Sufficient Conditions for Robust Probabilistic Reach-Avoid-Stay Specifications using Stochastic Lyapunov-Barrier Functions
• Data-driven verification and synthesis of stochastic systems via barrier certificates
• Ranking and Repulsing Supermartingales for Reachability in Randomized Programs
• Supermartingales, Ranking Functions and Probabilistic Lambda Calculus
• Quantitative Analysis of Assertion Violations in Probabilistic Programs
• Automated Termination Analysis of Polynomial Probabilistic Programs
• Smooth Converse Lyapunov-Barrier Theorems for Asymptotic Stability with Safety Constraints and Reach-Avoid-Stay Specifications
• Learning for Safety-Critical Control with Control Barrier Functions
• A Barrier Function Approach to Finite-Time Stochastic System Verification and Control
• An Efficient Reachability-Based Framework for Provably Safe Autonomous Navigation in Unknown Environments
• Control Barrier Functions: Theory and Applications
• Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
• Temporal Logic Verification of Stochastic Systems Using Barrier Certificates
• Permissive Barrier Certificates for Safe Stabilization Using Sum-of-squares
• A New Proof Rule for Almost-Sure Termination
• Stochastic Invariants for Probabilistic Termination
• Reach-Avoid Problems with Time-Varying Dynamics, Targets and Constraints
• On the Construction of Barrier Certificate: A Dynamic Programming Perspective

Related

• Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
• Finite-time Safety and Reach-avoid Verification of Stochastic Discrete-time Systems
• Refined Barrier Conditions for Finite-Time Safety and Reach-Avoid Guarantees in Stochastic Systems
• Reachability Verification for Stochastic Discrete-time Dynamical Systems
• Inner approximations of stochastic programs for data-driven stochastic barrier function design