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:
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: