Model Checking for Trustworthy Reasoning in Autonomous Driving

This archive contains code and analysis details for two case studies investigating the use of discrete model checking and closed-loop control for obstacle avoidance. The aim of the research was to develop an approach using model checking for online reasoning which is computationally efficient and transparent as a first step towards trustworthy reasoning for fully autonomous vehicles. To this end, we develop a bespoke model checking approach capable of online reasoning on a low-powered robot. In our first case study, we focus on avoiding obstacles without making progress to a goal and then extend our approach to accomodate goal-directed behaviour in our second case study. We discuss the merits and limitations of the approach and suggest avenues for further work.