Skip to main content

Autonomous urban driving

Supervisor

Suitable for

Abstract

This project is concerned with synthesising strategies for autonomous driving directly from requirements expressed in temporal logic, so that they are correct by construction. Probability is used to quantify information about hazards, such as accidents hotspots. Inspired by the DARPA Urban Challenge, a method for synthesising strategies (controllers) from multi-objective requirements was developed and validated on map data for villages in Oxfordshire (http://www.prismmodelchecker.org/bibitem.php?key=CKSW13). The idea is to develop the techniques further, to allow high-level navigation based on waypoints, and to develop strategies for avoiding threats, such as road blockage, at runtime. In the longer term, the goal is to validate the methods on realistic scenarios in collaboration with the Mobile Robotics Group. The project will suit a student interested in theory or software implementation. For more information about the project see http://www.veriware.org/autonomous.php