When evaluating safety specifications for trajectories of a dynamical system, it is vital to be able to bound the worst-case probability of unsafety (constraint violation) Certifications of stochastic safety and worst-case probabilities of unsafety can be expressed as infinite-dimensional linear programs (e.g. stochastic barrier functions, occupation measure problems) This paper proves that the infinite-dimensional linear programs and their finite-dimensional Moment-Sum-of-Squares truncations are nonconservative (to the true probability of unsafety) under compactness and regularity conditions in stochastic dynamics. Unsafe-probability estimates and risk contours are generated for example stochastic processes.
Miller et al. (Tue,) studied this question.