论文标题
是时候玩安全了：定时系统的盾牌合成
It's Time to Play Safe: Shield Synthesis for Timed Systems
论文作者
论文摘要
安全性实时系统中的错误行为可能会造成严重的后果。在本文中，我们展示了如何从定时安全性的定时安全性属性中综合定时屏蔽。定时的盾牌在尽可能少地干扰系统的同时，执行运行系统的安全性。我们提出定时的弹药和定时弹药。定时屏蔽将放置在系统之前，并提供一组安全输出。该集合限制了系统的选择。系统后实现定时屏蔽。它仅在必要时才监视系统并纠正系统的输出。我们进一步扩展了定时的弹药后施工，以提供恢复阶段的保证，即规范违规和可以将完全控制的点交给系统之间的时间。在我们的实验结果中，我们使用定时的弹药后来确保在学习和执行阶段进行加固学习环境中的安全性，以控制一排汽车，并研究效果。
Erroneous behaviour in safety critical real-time systems may inflict serious consequences. In this paper, we show how to synthesize timed shields from timed safety properties given as timed automata. A timed shield enforces the safety of a running system while interfering with the system as little as possible. We present timed post-shields and timed pre-shields. A timed pre-shield is placed before the system and provides a set of safe outputs. This set restricts the choices of the system. A timed post-shield is implemented after the system. It monitors the system and corrects the system's output only if necessary. We further extend the timed post-shield construction to provide a guarantee on the recovery phase, i.e., the time between a specification violation and the point at which full control can be handed back to the system. In our experimental results, we use timed post-shields to ensure the safety in a reinforcement learning setting for controlling a platoon of cars, during the learning and execution phase, and study the effect.
