Linear temporal logic
Linear temporal logic (LTL or linear temporal logic) is a model of temporal logic with temporal modalities. In LTL formulas about the future of paths can be established, for example, that a condition will eventually be true or a condition remains true until another condition is met.
Syntax
LTL is built up from a set of propositional variables, the logical links and the subsequent temporal modal operators:
- X for successor (N is used synonymously )
- G for global
- F for sometime ( finally)
- U up ( until)
- R for resolution (release).
The first three operators are unary, so that X is a syntactically correct formula if it is syntactically correct. The last two operators are binary, so that U is a syntactically correct formula if and syntactically correct formulas.
Semantics
An LTL formula can be evaluated both on an infinite sequence of statements as well as a single position on the path. An LTL formula is exactly fulfilled on a path, if it is satisfied at position 0 of the path. The semantics of the modal operators is as follows.
Already two of the operators are fundamental, that is, they define the other by appropriate links:
- F = true U
- G = false R = F
- R = ( U)
Special links
Some authors define a weak to operator ( until weak, W hereinafter), which has similar semantics as to the operator, however, does not stop condition is required. Sometimes it is useful if U and R can be defined with formulas of the weak until operator:
- U = F ( W)
- R = W ()
- W = R ( )
- W = ( U) G
Key Features
There are two properties of the linear temporal logic can be attributed to: security (safety ), indicates that something undesirable will never occur (G) and vitality ( liveness ), which says that something always happens Desired (GF or GF). General: Safety is a property for which a counterexample has a finite prefix, even if the path to be examined is infinite. For the vibrancy in turn, each finite prefix of a counter-example which satisfies the formula, be extended to an infinite path.
Equivalence transformations
The following equivalence transformations are possible:
Relationships to other logics
Linear temporal logic (LTL) is a subset of the Computation Tree Logic * (CTL *), has a common subset of CTL, however, is neither upper nor subset of CTL.
LTL is equivalent to the predicate logic with single-digit relation symbols and the smaller ratio, as well as a star - free regular expressions.
Automata theoretic linear temporal logic model checking
One important way of model checking is the desired properties ( as described above ) express with LTL operators and then to check whether the model satisfies these properties.
Furthermore, it is possible to create a model for "equivalent " Büchi automata and one which is the negation of the property to be tested are equivalent. The intersection of the two non - deterministic Büchi automaton is empty if the model satisfies the properties.