Safe Reinforcement Learning via Probabilistic Shields
  This paper targets the efficient construction of a safety shield for decision
making in scenarios that incorporate uncertainty. Markov decision processes
(MDPs) are prominent models to capture such planning problems. Reinforcement
learning (RL) is a machine learning technique to determine near-optimal
policies in MDPs that may be unknown prior to exploring the model. However,
during exploration, RL is prone to induce behavior that is undesirable or not
allowed in safety- or mission-critical contexts. We introduce the concept of a
probabilistic shield that enables decision-making to adhere to safety
constraints with high probability. In a separation of concerns, we employ
formal verification to efficiently compute the probabilities of critical
decisions within a safety-relevant fragment of the MDP. We use these results to
realize a shield that is applied to an RL algorithm which then optimizes the
actual performance objective. We discuss tradeoffs between sufficient progress
in exploration of the environment and ensuring safety. In our experiments, we
demonstrate on the arcade game PAC-MAN and on a case study involving service
robots that the learning efficiency increases as the learning needs orders of
magnitude fewer episodes.
