Robust Policy Optimisation with RL

Several formal verification methods exist to generate policies for dynamical systems which ensure they satisfy some reachability specification, for example, reach a goal region without hitting an obstacle. In stochastic settings, often modelled as Markov decision processes (MDPs), we generate robust policies that provide guarantees of worst-case scenario satisfaction probability for the specification. A common approach involves creating a finite abstraction of our system and then using value/policy iteration to generate a policy to navigate the system.

While these methods are good at satisfying these specifications, they do not give us fine-grained control. To the best of our knowledge there is no published method that allows us to generate robust policies via MDP abstraction methods, while also optimising for a secondary objective without sacrificing our safety guarantees. For example, there is no current way to change a policy after abstraction to be more energy efficient without sacrificing satisfaction guarantees.

To overcome this gap in the research, I propose a novel modification to policy synthesis via robust permissive policy synthesis. These permissive policies produce a set of actions at each state. I prove that we achieve robust safety guarantees with these permissive policies and can thus resolve the action non-determinism runtime via any online control method. We instantiate our novel framework, using reinforcement learning methods to choose actions that optimise for secondary objectives. This application is non-trivial due to the agent having to deal with a continuous action space that changes at each step, dictated by the robust permissive policies that we have synthesized. Finally, we explore the creation of these action sets, proposing that dynamically-shaped “irregular-ball” give us the most control while maintaining a high level of safety. We show via thorough experimentation that our reinforcement learning agent successfully uses them to achieve the secondary objectives while still navigating the system safely.

Please download my final write-up from above. We were able to achieve very strong results, beating all other known solutions. In this write-up, I demonstrate strong theoretical results, rigorously proving my claims, and then go on to show that our hypothesis holds up after extensive experimentation. This work was awarded a distinction, and we are looking to publish our findings. This was supervised by Alessandro Abate and Thom Badings.