LINEAR TEMPORAL LOGIC

'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 eventually be true, that a condition will be true until another fact becomes true, etc.

Contents

Syntax

Semantics

Nonstandard connectives

Important properties

Relations with other logics

Automata theoretic Linear temporal logic model checking

See also

External links

Syntax

LTL is built up from a set of proposition variables $p\_1,\; p\_2,\; ...$, the usual logic connectives $$
eg,or,nd,
ightarrow and the following temporal modal operators:

★ 'X' for next;

★ 'G' for always ('g'lobally);

★ 'F' for eventually (in the 'f'uture);

★ 'U' for until;

★ 'R' for release.
The first three operators are unary, so that 'X' $phi$ is a well-formed formula whenever $phi$ is a well-formed formula. The last two operators are binary, so that $phi$ 'U' $psi$ is a well-formed formula whenever $phi$ and $psi$ are well-formed formulas.

Semantics

An LTL formula can be evaluated over an infinite 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.
{| border="1" align="center"
|-
!Textual
!Symbolic
!Explanation
!Diagram
|-
| colspan="4" | Unary operators:
|-
|'X' $phi$
|$circ\; phi$
|ne'X't: $phi$ has to hold at the next state. ('N' is used synonymously.)
|
|-
|'G' $phi$
|$Box\; phi$
|'G'lobally: $phi$ has to hold on the entire subsequent path.
|
|-
|'F' $phi$
|$Diamond\; phi$
|'F'inally: $phi$ eventually has to hold (somewhere on the subsequent path).
|
|-
| colspan="4" | Binary operators:
|-
|$psi$ 'U' $phi$
|$psimathcal\{U\}phi$
|'U'ntil: $phi$ holds at the current or a future position, and $psi$ has to hold until that position. At that position $psi$ does not have to hold any more.
|
|-
|$psi$ 'R' $phi$
|$psimathcal\{R\}phi$
|'R'elease: $psi$ releases $phi$ if $phi$ is true until the first position in which $psi$ 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' $phi$ = 'true' 'U' $phi$

★ 'G' $phi$ = 'false' 'R' $phi$ = $$
eg 'F' $$
eg$phi$

★ $psi$ 'R' $phi$ = $$
eg($$
eg$psi$ 'U' $$
eg$phi$)

Nonstandard connectives

Some authors also define a ''weak until'' binary operator, denoted 'W', with semantics similar to that of the until operator but the stop condition is not required to occur (similar to release). It is sometimes useful since both 'U' and 'R' can be defined in terms of the weak until:

★ $psi$ 'U' $phi$ = 'F' $phi$$land$($psi$ 'W' $phi$)

★ $psi$ 'R' $phi$ = $phi$ 'W' ($psi$$land$$phi$)

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'$$
eg$phi$), while 'liveness' properties state that ''something good keeps happening'' ('GF'$psi$ or 'G'$(phi$
ightarrow'F'$psi)$). More generally: Safety properties are those for which every counterexample has a finite prefix such 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.

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.

Automata theoretic Linear temporal logic model checking

An important way to model check is to express desired properties (such as the ones described above) using LTL operators and actually check if the model satisfies this property. One technique is to obtain a Büchi automaton that is "equivalent" to the model and one that is "equivalent" to the property. Obtain a synchronized product of the two non-deterministic Büchi automata and then do an emptiness check of this product. Another possibility is to develop the negated version of the same property and make sure that the product is not empty.

See also

★ Temporal logic in finite-state verification

★ Computational tree logic (CTL)

★ Interval temporal logic (ITL)

★ Büchi automaton

External links

★ A presentation of LTL

★ Linear-Time Temporal Logic and Büchi Automata