Declarative Specifications for Efficient and Safe Reinforcement Learning

Abstract

In recent years, there have been several developments combining reinforcement learning (RL) with techniques from theoretical computer science fields such as logic and formal methods. The main goal of these works was to improve training speed and quality, and in some cases also enforce safety constraints. In this dissertation, we present several works that followed this research line. First, we explore research directions concerning reward machines (RMs), an approach proposed to improve training speed and train agents in achieving tasks that require temporally extended behaviours. Given an abstraction of the environment in which the agent acts, we show how we can generate a reward machine from the set of all plans to achieve the task in the abstraction. As the plans come from an abstraction of the environment, the agent still needs to learn how to enact them in order to achieve the task, which is done via RL. Then, we synthesise reward machines in a cooperative multi-agent scenario by using Alternating-time Temporal Logic (ATL) formulas encoding coalition tasks. By model checking the ATL formula, we can obtain a strategy (if there is any) for the coalition to achieve the task, which is then translated to a RM and used to train the agents. We then present an extension of reward machines that endows them with a pushdown stack, obtaining a "pushdown reward machine" (pdRM). As pdRMs are based on pushdown automata, they can encode a strictly larger set of tasks compared to standard RMs, while still enabling more efficient learning compared to other approaches. Finally, we present a work in safe RL, where agents must also respect safety constraints. We present how to enforce safety constraints using pure-past linear-time temporal logic (PPLTL). Each action is associated to a PPLTL formula, and by evaluating the formulas at each timestep we determine which actions the agent can to perform, guaranteeing constraint satisfaction.