Search papers, labs, and topics across Lattice.
This paper introduces a novel finite-state safety-game construction that incorporates high-order smoothness constraints for safety shields in cyber-physical systems. By defining differential safety properties using finite differences over a discretized state space, the authors develop an efficient synthesis algorithm that minimizes state space exploration while ensuring compliance with multiple derivative constraints. The key result is a maximally permissive shield that effectively balances safety with operational flexibility by storing only the necessary past states for enforcing safety properties of order \(k\).
Safety shields can now enforce complex derivative constraints without sacrificing efficiency, enabling safer and more flexible control in cyber-physical systems.
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.
