LTL Goal Specifications Revisited

13 years 21 days ago
LTL Goal Specifications Revisited
The language of linear temporal logic (LTL) has been proposed as a formalism for specifying temporally extended goals and search control constraints in planning. However, the semantics of LTL is defined wrt. infinite state sequences, while a finite plan generates only a finite trace. This necessitates the use of a finite trace semantics for LTL. A common approach 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.
Andreas Bauer 0002, Patrik Haslum
Added 10 Feb 2011
Updated 10 Feb 2011
Type Journal
Year 2010
Where ECAI
Authors Andreas Bauer 0002, Patrik Haslum
Comments (0)