TY - GEN
T1 - LTL goal specifications revisited
AU - Bauer, Andreas
AU - Haslum, Patrik
PY - 2010
Y1 - 2010
N2 - 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 se mantics: 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.
AB - 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 se mantics: 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.
UR - http://www.scopus.com/inward/record.url?scp=77956032505&partnerID=8YFLogxK
U2 - 10.3233/978-1-60750-606-5-881
DO - 10.3233/978-1-60750-606-5-881
M3 - Conference contribution
SN - 9781607506058
T3 - Frontiers in Artificial Intelligence and Applications
SP - 881
EP - 886
BT - ECAI 2010
PB - IOS Press
T2 - 2nd Workshop on Knowledge Representation for Health Care, KR4HC 2010, held in conjunction with the 19th European Conference in Artificial Intelligence, ECAI 2010
Y2 - 17 August 2010 through 17 August 2010
ER -