Provably-correct stochastic motion planning with safety constraints. Yoo, C, Fitch, R, & Sukkarieh, S In 2013 IEEE International Conference on Robotics and Automation, pages 981–986, May, 2013. ISSN: 1050-4729doi abstract bibtex 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.
@inproceedings{yoo_provably-correct_2013,
title = {Provably-correct stochastic motion planning with safety constraints},
doi = {10.1109/ICRA.2013.6630692},
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.},
booktitle = {2013 {IEEE} {International} {Conference} on {Robotics} and {Automation}},
author = {Yoo, C and Fitch, R and Sukkarieh, S},
month = may,
year = {2013},
note = {ISSN: 1050-4729},
keywords = {Markov decision process formalism, Markov processes, Mobile communication, PCTL, Robots, arbitrary weighted cost function, control policy analysis, control policy synthesis, control system synthesis, formal methods, formal verification, mission success probability maximisation, mobile robots, mobility prediction methods, model checking, outdoor robots, path planning, probabilistic computation tree logic, probabilistic logic, probabilistic success threshold, probability, provably-correct stochastic motion planning, quantitative safety measure, reward maximisation, risk levels, risk minimisation, safety constraints, safety threshold, stochastic outdoor navigation domain, stochastic path planning, time-to-completion minimisation, trees (mathematics)},
pages = {981--986}
}
Downloads: 0
{"_id":"3acE6fFAq6cKYHpeD","bibbaseid":"yoo-fitch-sukkarieh-provablycorrectstochasticmotionplanningwithsafetyconstraints-2013","authorIDs":[],"author_short":["Yoo, C","Fitch, R","Sukkarieh, S"],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Provably-correct stochastic motion planning with safety constraints","doi":"10.1109/ICRA.2013.6630692","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.","booktitle":"2013 IEEE International Conference on Robotics and Automation","author":[{"propositions":[],"lastnames":["Yoo"],"firstnames":["C"],"suffixes":[]},{"propositions":[],"lastnames":["Fitch"],"firstnames":["R"],"suffixes":[]},{"propositions":[],"lastnames":["Sukkarieh"],"firstnames":["S"],"suffixes":[]}],"month":"May","year":"2013","note":"ISSN: 1050-4729","keywords":"Markov decision process formalism, Markov processes, Mobile communication, PCTL, Robots, arbitrary weighted cost function, control policy analysis, control policy synthesis, control system synthesis, formal methods, formal verification, mission success probability maximisation, mobile robots, mobility prediction methods, model checking, outdoor robots, path planning, probabilistic computation tree logic, probabilistic logic, probabilistic success threshold, probability, provably-correct stochastic motion planning, quantitative safety measure, reward maximisation, risk levels, risk minimisation, safety constraints, safety threshold, stochastic outdoor navigation domain, stochastic path planning, time-to-completion minimisation, trees (mathematics)","pages":"981–986","bibtex":"@inproceedings{yoo_provably-correct_2013,\n\ttitle = {Provably-correct stochastic motion planning with safety constraints},\n\tdoi = {10.1109/ICRA.2013.6630692},\n\tabstract = {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.},\n\tbooktitle = {2013 {IEEE} {International} {Conference} on {Robotics} and {Automation}},\n\tauthor = {Yoo, C and Fitch, R and Sukkarieh, S},\n\tmonth = may,\n\tyear = {2013},\n\tnote = {ISSN: 1050-4729},\n\tkeywords = {Markov decision process formalism, Markov processes, Mobile communication, PCTL, Robots, arbitrary weighted cost function, control policy analysis, control policy synthesis, control system synthesis, formal methods, formal verification, mission success probability maximisation, mobile robots, mobility prediction methods, model checking, outdoor robots, path planning, probabilistic computation tree logic, probabilistic logic, probabilistic success threshold, probability, provably-correct stochastic motion planning, quantitative safety measure, reward maximisation, risk levels, risk minimisation, safety constraints, safety threshold, stochastic outdoor navigation domain, stochastic path planning, time-to-completion minimisation, trees (mathematics)},\n\tpages = {981--986}\n}\n\n","author_short":["Yoo, C","Fitch, R","Sukkarieh, S"],"key":"yoo_provably-correct_2013","id":"yoo_provably-correct_2013","bibbaseid":"yoo-fitch-sukkarieh-provablycorrectstochasticmotionplanningwithsafetyconstraints-2013","role":"author","urls":{},"keyword":["Markov decision process formalism","Markov processes","Mobile communication","PCTL","Robots","arbitrary weighted cost function","control policy analysis","control policy synthesis","control system synthesis","formal methods","formal verification","mission success probability maximisation","mobile robots","mobility prediction methods","model checking","outdoor robots","path planning","probabilistic computation tree logic","probabilistic logic","probabilistic success threshold","probability","provably-correct stochastic motion planning","quantitative safety measure","reward maximisation","risk levels","risk minimisation","safety constraints","safety threshold","stochastic outdoor navigation domain","stochastic path planning","time-to-completion minimisation","trees (mathematics)"],"downloads":0},"bibtype":"inproceedings","biburl":"https://bibbase.org/zotero/tillhofmann","creationDate":"2019-12-09T14:42:18.222Z","downloads":0,"keywords":["markov decision process formalism","markov processes","mobile communication","pctl","robots","arbitrary weighted cost function","control policy analysis","control policy synthesis","control system synthesis","formal methods","formal verification","mission success probability maximisation","mobile robots","mobility prediction methods","model checking","outdoor robots","path planning","probabilistic computation tree logic","probabilistic logic","probabilistic success threshold","probability","provably-correct stochastic motion planning","quantitative safety measure","reward maximisation","risk levels","risk minimisation","safety constraints","safety threshold","stochastic outdoor navigation domain","stochastic path planning","time-to-completion minimisation","trees (mathematics)"],"search_terms":["provably","correct","stochastic","motion","planning","safety","constraints","yoo","fitch","sukkarieh"],"title":"Provably-correct stochastic motion planning with safety constraints","year":2013,"dataSources":["9pYjFWPBodPyDyb7N"]}