Safety Verification for Random Ordinary Differential Equations

Random ordinary differential equations (RODEs) are ordinary differential equations (ODEs) that contain a stochastic process in their vector field functions. They have been used for many years in a wide range of applications, but have been a shadow existence to stochastic differential equations (SDEs) despite being able to model a wider and often physically more adequate range of disturbances. In this article, we study the safety verification problem over both finite time horizons and the infinite time horizon for RODEs incorporating Wiener processes. Concretely, we investigate the ${p}$ -safety problem, where we identify the set of initial states from which the probability to satisfy safety specifications is at least ${p}$ . Based on identifying a set of sample paths whose probability measure is larger than ${p}$ , we propose a method of reducing stochastic reachability to adversary reachability of ODEs for solving the ${p}$ -safety problem over finite time horizons. This method permits an efficient lifting of reach-set computation methods for perturbed ODEs to RODEs. In this method, the ${p}$ -safety problem over finite time horizons is reduced to the problem of inner-approximating robust backward reachable sets for ODEs with time-varying perturbation inputs. We then extend the method to the ${p}$ -safety problem over the infinite time horizon. Finally, we demonstrate our method on several examples.