Reach-Avoid Analysis for Polynomial Stochastic Differential Equations

• 成果类型: Article
• 署名作者: Xue, Bai; Zhan, Naijun; Fraenzle, Martin
• 署名单位: Chinese Academy of Sciences; Institute of Software, CAS; Chinese Academy of Sciences; University of Chinese Academy of Sciences, CAS; Carl von Ossietzky Universitat Oldenburg
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2023.3332570
• 发表日期: 2024
• 页码: 1882-1889
• 关键词: STOCHASTIC PROCESSES; mathematical models; Stochastic systems; safety; computational modeling; Upper bound; Probabilistic logic; inner approximation; reach-avoid analysis; Semidefinite programming; stochastic differential equations (SDEs)

摘要

In this article, we propose a novel semidefinite 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 article 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 semidefinite program using sum-of-squares decomposition for multivariate polynomials and thus, the transformation of nonconvex reach-avoid problems into a convex optimization problem. 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.