Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1109/ICRA.2013.6630692 | ICRA |
Keywords | Field | DocType |
provably-correct stochastic motion planning,trees (mathematics),model checking,control system synthesis,probabilistic computation tree logic,mobile robots,pctl,quantitative safety measure,stochastic outdoor navigation domain,probabilistic logic,risk levels,probabilistic success threshold,mission success probability maximisation,path planning,mobility prediction methods,time-to-completion minimisation,reward maximisation,arbitrary weighted cost function,stochastic path planning,risk minimisation,formal methods,safety constraints,control policy analysis,markov decision process formalism,control policy synthesis,outdoor robots,markov processes,formal verification,probability,safety threshold,mobile communication,robots | Motion planning,Mathematical optimization,Model checking,Markov process,Markov decision process,Probabilistic CTL,Probabilistic logic,Formal methods,Mathematics,Formal verification | Conference |
Volume | Issue | ISSN |
2013 | 1 | 1050-4729 |
ISBN | Citations | PageRank |
978-1-4673-5641-1 | 11 | 0.61 |
References | Authors | |
9 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chanyeol Yoo | 1 | 17 | 5.58 |
| Robert Fitch | 2 | 323 | 38.97 |
| Salah Sukkarieh | 3 | 1142 | 141.84 |