Linear temporal logic
|
|
Linear temporal logic (LTL) is a field of mathematical logic that is able to talk about the future of paths (LTL is a temporal logic). LTL is built 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 | Diagram |
|---|---|---|---|
| Unary operators: | |||
| N <math>\phi<math> | <math>\circ \phi<math> | Next: <math>\phi<math> has to hold at the next state. (X is used synonymously.) | <timeline>
ImageSize = width:240 height:60 PlotArea = left:20 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:0 till:6 bar:-p color:red width:10 align:left fontsize:S from:0 till:1 from:2 till:6 </timeline> |
| G <math>\phi<math> | <math>\Box \phi<math> | Globally: <math>\phi<math> has to hold on the entire subsequent path. | <timeline>
ImageSize = width:240 height:60 PlotArea = left:20 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:0 till:6 bar:-p color:red width:10 align:left fontsize:S </timeline> |
| F <math>\phi<math> | <math>\Diamond \phi<math> | Finally: <math>\phi<math> eventually has to hold (somewhere on the subsequent path). | <timeline>
ImageSize = width:240 height:60 PlotArea = left:20 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:0 till:6 bar:-p color:red width:10 align:left fontsize:S from:0 till:3 from:4 till:6 </timeline> |
| Binary operators: | |||
| <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. | <timeline>
ImageSize = width:240 height:100 PlotArea = left:20 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:0 till:6 bar:-p color:red width:10 align:left fontsize:S from:3 till:6 bar:q color:red width:10 align:left fontsize:S from:0 till:6 bar:-q color:red width:10 align:left fontsize:S from:0 till:3 from:4 till:6 </timeline> |
| <math>\phi<math> R <math>\psi<math> | <math>\phi ~\mathcal{R}~ \psi<math> | Release: <math>\phi<math> releases <math>\psi<math> if <math>\psi<math> ever stops to hold. I.e. either <math>\phi<math> holds after a finite number of steps and on the way to this state, including it, <math>\psi<math> holds, or <math>\psi<math> holds continuously forever. | <timeline>
ImageSize = width:240 height:100 PlotArea = left:20 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:0 till:6 bar:-p color:red width:10 align:left fontsize:S from:0 till:3 from:4 till:6 bar:q color:red width:10 align:left fontsize:S from:0 till:6 bar:-q color:red width:10 align:left fontsize:S from:4 till:6 </timeline> <math>\or<math>
<timeline> ImageSize = width:240 height:100 PlotArea = left:20 bottom:30 top:0 right:20 DateFormat = x.y Period = from:0 till:6 TimeAxis = orientation:horizontal AlignBars = justify ScaleMajor = gridcolor:black increment:1 start:0 ScaleMinor = gridcolor:black increment:1 start:0 PlotData= bar:p color:red width:10 align:left fontsize:S from:0 till:6 bar:-p color:red width:10 align:left fontsize:S from:0 till:6 bar:q color:red width:10 align:left fontsize:S from:0 till:6 bar:-q color:red width:10 align:left fontsize:S </timeline> |
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>
- <math>\phi<math>R<math>\psi<math> = <math>\neg<math>(<math>\neg<math><math>\phi<math>U<math>\neg<math><math>\psi<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.