Safe Probabilistic Invariance Verification for Stochastic Discrete-Time Dynamical Systems

Abstract

Ensuring safety through set invariance has proven a useful method in a variety of applications in robotics and control. In this paper, we focus on the safe probabilistic invariance verification problem for discrete-time dynamical systems subject to stochastic disturbances over the infinite time horizon. Our goal is to compute the lower and upper bounds of the liveness probability for a given safe set and set of initial states. This probability represents the likelihood that the system will remain within the safe set for all time. To address this problem, we draw inspiration from stochastic barrier certificates for safety verification and build upon the findings in [21], where an equation was presented for exact probability analysis. We present two sets of optimizations and demonstrate their effectiveness through two examples, using semi-definite programming tools.