It's Time to Play Safe: Shield Synthesis for Timed Systems
Roderick Bloem, Peter Gj{\o}l Jensen, Bettina K\"onighofer, Kim, Guldstrand Larsen, Florian Lorber, Alexander Palmisano

TL;DR
This paper introduces a method for synthesizing timed shields from safety properties to ensure safety in real-time systems with minimal interference, including new constructions and guarantees on recovery time.
Contribution
It presents the concept of timed shields, including pre-shields and post-shields, with extensions for recovery guarantees, applied to safety in reinforcement learning for car platoons.
Findings
Timed post-shields effectively enforce safety during learning and execution.
The approach minimizes system interference while ensuring safety.
Recovery time guarantees improve safety assurance in real-time systems.
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
