Testing and Symbolic Analysis For Reinforcement Learning

Reinforcement learning (RL) is a type of active learning whereby an agent learns to act in an environment by interacting with it. RL has applications in many domains, including robotics, gaming, electronics, healthcare, water management systems, etc. The majority of real-world applications of RL, such as those in robotics, necessitate a preliminary training phase in a simulation environment. It is otherwise either infeasible or prohibitively expensive to train the agent in a real-world setting. At the same time, there are clear advantages to be gained from the use of formal methods for the enhancement of software qualities. Given that RL and its applications are computer programs, the objective of this thesis is to employ formal methods, in particular pecification, testing, and symbolic execution, in order to improve the reliability and explainability of reinforcement learning.