Reach-Avoid Analysis for Polynomial Stochastic Differential Equations

TL;DR

This paper introduces a semi-definite programming method for probabilistic reach-avoid analysis of polynomial stochastic differential equations, enabling efficient safety verification over open time horizons.

Contribution

It presents a novel convex optimization approach using sum-of-squares decomposition to solve reach-avoid problems for stochastic systems with polynomial dynamics.

Findings

Efficient polynomial-time solution for probabilistic reach-avoid problems.

Extension to classical safety verification and barrier certificates.

Demonstrated effectiveness through multiple examples.

Abstract

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.