Reach-Avoid Analysis for Polynomial Stochastic Differential Equations

In this paper we propose a novel semi-definite programming approach that solves reach-avoid problems over open (i.e., not bounded a priori) time horizons for dynamical systems modeled by polynomial stochastic differential equations. The reach-avoid problem in this paper is a probabilistic guarantee: we approximate from the inner a $p$-reach-avoid set, i.e., the set of initial states guaranteeing with probability larger than $p$ that the system eventually enters a given target set while remaining inside a specified safe set till the target hit. Our approach begins with the construction of a bounded value function, whose strict $p$ super-level set is equal to the $p$-reach-avoid set. This value function is then reduced to a twice continuously differentiable solution to a system of equations. The system of equations facilitates the construction of a semi-definite program using sum-of-squares decomposition for multivariate polynomials and thus the transformation of nonconvex reach-avoid problems into a convex optimization problem. The semi-definite program can be solved efficiently in polynomial time with many existing powerful algorithms such as interior point methods and off-the-shelf software packages. We would like to point out that our approach can straightforwardly be specialized to address classical safety verification by, a.o., stochastic barrier certificate methods and reach-avoid analysis for ordinary differential equations. In addition, several examples are provided to demonstrate theoretical and algorithmic developments of the proposed method.