---
title: "Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications"
authors:
  - "Bruno Lacerda"
  - "David Parker"
  - "Nick Hawes"
doi: ""
url: "https://ijcai.org/proceedings/2015/227"
pdf: "https://ijcai.org/proceedings/2015/0227.pdf"
venue: "Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence"
year: 2015
pages: "1587-1592"
track: "Main Track"
keywords:
---

# Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications

Bruno Lacerda, David Parker, Nick Hawes

*Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence*, 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.