arXiv:2608.03662cs.AI2026-08中稿 · RV 2026

为高阶物理约束设计安全防护罩,确保系统不仅不碰撞,还满足加速度与急动度限制。

Shielding for Higher-Order Safety

论文配图:Shielding for Higher-Order Safety
图 1 · 摘自论文原文
  • 基于状态导数构建安全约束,用有限差分刻画高阶平滑性要求。
  • 合成的防护罩需存储恰好k个历史状态,且该记忆量不可减少。
  • 逐层迭代求解,高效剪枝不安全状态空间,适合复杂物理系统控制。

安全防护罩是运行时机制,用于限制控制器行为以保证系统安全。传统防护罩针对状态谓词:当前状态要么安全,要么不安全,屏蔽那些可能使系统未来进入不安全状态的动作。但在许多网络物理应用中,此视角过于粗略。例如车辆接近障碍物时,不仅需避免碰撞,还应遵守速度限值、加速度力限制以及急动度限制以防止伤害。从物理角度看,这些要求依赖于状态的导数。本文提出一种针对高阶平滑性约束的有限状态安全博弈构造方法。通过在离散状态空间上使用有限差分定义微分安全属性,刻画其表达能力,并将防护罩合成转化为对历史状态空间的普通安全博弈。给出一种合成算法,其防护罩恰好存储k个过去状态(对应k阶属性),并证明该内存需求是必要的。描述了一种迭代合成过程,可生成最大化允许性的防护罩,按导数约束层级逐层处理。每一步解出约束后,利用结果剪枝后续状态空间,显著提升实际效率,避免探索已知不安全区域。

原文摘要 · Abstract (English)

Safety shields are runtime enforcement mechanisms that restrict the actions of a controller to guarantee safety. Classical shields are usually synthesised for state predicates: the current physical state is either safe or unsafe, and the shield disables precisely those actions that can force the system into an unsafe state in the future. In many cyber-physical applications this view is too coarse. A vehicle approaching an obstacle should not only avoid collision, but also respect speed regulations, force limits induced by acceleration, and jerk limits to prevent injuries. From a physical perspective, these requirements are predicated over the derivatives of the state. This paper develops a finite-state safety-game construction for such high-order smoothness constraints. We define differential safety properties using finite differences over a discretised state space, characterise their expressiveness, and reduce shield synthesis to an ordinary safety game over a history state space. We give a synthesis algorithm whose shields store exactly $k$ past states for properties of order $k$ and prove that this memory is necessary. We describe an iterative synthesis procedure for a maximally permissive shield that operates over hierarchies of derivative constraints. The algorithm solves constraints iteratively in increasing order and uses the solution at each iteration to prune the state space for the next constraint. This makes shield synthesis more efficient in practice, as the algorithm refrains from exploring large regions of the state space that are known to be unsafe.

安全防护高阶约束控制合成物理系统

Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。