Finite-time Safety and Reach-avoid Verification of Stochastic Discrete-time Systems

This paper proposes novel barrier-like sufficient conditions to compute both lower and upper bounds of the probability that a stochastic discrete-time system will exit a safe set or reach a target set within a given bounded time horizon.