Shielding is a prominent model-based technique to ensure safety of autonomous agents. Classical shielding aims to ensure that nothing bad ever happens and comes with strong guarantees about safety and maximal permissiveness. However, shielding systems for probabilistic safety, where something bad is allowed to happen with an acceptable probability, has proven to be more intricate. This paper presents a formal framework that conservatively extends classical shields to probabilistic safety. In this framework, we (i) demonstrate the impossibility of preserving the strong guarantees on safety and permissiveness, (ii) provide natural shields with weaker guarantees, and (iii) introduce offline and online shield constructions ensuring strong safety guarantees. The empirical evaluation highlights the practical advantages of the new shields, as well as their computational feasibility.

翻译：防护是一种基于模型的先进技术，用于确保自主智能体的安全性。经典防护机制旨在保证绝对不发生危险事件，并提供关于安全性和最大许可性的强约束保证。然而，针对概率安全性的防护系统（允许以可接受概率发生危险事件）的实现已被证明更为复杂。本文提出一个形式化框架，将经典防护机制保守地扩展到概率安全性领域。在该框架中，我们(i)论证了无法同时保留安全性与许可性的强约束保证，(ii)提出具有较弱保证的自然防护机制，以及(iii)引入能确保强安全性保证的离线和在线防护构建方法。实验评估凸显了新防护机制的实际优势及其计算可行性。