Skip to main content

TS

LTL goal specifications revisited

Authors

Andreas Bauer and Patrik Haslum

NICTA

Australian National University

Abstract

The language of linear temporal logic (\LTL) has been proposed as a formalism for specifying temporally extended goals and search control constraints. However, the semantics of \LTL is defined \wrt \emph{infinite} state sequences, while a finite plan generates only a finite trace. This necessitates the use of a finite trace semantics for \LTL. The approach commonly adopted in planning is to evaluate \LTL formulae on an infinite extension of the finite trace, obtained by infinitely repeating the last state. We study several aspects of this finite \LTL semantics: we show its satisfiability problem is PSpace-complete (same as normal LTL), show that it complies with all equivalence laws that hold under standard (infinite) \LTL semantics, and compare it with other finite trace semantics for \LTL proposed in planning and in runtime verification. We also examine different mechanisms for determining whether or not a finite trace satisfies or violates an \LTL formula, interpreted using the infinite extension semantics.

BibTeX Entry

  @inproceedings{Bauer_Haslum_10,
    publisher        = {IOS Press},
    author           = {Bauer, Andreas and Haslum, Patrik},
    month            = aug,
    year             = {2010},
    keywords         = {planning, ltl, finite trace semantics},
    title            = {{LTL} Goal Specifications Revisited},
    booktitle        = {European Conference on Arificial Intelligence},
    address          = {Lisbon, Portugal}
  }

Download

Served by Apache on Linux on seL4.