An Update to the Level Set Theorems in Hamilton-Jacobi Reachability Analysis

技术摘要：Hamilton-Jacobi 可达性分析中水平集定理的更新

问题陈述
Hamilton-Jacobi 可达性（HJR）是一个成熟的框架，用于在存在不确定性的情况下为安全关键型非线性系统合成控制器，该框架通常被表述为微分博弈。该过程涉及将定性的控制任务（例如避障或目标达成）转化为“度量博弈”（game of degree），通过求解相关的 Hamilton-Jacobi 偏微分方程以获得值函数，最后通过解释该值函数来定义安全或不安全状态的集合。这一最后步骤依赖于“水平集定理”（Level Set Theorems）。

作者指出，现有文献在这些定理的技术细节上存在错误和歧义，特别是关于值函数的水平集在何种条件下能正确对应于博弈的获胜集。这些问题导致了社区的困惑，特别是关于处于值函数零水平集上的状态的解释。论文认为，以往的表述往往忽略了必要的拓扑和凸性假设，导致对安全性（safety）和可达性（reachability）集合的特征描述出现偏差。

方法论
本文采用了一种植根于微分博弈论和拓扑学的严谨数学方法。作者：

1. 形式化博弈设置： 他们定义了一个有限时界的微分博弈，包含一个控制器玩家和一个对抗性扰动玩家。系统的动力学由 $\dot{x} = f(x, a, b)$ 控制，其中 $a$ 和 $b$ 分别是控制信号和扰动信号。扰动玩家使用非预见性策略（non-anticipative strategies）。
2. 建立假设： 该分析依赖于五个关键假设：
   • 动力学和控制集的标准连续性和紧致性（假设 1-3）。
   • 扰动动力学的凸性： 对于每个状态和控制，由扰动集 $B$ 诱导的可能动力学向量的集合必须是凸的（假设 4）。
   • 失效模式的封闭性： 失效轨迹集 $F(t)$ 在连续轨迹空间中必须是封闭的（假设 5）。
3. 推导通用定理： 他们证明了一个广义水平集定理（定理 1），将值函数 $v(x,t)$ 与安全集 ($L(t)$) 和不安全集 ($G(t)$) 联系起来。该定理确立了 $L(t) = \{x \mid v(x,t) > 0\}$ 且 $G(t) = \{x \mid v(x,t) \leq 0\}$，前提是定义失效模式的泛函 $J$ 是连续且有界的。
4. 构建反例： 为了证明新假设的必要性，作者构建了两个特定的反例：
   • 缺乏凸性： 一个扰动集 $B$ 为非凸（离散点）的避障博弈。他们展示了在缺少假设 4 的情况下，位于零水平集（$v=0$）上的状态可能并不属于不安全集，这与标准的解释相矛盾。
   • 封闭目标集： 一个目标集为封闭而非开集的趋向目标博弈。他们证明了在违反假设 5（即假设目标集应为开集）的情况下，位于零水平集上的状态可能不属于安全集，这同样与标准的解释相矛盾。
5. 证明技术： 证明过程利用 Filippov 引理来建立可测扰动信号的存在性，并利用涉及轨迹集紧致性和非预见性扰动计划的拓扑论证（使用 Tychonoff 定理和字典序）来证明主定理。

核心贡献

1. 纠正技术错误： 本文识别并纠正了先前文献中存在的水平集定理的技术缺陷，特别指出了忽略动力学凸性条件（假设 4）以及要求失效集封闭（假设 5）的问题。
2. 通用水平集定理： 作者提供了一个适用于所有相关有限时界 HJR 博弈的统一、简洁的定理，明确了安全集使用严格不等式（$v > 0$）以及不安全集使用非严格不等式（$v \leq 0$）的规定。
3. 澄清零水平集歧义： 通过反例，本文解释了当标准假设被违反时，值函数的零水平集为何具有歧义性。在这种情况下，仅凭值函数为零无法确定博弈的结果（胜/负）；对于这些特定点，控制器可能在某些点获胜，而扰动者在另一些点获胜。
4. 拓扑严谨性： 本工作弥合了 HJR 与违反理论（viability theory）及半渗透屏障（semi-permeable barriers）中所使用的拓扑论证之间的差距，为解释值函数提供了更稳健的理论基础。

结果
主要结果是定理 1，它在指定假设下，通过值函数严格定义了安全集和不安全集。论文表明：

• 如果扰动动力学不是凸的（例如，离散扰动集），那么对于边界上的点，标准解释即 $v(x,t) \leq 0$ 意味着状态是不安全的，这一结论会失效。
• 如果目标集是封闭的（违反了趋向目标博弈中目标集应为开集的要求），那么对于边界上的点，标准解释即 $v(x,t) > 0$ 意味着状态是安全的，这一结论也会失效。
• 在修正后的假设下，值函数提供了对获胜集的精确刻画，其中扰动玩家拥有“瞬时优势”，这使得严格/非严格不等式的划分成为必要。

意义
作者指出，虽然这些技术问题可能不会立即影响依赖现有软件工具的从业者，但其理论层面的解决是“有趣且细致的”。本文旨在消除因先前技术错误而导致的社区困惑。通过提供修正后的通用定理并利用反例解释差异的来源，这项工作确保了 Hamilton-Jacobi 可达性的理论基础是可靠的。这对于开发基于学习的 HJR 方法或将该框架扩展到复杂分层任务的研究人员尤为重要，因为它澄清了值函数能够正确认证安全性（safety）和活性（liveness）所需的精确条件。