Is verification a requisite for safe adaptive robots?

This paper argues in favour of using formal methods to ensure safety of deployed stochastic policies learned by robots in unstructured environments. It has been demonstrated that multi-objective learning alone is not sufficient to ensure globally safe behaviours in such robots, whereas learning-specific methods yield deterministic policies which are less flexible or effective in practice. Under certain restrictions on state-space, modelling safety using probabilistic computational tree logic and ensuring such safety via automated repair can overcome these shortcomings. Promising results are obtained on a realistic setup and pros and cons of such method are discussed.