📝 SummarXiv

Abstract

Providing finite-time probabilistic safety and reach-avoid guarantees is crucial for safety-critical stochastic systems. Existing barrier certificate methods often rely on a restrictive boundedness assumption for auxiliary functions, limiting their applicability. This paper presents refined barrier-like conditions that remove this assumption. Specifically, we establish conditions for deriving upper bounds on finite-time safety probabilities in discrete-time systems and lower bounds on finite-time reach-avoid probabilities in continuous-time systems. This key relaxation significantly expands the class of verifiable systems, especially those with unbounded state spaces, and facilitates the application of advanced optimization techniques, such as semi-definite programming with polynomial functions. The efficacy of our approach is validated through numerical examples.