Provably-correct stochastic motion planning with safety constraints

Publication Type:
Conference Proceeding
Proceedings - IEEE International Conference on Robotics and Automation, 2013, pp. 981 - 986
Issue Date:
Filename Description Size
06630692.pdfPublished version2.22 MB
Adobe PDF
Full metadata record
Formal methods based on the Markov decision process formalism, such as probabilistic computation tree logic (PCTL), can be used to analyse and synthesise control policies that maximise the probability of mission success. In this paper, we consider a different objective. We wish to minimise time-to-completion while satisfying a given probabilistic threshold of success. This important problem naturally arises in motion planning for outdoor robots, where high quality mobility prediction methods are available but stochastic path planning typically relies on an arbitrary weighted cost function that attempts to balance the opposing goals of finding safe paths (minimising risk) while making progress towards the goal (maximising reward). We propose novel algorithms for model checking and policy synthesis in PCTL that 1) provide a quantitative measure of safety and completion time for a given policy, and 2) synthesise policies that minimise completion time with respect to a given safety threshold. We provide simulation results in a stochastic outdoor navigation domain that illustrate policies with varying levels of risk. © 2013 IEEE.
Please use this identifier to cite or link to this item: