是时候安全行事了：时序系统的屏蔽合成

安全关键实时系统中的错误行为可能造成严重后果。在本文中，我们展示了如何由给定为时序自动机的时序安全性质合成时序屏蔽。时序屏蔽在尽可能少地干预系统的同时强制运行系统的安全性。我们提出时序后屏蔽和时序前屏蔽。时序前屏蔽置于系统之前，提供一组安全输出。该集合限制了系统的选择。时序后屏蔽实现于系统之后。它监控系统并仅在必要时修正系统的输出。我们进一步扩展时序后屏蔽的构造，以提供对恢复阶段的保证，即规范违例与可将完全控制权交还系统的时刻之间的时间。在我们的实验结果中，我们在强化学习设定中使用时序后屏蔽来确保车辆队列控制的安全性（在学习和执行阶段），并研究其效果。