Linear temporal logic

From Wikipedia, the free encyclopedia

Linear temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will be eventually be true, that a condition will be true until another fact becomes true, etc.

1 Syntax
2 Semantics
3 Important properties
4 Relations with other logics
5 See also
6 External links

[edit] Syntax

LTL is built up from a set of proposition variables $p 1, p 2,...$ , the usual logic connectives $\neg,\or,\and,\rightarrow$ and the following temporal modal operators:

N for next;
G for always (globally);
F for eventually (in the future);
U for until;
R for release.

The first three operators are unary, so that N $φ$ is a well-formed formula whenever $φ$ is a well-formed formula. The last two operators are binary, so that $φ$ U $ψ$ is a well-formed formula whenever $φ$ and $ψ$ are well-formed formulas.

[edit] Semantics

An LTL formula can be evaluated over a sequence of truth evaluations and a position on that path. An LTL formula is satisfied by a path if and only if it is satisfied for position 0 on that path. The semantics for the modal operators is given as follows.

Textual	Symbolic	Explanation
Unary operators:
N $φ$	$\circ \phi$	Next: $φ$ has to hold at the next state. (X is used synonymously.)
G $φ$	$\Box \phi$	Globally: $φ$ has to hold on the entire subsequent path.
F $φ$	$\Diamond \phi$	Finally: $φ$ eventually has to hold (somewhere on the subsequent path).
Binary operators:
$φ$ U $ψ$	$\phi ~\mathcal{U}~ \psi$	Until: $ψ$ holds at the current or a future position, and $φ$ has to hold until that position. At that position $φ$ does not have to hold any more.
$φ$ R $ψ$	$\phi ~\mathcal{R}~ \psi$	Release: $φ$ releases $ψ$ if $ψ$ is true until the first position in which $φ$ is true (or forever if such a position does not exist).

One can reduce to two of those operators since the following is always satisfied:

F $φ$ = true U $φ$
G $φ$ = false R $φ$ = $\neg$ F $\neg$ $φ$
$φ$ R $ψ$ = $\neg$ ( $\neg$ $φ$ U $\neg$ $ψ$ )

[edit] Important properties

There are two main types of properties that can be expressed using linear temporal logic: Safety properties usually state that something bad never happens (G $\neg$ $φ$ ), while Liveness properties state that something good eventually happens (F $ψ$ ). More generally safety properties are those for which every counterexample has a finite prefix that, however it is extended to an infinite path, it is still a counterexample. For liveness properties, on the other hand, every finite prefix of a counterexample can be extended to an infinite path that satisfies the formula.

[edit] Relations with other logics

Linear temporal logic (LTL) is a subset of CTL*.

LTL can be shown to be equivalent to the first-order logic over one successor and the smaller relation, FO[S,<] as well as star-free regular expressions or deterministic finite automata with loop complexity 0.