连续时间随机可达-避让验证的充分且必要的类屏障条件

中文摘要 AI 辅助

本文研究了由随机微分方程（SDEs）建模的连续时间随机系统的无限时域可达-避让验证问题。我们在基于屏障函数的框架内表述该问题，该框架将验证问题转化为满足以函数不等式形式表达的类屏障条件的屏障函数的存在性问题。在适当的正则性和一致椭圆性假设下，我们针对无限时域可达-避让验证，给出了关于多项式屏障函数的充分且必要的类屏障条件。我们首先构造一个折扣值函数，用以刻画可达-避让概率的下界。然后我们证明它是相关联的椭圆Dirichlet问题的唯一经典解。基于这一刻画，我们进一步证明，在我们先前关于有限时域可达-避让验证的工作中提出的类屏障条件，对于无限时域可达-避让验证不仅是充分的，而且在可达-避让概率严格大于指定阈值时也是必要的。特别地，当初始集合中每个状态的可达-避让概率严格大于指定阈值时，满足该条件的多项式屏障函数存在。此外，当系统动力学为多项式时，我们将寻找满足该条件的多项式屏障函数的问题表述为平方和（SOS）规划，并证明这些规划是可靠且完备的。最后，我们在两个数值示例上展示了理论结果。

英文摘要

In this paper, we study infinite-horizon reach-avoid verification for continuous-time stochastic systems modeled by stochastic differential equations (SDEs). We formulate this problem within a barrier-function-based framework, which transforms the verification problem into an existence problem for barrier functions satisfying barrier-like conditions expressed as functional inequalities. We provide sufficient and necessary barrier-like conditions in terms of polynomial barrier functions for infinite-horizon reach-avoid verification under suitable regularity and uniform ellipticity assumptions. We first construct a discounted value function that characterizes lower bounds on the reach-avoid probability. We then show that it is the unique classical solution of an associated elliptic Dirichlet problem. Based on this characterization, we further show that the barrier-like condition proposed in our previous work on finite-horizon reach-avoid verification is not only sufficient for infinite-horizon reach-avoid verification but also necessary whenever the reach-avoid probability is strictly larger than the specified threshold. In particular, whenever the reach-avoid probability is strictly larger than the specified threshold fro every state in the initial set, polynomial barrier functions satisfying this barrier-like condition exist. Furthermore, when the system dynamics are polynomial, we formulate the problem of finding polynomial barrier functions satisfying this barrier-like condition as sum-of-squares (SOS) programs, which are shown to be sound and complete. Finally, we demonstrate the theoretical results on two numerical examples.

发表机构

• Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）

机构由 AI 辅助整理，请以论文原文为准。