|
Linear temporal logic - Definition and Overview |
|
|
|
|
Linear temporal logic (LTL) is a field of mathematical logic that is able to talk about the future of paths. LTL is build up from proposition variables <math>p_1, p_2, ...<math>, the usual logic connectives <math>\neg,\or,\and,\rightarrow<math> and the following temporal operators. LTL formulas are generally evaluated over paths and a position on that path. A LTL formula as such is satisfied if and only if it is satisfied for position 0 on that path.
| Textual
| Symbolic
| Explanation
|
| Unary operators:
|
| N <math>\phi<math>
| <math>\circ \phi<math>
| Next: <math>\phi<math> has to hold at the next state.
|
| G <math>\phi<math>
| <math>\Box \phi<math>
| Globally: <math>\phi<math> has to hold on the entire subsequent path.
|
| F <math>\phi<math>
| <math>\Diamond \phi<math>
| Finally: <math>\phi<math> eventually has to hold (somewhere on the subsequent path).
|
| Binary operator:
|
| <math>\phi<math> U <math>\psi<math>
| <math>\phi ~\mathcal{U}~ \psi<math>
| Until: <math>\phi<math> has to hold until at some position <math>\psi<math> holds. At that position <math>\phi<math> does not have to hold any more.
|
However one can reduce to two of those operators since the following is always satisfied:
- F <math>\phi<math> = true U <math>\phi<math>
- G <math>\phi<math> = <math>\neg<math> F <math>\neg<math><math>\phi<math>
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.
|
|
|
