Search engine for discovering works of Art, research articles, and books related to Art and Culture
Javascript must be enabled to continue!
LTL Goal Specifications Revisited
View through CrossRef
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.
Title: LTL Goal Specifications Revisited
Description:
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.
Related Results
A metamodel for design review derived from design specification templates
A metamodel for design review derived from design specification templates
In order to improve the quality of software, we review specifications refined from the specifications of the previous design process. Nevertheless, errors and defects of specificat...
Teaching technical specifications in fashion design education
Teaching technical specifications in fashion design education
Technical specifications of the fashion designs should be made into written form to produce a clothing collection. Thus, the designer visualizes his/her idea using technical drawin...
Converging from branching to linear metrics on Markov chains
Converging from branching to linear metrics on Markov chains
We study two well-known linear-time metrics on Markov chains (MCs), namely, the strong and strutter trace distances. Our interest in these metrics is motivated by their relation to...
Non-Martial and Martial Methods to an Ultimate Political Goal of the Tiger Movement in Sri Lanka
Non-Martial and Martial Methods to an Ultimate Political Goal of the Tiger Movement in Sri Lanka
The Tiger Movement had one ultimate political goal, and two main alternating methods to reach this goal, which was to obtain recognition by world community for the right of self-de...
Gödel logics and the fully boxed fragment of LTL
Gödel logics and the fully boxed fragment of LTL
In this paper we show that a very basic fragment of FO-LTL, the monadic fully boxed fragment (all connectives and quantifiers are guarded by P) is not recursively enumerable wrt va...