# Reach-Avoid Analysis for Polynomial Stochastic Differential Equations

arXiv: https://arxiv.org/abs/2208.10752 · HTML: https://mlsanity.com/paper/2208.10752/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Aug 2022.

## Built on by (most cited first, 3 of 3)

- [Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems](https://mlsanity.com/paper/2404.01769/) (2024)
- [Set Invariance with Probability One for Controlled Diffusion: Score-based Approach](https://mlsanity.com/paper/2507.22385/) (2025)
- [Runtime Monitoring of Supermartingale Certificates](https://mlsanity.com/paper/2610.19701/) (2026)

## Abstract (arXiv)

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.
