Supervisor

Suitable for

Abstract

Autonomous robots have numerous applications in scenarios such as warehouse management, planetary exploration, or search and rescue. In view of environmental uncertainty, such scenarios are modelled using Markov decision processes. The goals (e.g. the goods should be delivered to location A while avoiding the hazardous location B) can be conveniently specified using temporal logic, from which correct-by-construction controllers (strategies) can be generated. This project aims to develop a PRISM model of a system of robots for a particular scenario so that safety and effectiveness of their cooperation is guaranteed. Techniques based on machine learning, and specifically real-time dynamic programming (http://www.prismmodelchecker.org/papers/atva14.pdf), will be utilised to generate controllers directly from temporal logic goals. This project will suit a student interested in machine learning and software implementation.