Probabilistic planning with formal guarantees for mobile service robots

Bruno Lacerda, Fatma Faruq, David Parker, Nick Hawes

PosterID: 63
picture_as_pdf PDF
library_books Slides
library_books Poster
We present a framework for mobile service robot task planning and execution, based on the use of probabilistic verification techniques for the generation of optimal policies with attached formal performance guarantees. Our approach is based on a Markov decision process model of the robot in its environment, encompassing a topological map where nodes represent relevant locations in the environment, and a range of tasks that can be executed in different locations. The navigation in the topological map is modelled stochastically for a specific time of day. This is done by using spatio-temporal models that provide, for a given time of day, the probability of successfully navigating between two topological nodes, and the expected time to do so. We then present a methodology to generate cost optimal policies for tasks specified in co-safe linear temporal logic. Our key contribution is to address scenarios in which the task may not be achievable with probability one. We introduce a task progression function and present an approach to generate policies that are formally guaranteed to, in decreasing order of priority: maximise the probability of finishing the task; maximise progress towards completion, if this is not possible; and minimise the expected time or cost required. We illustrate and evaluate our approach with a scalability evaluation in a simulated scenario, and reporting on its implementation in a robot performing service tasks in an office environment for long periods of time.

Session E3: Planning with Uncertainty
Canb 10/29/2020, 01:00 – 02:00
10/30/2020, 21:00 – 22:00
Paris 10/28/2020, 15:00 – 16:00
10/30/2020, 11:00 – 12:00
NYC 10/28/2020, 10:00 – 11:00
10/30/2020, 06:00 – 07:00
LA 10/28/2020, 07:00 – 08:00
10/30/2020, 03:00 – 04:00