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) 引入了确保强安全性保证的离线与在线防护罩构建方法。实验评估凸显了新防护罩的实用优势及其计算可行性。