Optimal Policy Generation for Partially Satisfiable Co-Safe LTL Specifications

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Colleges, School and Institutes


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.


Original languageEnglish
Title of host publicationProc. 24th International Joint Conference on Artificial Intelligence (IJCAI'15)
EditorsQiang Yang, Michael Wooldridge
Publication statusPublished - 20 Jul 2015
EventInternational Joint Conference on Artificial Intelligence, 24th (ICJAI 2015) - Buenos Aires, Argentina
Duration: 25 Jul 201531 Jul 2015


ConferenceInternational Joint Conference on Artificial Intelligence, 24th (ICJAI 2015)