Abstract
Deep reinforcement learning has been successfully applied to many controltasks, but the application of such agents in safety-critical scenarios has beenlimited due to safety concerns. Rigorous testing of these controllers ischallenging, particularly when they operate in probabilistic environments dueto, for example, hardware faults or noisy sensors. We propose MOSAIC, analgorithm for measuring the safety of deep reinforcement learning agents instochastic settings. Our approach is based on the iterative construction of aformal abstraction of a controller's execution in an environment, and leveragesprobabilistic model checking of Markov decision processes to produceprobabilistic guarantees on safe behaviour over a finite time horizon. Itproduces bounds on the probability of safe operation of the controller fordifferent initial configurations and identifies regions where correct behaviourcan be guaranteed. We implement and evaluate our approach on agents trained forseveral benchmark control problems.