@techreport{057d3d68835a4854a95c820128ded3fe,
title = "It's Time to Play Safe: Shield Synthesis for Timed 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 ensure the safety in a reinforcement learning setting for controlling a platoon of cars, during the learning and execution phase, and study the effect. ",
keywords = "cs.LO, cs.LG",
author = "Roderick Bloem and Jensen, {Peter Gj{\o}l} and Bettina K{\"o}nighofer and Larsen, {Kim Guldstrand} and Florian Lorber and Palmisano, {Alexander Matteo}",
note = "Submitted to RV2020",
year = "2020",
month = jun,
day = "30",
language = "English",
series = "arXiv.org e-Print archive",
publisher = "Cornell University Library",
type = "WorkingPaper",
institution = "Cornell University Library",
}