# It's Time to Play Safe: Shield Synthesis for Timed Systems

arXiv: https://arxiv.org/abs/2006.16688 · HTML: https://mlsanity.com/paper/2006.16688/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Jun 2020.

## Built on by (most cited first, 4 of 4)

- [Shielding Atari Games with Bounded Prescience](https://mlsanity.com/paper/2101.08153/) (2021)
- [Dynamic Shielding for Reinforcement Learning in Black-Box Environments](https://mlsanity.com/paper/2207.13446/) (2022)
- [Adaptive GR(1) Specification Repair for Liveness-Preserving Shielding in Reinforcement Learning](https://mlsanity.com/paper/2511.02605/) (2025)
- [Shielded Controller Units for RL with Operational Constraints Applied to Remote Microgrids](https://mlsanity.com/paper/2512.01046/) (2025)

## Abstract (arXiv)

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.