高阶安全防护
Shielding for Higher-Order Safety
浏览论文内容
中文总结 AI 辅助
本文针对网络物理系统的高阶安全约束，提出有限状态安全博弈构造方法，给出对应防护综合算法，提升了防护综合的效率。
中文摘要 AI 辅助
安全防护（Safety shields）是一种运行时执行机制，用于限制控制器的动作以保障安全性。经典防护通常针对状态谓词进行综合：当前物理状态要么安全要么不安全，防护会精确禁用那些可能导致系统未来进入不安全状态的动作。在许多网络物理应用中，这种视角过于粗糙：接近障碍物的车辆不仅要避免碰撞，还需遵守速度规定、加速度引发的力限制以及防止人员受伤的加加速度（jerk）限制。从物理角度看，这些要求基于状态的导数。本文针对这类高阶平滑约束，提出了一种有限状态安全博弈构造方法：我们通过离散状态空间上的有限差分定义微分安全属性，刻画其表达能力，并将防护综合归约为历史状态空间上的普通安全博弈；我们给出一种综合算法，对于k阶属性，其防护恰好存储k个过去状态，并证明该内存是必要的；我们还描述了一种用于最大化许可性的防护的迭代综合过程，该过程基于导数约束的层次结构运行，按递增顺序迭代求解约束，并使用每次迭代的解为下一个约束修剪状态空间，这使得防护综合在实践中更高效，因为算法避免探索已知为不安全的大状态空间区域。
英文摘要
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.
