고차 안전을 위한 보호 장치

Shielding for Higher-Order Safety

안전 보호 장치는 제어기의 동작을 제한하여 안전성을 보장하는 런타임 강제 메커니즘입니다. 기존의 보호 장치는 일반적으로 상태 예측 기반으로 설계됩니다. 즉, 현재 시스템의 물리적 상태가 안전하거나 위험한 상태이며, 보호 장치는 미래에 시스템을 위험한 상태로 만들 수 있는 특정 동작들을 비활성화합니다. 그러나 많은 사이버-물리 시스템 응용 분야에서 이러한 방식은 너무 단순할 수 있습니다. 예를 들어, 장애물을 향해 접근하는 차량은 충돌을 피하는 것 외에도 속도 제한, 가속으로 인한 힘 제한, 그리고 부상을 예방하기 위한 급격한 변화(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.