Controller synthesis for robot coordination
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.