💻 computer science

Shielding for Higher-Order Safety

本文介绍了一种用于网络物理系统的创新型屏蔽合成框架，该框架通过将问题简化为基于历史相关状态空间的有限状态安全博弈，来强制执行涉及状态导数（如速度和加加速度）的高阶安全约束，并采用一种通过基于层级排序的导数约束来剪枝不安全区域的迭代算法来提高效率。

原作者： Filip Cano, Thomas A. Henzinger, Konstantin Kueffner

发布于 2026-08-05

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Filip Cano, Thomas A. Henzinger, Konstantin Kueffner

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下你正在为一个机器人编写程序来驾驶汽车。在最简单的版本中，安全性仅仅关乎“现在”是否撞到了东西。如果机器人在一个没有墙壁接触的地方，它就是“安全”的。但现实世界中，安全不仅仅关乎你所处的位置，还关乎你是如何到达那里的，以及你下一步要去向何方。如果那个机器人停在距离墙壁一米处，它是安全的。但如果它正以每小时 100 英里的速度冲向那面墙，它就注定会毁灭，尽管它现在还没有撞上墙。危险来自于停止时所涉及的“力”：速度、突然的制动（加速度）以及那种制动的顿挫感（加加速度/Jerk）。

这就是**信息物理系统（Cyber-Physical Systems）**的世界，在这里，数字代码控制着物理机器。为了保持这些机器的安全，工程师们使用了“屏蔽器（Shields）”。把屏蔽器想象成一个坐在驾驶员身旁、高度警觉的副驾驶。如果驾驶员（主 AI）试图做一个会导致碰撞的动作，副驾驶会瞬间夺取方向盘并强制执行一个更安全的动作。传统上，这些副驾驶只关注汽车当前的位置。但随着机器变得越来越复杂，我们需要能够理解运动的“故事”，而不仅仅是理解当前这一帧的副驾驶。这篇论文探讨了如何构建能够理解速度、加速度甚至“加加速度”（加速度的变化率）的屏蔽器，从而在不显得过于霸道的前提下确保安全。

问题所在：“反应迟钝”的副驾驶

作者 Filip Cano、Thomas A. Henzinger 和 Konstantin Kueffner 指出，传统的安全屏蔽器过于近视。它们只检查当前状态是“安全”还是“不安全”。但在物理学中，安全是一个连锁事件。

想象一辆车正在接近一堵墙。

0 阶（位置）： 车是否碰到了墙？没碰？那就好。
1 阶（速度）： 车是否开得太快以至于无法停下？
2 阶（加速度）： 车辆刹车力度是否足够大，能在规定时间内停下来？
3 阶（加加速度/Jerk）： 制动是否过于突然，以至于会将乘客甩出座位？

如果你只检查位置（0 阶），你可能会允许汽车以高速驶向墙壁，因为目前还没撞到墙。等到位置变得“不安全”时，已经太晚了，无法停下来。汽车需要一个能够观察其运动“历史”的屏蔽器。它需要知道：“如果我继续以这个速度跑三秒钟，我就会撞车，”并在撞车发生前停下车。

解决方案：拥有记忆的屏蔽器

论文介绍了一种构建这些屏蔽器的新方法，称为微分安全属性（Differential Safety Properties）。屏蔽器不再仅仅观察当前状态，而是观察过去几刻钟的一个“窗口”。

为了让这变得具体，请将汽车的运动想象成一串脚印。

0 阶屏蔽器只看汽车轮胎正下方的那个脚印。
1 阶屏蔽器观察最后两个脚印，以观察汽车移动的速度。
2 阶屏蔽器观察最后三个脚印，以观察速度变化的快慢（加速度）。

作者证明了，为了强制执行关于第 $k$ 阶导数（如加加速度，即 3 阶导数）的规则，屏蔽器需要精确记住最后 $k$ 步的历史。他们称之为“依赖历史的策略（history-dependent strategy）”。

重大发现：更聪明的记忆

这是论文精妙之处。构建这种屏蔽器的显而易见的方法是创建一个包含最后 $k+1$ 步所有可能组合的庞大地图。如果你在一个网格上有一辆车，并且需要记住 4 步，那么可能的历史序列数量会爆炸式增长。这就像试图记住国际象棋中 4 步走法的每一种可能序列一样；地图会变得如此巨大，以至于计算机在完成计算之前就会崩溃。

作者找到了两种解决方法：

