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