关于障碍证书的构造：动态规划视角

本文从障碍证书的角度重新审视有限时域随机动态系统的形式化验证问题。该主题的大多数现有工作通过基于$c$-鞅的概念构造障碍证书来关注安全性。本文首先从动态规划算子的角度对现有基于鞅的障碍证书条件提供了新见解。具体而言，我们表明现有条件本质上为动态规划解提供了一个界，而该解精确刻画了安全概率。基于这一新视角，我们证明现有方法中的障碍条件在非安全状态上过于保守。为解决此问题，我们提出了一组新的安全障碍证书条件，其严格比现有条件更不保守，从而为安全验证提供了更紧的概率界。我们进一步将方法扩展到可达-规避规范的情况，提供了一组新的障碍证书条件。我们还说明了如何使用平方和（SOS）规划来搜索这些新障碍证书。最后，通过两个数值示例展示了我们方法相较于现有方法的优势。