Non-Deterministic Planning with Temporally Extended Goals: LTL over Finite and Infinite Traces

Authors

  • Alberto Camacho University of Toronto
  • Eleni Triantafillou University of Toronto
  • Christian Muise Massachusetts Institute of Technology
  • Jorge Baier Pontificia Universidad Católica de Chile
  • Sheila McIlraith University of Toronto

DOI:

https://doi.org/10.1609/aaai.v31i1.11058

Keywords:

LTL, FOND, infinite, planning, synthesis, temporally extended goals

Abstract

Temporally extended goals are critical to the specification of a diversity of real-world planning problems. Here we examine the problem of non-deterministic planning with temporally extended goals specified in linear temporal logic (LTL), interpreted over either finite or infinite traces. Unlike existing LTL planners, we place no restrictions on our LTL formulae beyond those necessary to distinguish finite from infinite interpretations. We generate plans by compiling LTL temporally extended goals into problem instances described in the Planning Domain Definition Language that are solved by a state-of-the-art fully observable non-deterministic planner. We propose several different compilations based on translations of LTL to (Büchi) alternating or (Büchi) non-deterministic finite state automata, and evaluate various properties of the competing approaches. We address a diverse spectrum of LTL planning problems that, to this point, had not been solvable using AI planning techniques, and do so in a manner that demonstrates highly competitive performance.

Downloads

Published

2017-02-12

How to Cite

Camacho, A., Triantafillou, E., Muise, C., Baier, J., & McIlraith, S. (2017). Non-Deterministic Planning with Temporally Extended Goals: LTL over Finite and Infinite Traces. Proceedings of the AAAI Conference on Artificial Intelligence, 31(1). https://doi.org/10.1609/aaai.v31i1.11058

Issue

Section

AAAI Technical Track: Reasoning under Uncertainty