Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Main Track. Pages 1587-1592.
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.
@inproceedings{ijcai2015p227,
title = {Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications},
author = {Lacerda, Bruno and Parker, David and Hawes, Nick},
booktitle = {Proceedings of the Twenty-Fourth International Joint Conference on
Artificial Intelligence, {IJCAI-15}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Qiang Yang and Michael Wooldridge},
pages = {1587--1592},
year = {2015},
month = {7},
note = {Main Track},
url = {https://ijcai.org/proceedings/2015/227},
}
TY - CPAPER TI - Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications AU - Lacerda, Bruno AU - Parker, David AU - Hawes, Nick T2 - Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15 PB - International Joint Conferences on Artificial Intelligence PY - 2015 SP - 1587 EP - 1592 UR - https://ijcai.org/proceedings/2015/227 ER -Copied
Machine-readable versions of this paper, for tools and AI agents: