Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications
Abstract
We present a method to calculate cost-optimal policies for co-safe linear temporal logic task specifications over a Markov decision process model of a stochastic system. Our key contribution is to address scenarios in which the task may not be achievable with probability one. We formalise a task progression metric and, using multi-objective probabilistic model checking, generate policies that are formally guaranteed to, in decreasing order of priority: maximise the probability of finishing the task; maximise progress towards completion, if this is not possible; and minimise the expected time or cost required. We illustrate and evaluate our approach in a robot task planning scenario, where the task is to visit a set of rooms that may be inaccessible during execution.
Cite
Text
Lacerda et al. "Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications." International Joint Conference on Artificial Intelligence, 2015.Markdown
[Lacerda et al. "Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications." International Joint Conference on Artificial Intelligence, 2015.](https://mlanthology.org/ijcai/2015/lacerda2015ijcai-optimal/)BibTeX
@inproceedings{lacerda2015ijcai-optimal,
title = {{Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications}},
author = {Lacerda, Bruno and Parker, David and Hawes, Nick},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {2015},
pages = {1587-1593},
url = {https://mlanthology.org/ijcai/2015/lacerda2015ijcai-optimal/}
}