Model checking for trustworthy reasoning in autonomous driving

This thesis proposes model checking for trustworthy reasoning in autonomous driving. We combine closed-loop input control and model checking to plan sequences of closed loop controllers for obstacle avoidance in real-time—the former for its superior reactivity to immediate stimuli, and the latter for its strength in modal reasoning. In addition, as both closed-loop control and model checking are transparent, decisions can in principle be explained. To demonstrate our approach, we implement a bespoke model checker on low powered autonomous robot, an additional measure to further promote resource efficient planning. We conduct two case studies. In the first we focus simply on avoiding obstacles to investigate whether using model checking for real-time planning and obstacle avoidance is reliable on our platform. In the second we extend our approach to support goal-directed obstacle avoidance an again characterise its reliability. We show that it is possible to use model checking to develop an approach to real-time obstacle avoidance which is light on resources, transparent, and suitable for online decision-making.