直接合成（高效记忆）： 他们证明了你实际上不需要存储完整的 $k+1$ 步历史来做出决策。你只需要存储最后 $k$ 步。当屏蔽器考虑一个新的动作时，它会将存储的 $k$ 步与提议的新步骤结合起来，以检查其是否安全。这节省了大量的内存。他们在数学上证明了，你不可能在存储少于 $k$ 步的情况下完成任务；如果你忘记了哪怕一步，屏蔽器也可能会错过危险。
迭代合成（分层方法）： 这是他们处理复杂安全规则的“秘密武器”。通常，安全性不仅仅是一个规则，它是一个层级结构。你必须留在车道内（位置），然后不能超速（速度），然后再不能刹车过猛（加速度）。
- 旧方法会尝试同时解决所有这些规则，检查每一个可能的历史记录是否符合每一条规则。
- 新的迭代方法则是逐一解决它们，就像剥洋葱一样。
- 首先，它确定汽车可以在哪里行驶而不撞墙（位置）。它标记出所有“失败”的路径（即发生碰撞的路径）。
- 然后，它转向下一个规则（速度）。但诀窍在于：它会忽略任何在第一步中已经被标记为“失败路径”的路径。为什么要浪费时间去检查一辆已经撞车的车是否在超速呢？
- 通过在每个层级削减“坏”路径，该算法避免了探索那些已知已不安全的巨大状态空间。

研究结果

团队在模拟的 2D 汽车游戏中测试了这些方法。他们设置了一些场景，要求汽车在带有墙壁和障碍物的网格中导航，同时遵守关于位置、速度、加速度和加加速度的规则。

结果： 与旧的“基准”方法相比，新方法速度显著提高，且占用的内存更少。在某些情况下，基准方法在 60 秒后超时（放弃运行），而新的迭代方法在不到 2 秒的时间内就解决了问题。
权衡： 论文表明，随着你增加更复杂的规则（更高阶），屏蔽器会变得更加保守。它会迫使汽车更早地减速并进行更平滑的转弯，以确保能够应对停止时的“加加速度”。
证明： 他们不仅仅是猜测这行得通；他们还提供了数学证明，证明他们的内存需求是绝对最小的，并且他们的迭代方法能找到与缓慢的暴力破解法完全相同的“最大许可（maximally permissive）”屏蔽器（即干扰最小的屏蔽器）。

为什么这很重要

这不仅仅关乎汽车。任何由计算机控制物理对象的系统——无人机、机械臂甚至医疗设备——都需要遵守这些“平滑性”约束。如果无人机试图过于突然地停止，它可能会坠毁或伤及附近的人。如果机械臂移动得过于颠簸，它可能会损坏正在抓取的物体。

通过展示如何构建能够理解运动“历史”且不会陷入内存限制的屏蔽器，这篇论文为工程师提供了一个实用的工具包，使自主系统更加安全可靠。它将“导数”这一抽象数学概念转化为了一个具体的、高效的算法，可以在真实硬件上运行，确保机器人不仅能避开墙壁，还能平稳且安全地抵达目的地。

技术摘要：高阶安全防护（Shielding for Higher-Order Safety）

1. 问题陈述

经典的防护器（Shields）是运行时强制执行机制，旨在限制控制器的动作以保证安全性。传统上，这些防护器是针对状态谓词（State Predicates）进行综合的，即物理状态被分类为安全或不安全。然而，在许多信息物理系统（CPS）应用中，这种二元视角是不充分的。安全性往往取决于状态的导数（Derivatives），而不仅仅是状态本身。例如，一辆正在接近障碍物的车辆不仅必须避免碰撞（位置），还必须遵守速度限制（一阶导数）、由加速度引起的力限制（二阶导数），以及防止受伤的加加速度（Jerk）限制（三阶导数）。

本文解决的核心问题是如何在离散时间、离散状态设置下，系统地定义并执行基于位置状态的离散导数的安全性约束。挑战在于，一个 $k$ 阶约束依赖于长度为 $k+1$ 的连续状态窗口，这需要随约束阶数增加而增长的内存，并且需要高效的综合算法，以避免探索状态空间中的不可行区域。

2. 方法论

微分安全性属性（Differential Safety Properties）

作者引入了微分安全性属性，这是一种用于指定离散导数约束的语言。

离散导数： 使用离散化状态空间 $S \subseteq \mathbb{R}^d$ 及时间步 $\Delta \tau$ 上的向后有限差分进行递归定义。第 $k$ 阶导数在索引 $t$ 处取决于长度为 $k+1$ 的状态窗口 $(s_{t-k}, \dots, s_t)$ 。
语法与语义： 属性是关于形式为 $\partial^k \in R$ 的原子项（其中 $R$ 为安全集）的布尔表达式。阶数为 $k$ 的属性在整个序列上被解释为：若该属性对所有长度为 $k+1$ 的窗口均成立，则该属性成立。
表达能力： 论文证明了 $k$ 阶微分安全性属性与连续 $k+1$ 个状态的窗口谓词是完全等价的。

防护器综合方法

论文提出了三种方法，用于为这些属性合成最大允许性的获胜策略（即防护器），这些属性被建模为回合制安全性博弈（Turn-based Safety Games）。

A. 基准综合法（历史博弈/History Games）

该方法通过扩展状态空间，将微分安全性博弈简化为普通的安全性博弈。

