Applying Reinforcement Learning to Railway Interlocking Verification
Abstract
Formal verification (FV) is an increasingly popular method for guaranteeing correctness in safety critical systems. As an application domain, the railway shares a history with FV spanning decades. Interlockings, the systems responsible for monitoring safety violations within a bounded railway network, necessitate robust means of testing du to their high integrity level. FV has been shown to support this process yet widespread adoption in industry has been hindered by certain limitations. In this thesis we explore verification techniques applied to railway interlockings and how machine learning can be used to support SAT-based model checking in particular. We provide a brief overview of both disciplines and the necessary background required to understand, replicate and advance our approach. We propose the implementation of a reinforcement learning environment modelling the state space of a ladder logic program responsible for encoding basic safety properties for a pedestrian controlled light crossing. An RL agent is then successfully trained to output two sets of minimal transitions for traversing the state space to aid in identifying loop free paths for model checking.