Abstract
In recent years, deep reinforcement learning (DRL) approaches have generatedhighly successful controllers for a myriad of complex domains. However, theopaque nature of these models limits their applicability in aerospace systemsand safety-critical domains, in which a single mistake can have direconsequences. In this paper, we present novel advancements in both the trainingand verification of DRL controllers, which can help ensure their safe behavior.We showcase a design-for-verification approach utilizing k-induction anddemonstrate its use in verifying liveness properties. In addition, we also givea brief overview of neural Lyapunov Barrier certificates and summarize theircapabilities on a case study. Finally, we describe several other novelreachability-based approaches which, despite failing to provide guarantees ofinterest, could be effective for verification of other DRL systems, and couldbe of further interest to the community.