Safety Analysis of Stochastic Dynamical Systems

This paper presents a method for verifying the safety of a stochastic system. In particular, we show how to compute the largest set of initial conditions such that a given stochastic system is safe with probability p.
To compute the set of initial conditions we rely on the moment method that via Haviland's theorem allows an infinite dimensional optimization problem on measures to be formulated as a polynomial optimization problem. Subsequently, the moment sequence is truncated (relaxed) to obtain a finite dimensional polynomial optimization problem. Finally, we provide an illustrative example that shows how the p-safe initial set is computed numerically.