构建： 增强状态空间以存储长度为 $k+1$ 的历史记录。微分安全性属性变为历史状态上的状态不变性。
结果： 历史博弈上的无记忆策略会诱导出原博弈上的 $(k+1)$ -历史依赖策略。
复杂度： $O(|S|^{k+1} \cdot |A|)$ 。

B. 直接综合法（内存最优/Direct Synthesis）

作者提出了一种优化的算法，计算相同的最大允许性防护器，但仅需存储 $k$ 个过去的状态（长度为 $k$ 的历史记录）。

机制： 算法初始化长度小于 $k$ 的历史记录的安全动作（此时 $k$ 阶导数未定义）。对于长度为 $k$ 的历史记录，它检查所有后继状态是否满足该属性。随后，它进行冲突回溯传播：如果某个历史记录没有安全动作，则将其标记为不安全，并将导致该历史记录的动作从前驱历史记录中移除。
内存界限： 论文证明了 $k$ -历史依赖性是必要且紧致的；存在某些博弈，其获胜策略需要 $k$ -历史依赖性，而不存在 $(k-1)$ -历史依赖策略。
优化： 该算法可以限制在路径连通的历史记录（即在实际运行中可能发生的历史记录）上，从而将复杂度降低至 $O(|S| \cdot B^k \cdot |A|)$ ，其中 $B$ 是转移度的上界。

C. 迭代综合法（层次化/Iterative Synthesis）

对于构成层次结构的属性（例如：位置 $\land$ 速度 $\land$ 加速度），作者提出了一个迭代过程。

原理： 如果一个窗口对于较低阶的属性是不安全的（例如速度），那么对于包含该属性的高阶属性而言，该窗口也必然是不安全的。
流程： 算法逐层求解层次结构。在第 $i$ 层，它构建满足第 $i$ 阶属性且其后缀（最后 $i-1$ 个状态）是第 $i-1$ 层获胜窗口的候选窗口。这种方法在评估高阶约束之前，显著地剪枝了搜索空间。
复杂度： 在最坏情况下，其复杂度与直接综合法一致，但在实践中，通过利用低层级已知不安全的区域来剪枝状态空间，该方法提供了显著的效率提升。

3. 主要贡献

定义微分安全性属性： 一种用于约束离散导数的正式语言，并证明其与滑动状态窗口谓词等价。
基准规约： 将微分安全性博弈标准规约为基于 $(k+1)$ 个状态历史的普通安全性博弈。
直接综合算法： 一种内存最优的算法，通过仅使用 $k$ 个状态的历史记录来计算最大允许性防护器，并证明了该内存界限的紧致性。
迭代综合： 一种针对层次化微分安全性属性的算法，按复杂度递增顺序求解约束，并利用低层解来剪枝状态空间。
实验评估： 在 2D 车辆模型上的实现与评估，证明了直接综合法和迭代综合法在处理较大实例或更高阶约束时，相比基准法能显著降低时间与内存成本。

4. 实验结果

作者在离散化的 2D 汽车模型上评估了综合程序，该模型在接近墙壁或障碍物时具有各种速度、加速度、加加速度（Jerk）和加加加速度（Snap）约束。

性能： 基准方法在处理较大实例或更高阶属性时经常超时（60秒限制）。直接综合法和迭代综合法均能在数秒内解决这些实例。
效率： 当剪枝状态数量很大时（例如在某些基准测试中剪枝率为 89.5%），迭代综合法的表现优于直接综合法，证实了层次化方法的效用。
轨迹行为： 仿真显示，高阶防护器会比低阶防护器更早地迫使智能体远离高速度和急转弯，从而有效地防止进入因动量而导致碰撞不可避免的“注定失败”状态，即使当前的物理位置是安全的。
导数压力： 作者引入了一个度量指标来可视化约束满足情况，结果显示，与低阶防护器相比，高阶防护器在所有导数阶数上都维持着较低的压力。

5. 重要性与主张

本文声称为面向信息物理系统的高阶安全性提供了一个系统性的框架。其意义在于：

弥合差距： 超越了简单的状态谓词，将动态约束（速度、加速度、加加速度）纳入其中，这些约束对于物理安全性和舒适度至关重要。
内存效率： 证明了执行 $k$ 阶约束所需的内存可以从 $k+1$ 个状态减少到 $k$ 个状态，并且这种减少在理论上是必要的。
可扩展性： 展示了层次化综合如何通过利用安全性层次结构的结构特征来剪枝状态空间，从而使复杂的多层安全性约束的执行在计算上变得可行。
运行时强制执行： 提供了一种生成最大允许性防护器的方法，确保执行机制仅在严格保证安全所必需时才对控制器（例如学习到的策略）进行干预。

作者指出，虽然该方法是在离线状态下求解有限对抗博弈，但它为所选抽象提供了最坏情况下的最大允许性防护器。他们承认，未来的工作可以探索符号不动点方法（Symbolic Fixed-point Methods），以改进显式状态枚举法，并探索将微分约束与其他滑动窗口规范相结合的方法。