Probabilistic Shielding for Safe Reinforcement Learning

Abstract

at least some probability p. This framework comes from a probabilistic version of what is usually called the “safety” In real-life scenarios, a Reinforcement Learning (RL) agent aiming to maximise their reward, must often also behave in a fragment of Linear Temporal Logic (LTL) (Alshiekh et al. safe manner, including at training time. Thus, much attention 2018) (Jansen et al. 2020). Although, for simplicity’s sake, in recent years has been given to Safe RL, where an agent we consider only a subset of that safety fragment, i.e. safety aims to learn an optimal policy among all policies that satisfy definable by state-avoidance, it is possible to reduce the a given safety constraint. However, strict safety guarantees whole fragment to that subset with the usual trick of making are often provided through approaches based on linear pro- a product between the automaton representing the LTL prop- gramming, and thus have limited scaling. In this paper we erty and the MDP (Alshiekh et al. 2018) (Jansen et al. 2020). present a new, scalable method, which enjoys strict formal Thus, the model we use can capture many real-life scenarios, guarantees for Safe RL, in the case where the safety dynam- like a robot’s task of reaching a goal position while avoiding ics of the Markov Decision Process (MDP) are known, and objects on his path. safety is defined as an undiscounted probabilistic avoidance property. Our approach is based on state-augmentation of the Our approach is, to our knowledge, in the framework we MDP, and on the design of a shield that restricts the actions consider, the first approach not based on Linear Program- available to the agent. We show that our approach provides ming (Karmarkar 1984) that gives strict formal guarantees a strict formal safety guarantee that the agent stays safe at for safety throughout learning and at test time. Instead of training and test time. Furthermore, we demonstrate that our using Linear Programming, that has limite