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.

514061
de