Trustworthy Systems

LTL goal specifications revisited


Andreas Bauer and Patrik Haslum


Australian National University


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

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