Policy Generation with Probabilistic Guarantees for Long-term Autonomy of a Mobile Service Robot

7^th March 2017, 13:00 Ashton Lecture Theater
Dr. Bruno Lacerda
School of Computer Science
University of Birmingham
Edgbaston, Birmingham, B15 2TT
United Kingdom

Abstract

In this talk, I will describe some of the work developed at the University of Birmingham, tackling the issue of high-level control for mobile service robots. In particular, I will discuss two approaches that use probabilistic model checking techniques for generating policies for Markov decision process models of mobile robots, using (co-safe) linear temporal logic specifications. First, I will describe an approach that deals with specifications which are not satisfiable with probability one in the model. For this class of specification, we use a metric that represents progression towards the goal, i.e., that represents doing "as much as possible". We then minimise expected time for the robot to get to a state where it cannot get closer to the satisfaction of the linear temporal logic task, while doing as much of it as possible. Then, I will present a more recent approach, where we use time-bounded specifications, instead of expected time minimisation, and focus on oversubscription planning. In this case, we solve a multi-objective problem, using the expected time minimisation to prune the timed model such that we can greatly reduce the state space of the time-bounded problem while still achieving good approximations of the optimal Pareto front.