{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T02:22:34Z","timestamp":1773282154290,"version":"3.50.1"},"reference-count":54,"publisher":"SAGE Publications","issue":"9","license":[{"start":{"date-parts":[[2020,6,16]],"date-time":"2020-06-16T00:00:00Z","timestamp":1592265600000},"content-version":"vor","delay-in-days":366,"URL":"http:\/\/www.sagepub.com\/licence-information-for-chorus"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["PRINCESS"],"award-info":[{"award-number":["PRINCESS"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011102","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["600623 STRANDS"],"award-info":[{"award-number":["600623 STRANDS"]}],"id":[{"id":"10.13039\/100011102","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/R026084\/1 RAIN"],"award-info":[{"award-number":["EP\/R026084\/1 RAIN"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["The International Journal of Robotics Research"],"published-print":{"date-parts":[[2019,8]]},"abstract":"<jats:p> 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 modeled 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: maximize the probability of finishing the task; maximize progress towards completion, if this is not possible; and minimize the expected time or cost required. We illustrate and evaluate our approach with a scalability evaluation in a simulated scenario, and report on its implementation in a robot performing service tasks in an office environment for long periods of time. <\/jats:p>","DOI":"10.1177\/0278364919856695","type":"journal-article","created":{"date-parts":[[2019,6,17]],"date-time":"2019-06-17T06:04:36Z","timestamp":1560751476000},"page":"1098-1123","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":52,"title":["Probabilistic planning with formal performance guarantees for mobile service robots"],"prefix":"10.1177","volume":"38","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0862-331X","authenticated-orcid":false,"given":"Bruno","family":"Lacerda","sequence":"first","affiliation":[{"name":"Oxford Robotics Institute, University of Oxford, UK"}]},{"given":"Fatma","family":"Faruq","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Birmingham, UK"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Birmingham, UK"}]},{"given":"Nick","family":"Hawes","sequence":"additional","affiliation":[{"name":"Oxford Robotics Institute, University of Oxford, UK"}]}],"member":"179","published-online":{"date-parts":[[2019,6,16]]},"reference":[{"key":"bibr1-0278364919856695","volume-title":"Principles of Model Checking","author":"Baier C","year":"2008"},{"key":"bibr2-0278364919856695","author":"Baier C","year":"2014","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"bibr3-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2007.339624"},{"key":"bibr4-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2010.5509503"},{"key":"bibr5-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2011.942115"},{"key":"bibr6-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1613\/jair.575"},{"key":"bibr7-0278364919856695","volume-title":"Proceedings of the 25th International Conference on Planning and Scheduling (ICAPS)","author":"Cashmore M","year":"2015"},{"key":"bibr8-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2013.6760374"},{"key":"bibr9-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1177\/0278364914522312"},{"key":"bibr10-0278364919856695","volume-title":"Formal Verification of Probabilistic Systems","author":"de Alfaro L","year":"1997"},{"key":"bibr11-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2013.11.030"},{"key":"bibr12-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2013.6631226"},{"key":"bibr13-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2298143"},{"key":"bibr14-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15297-9_9"},{"key":"bibr15-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.021"},{"key":"bibr16-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"bibr17-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025842019552"},{"key":"bibr18-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2015.08.008"},{"key":"bibr19-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2016.2636359"},{"key":"bibr20-0278364919856695","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"Hopcroft JE","year":"2006","edition":"3"},{"key":"bibr21-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2014.11.003"},{"key":"bibr22-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"bibr23-0278364919856695","volume-title":"Proceedings of 28th Conference on Uncertainty in Artificial Intelligence (UAI)","author":"Kolobov A","year":"2012"},{"key":"bibr24-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"bibr25-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011254632723"},{"key":"bibr26-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"bibr27-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6942756"},{"key":"bibr28-0278364919856695","volume-title":"Proceedings of AAAI Fall Symposium on Sequential Decision Making for Intelligent Agents (SDMIA)","author":"Lacerda B","year":"2015"},{"key":"bibr29-0278364919856695","volume-title":"Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI)","author":"Lacerda B","year":"2015"},{"key":"bibr30-0278364919856695","first-page":"3664","volume-title":"Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI)","author":"Lahijanian M","year":"2015"},{"key":"bibr31-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2011.2172150"},{"key":"bibr32-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2016.7799414"},{"key":"bibr33-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2016.2544339"},{"key":"bibr34-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461380"},{"key":"bibr35-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2008.4543343"},{"key":"bibr36-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/ECMR.2015.7324192"},{"key":"bibr37-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90110-9"},{"key":"bibr38-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2015.7139315"},{"key":"bibr39-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887"},{"key":"bibr40-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039363"},{"key":"bibr41-0278364919856695","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2016.XII.017"},{"key":"bibr42-0278364919856695","volume-title":"Proceedings of 28th AAAI Conference on Artificial Intelligence (AAAI)","author":"Sprauel J","year":"2014"},{"key":"bibr43-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24489-1_28"},{"key":"bibr44-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2013.6760491"},{"key":"bibr45-0278364919856695","volume-title":"Proceedings of 2012 European Conference on Artificial Intelligence (ECAI)","author":"Teichteil-K\u00f6nigsbuch F","year":"2012"},{"key":"bibr46-0278364919856695","volume-title":"Proceedings of the 26th AAAI Conference on Artificial Intelligence (AAAI)","author":"Teichteil-K\u00f6nigsbuch F","year":"2012"},{"key":"bibr47-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461330"},{"key":"bibr48-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2012.6426346"},{"key":"bibr49-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1985.12"},{"key":"bibr50-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2017.7989177"},{"key":"bibr51-0278364919856695","volume-title":"Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI)","author":"Veloso MM","year":"2015"},{"key":"bibr52-0278364919856695","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2013.6631296"},{"key":"bibr53-0278364919856695","first-page":"3418","volume-title":"Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI)","author":"Wray KH","year":"2015"},{"key":"bibr54-0278364919856695","unstructured":"Younes HLS, Littman ML (2004) PPDDL 1.0: An extension to PDDL for expressing planning domains with probabilistic effects. Technical Report CMU-CS-04-162, Carnegie Mellon University, Pittsburgh, PA."}],"container-title":["The International Journal of Robotics Research"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0278364919856695","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.1177\/0278364919856695","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0278364919856695","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.1177\/0278364919856695","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T13:58:34Z","timestamp":1740837514000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.1177\/0278364919856695"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,16]]},"references-count":54,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2019,8]]}},"alternative-id":["10.1177\/0278364919856695"],"URL":"https:\/\/doi.org\/10.1177\/0278364919856695","relation":{},"ISSN":["0278-3649","1741-3176"],"issn-type":[{"value":"0278-3649","type":"print"},{"value":"1741-3176","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,6,16]]}}}