# 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 [itex]p_1, p_2, ...[itex], the usual logic connectives [itex]\neg,\or,\and,\rightarrow[itex] 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 [itex]\phi[itex] [itex]\circ \phi[itex] Next: [itex]\phi[itex] 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 [itex]\phi[itex] [itex]\Box \phi[itex] Globally: [itex]\phi[itex] 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 [itex]\phi[itex] [itex]\Diamond \phi[itex] Finally: [itex]\phi[itex] 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:
[itex]\phi[itex] U [itex]\psi[itex] [itex]\phi ~\mathcal{U}~ \psi[itex] Until: [itex]\phi[itex] has to hold until at some position [itex]\psi[itex] holds. At that position [itex]\phi[itex] 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>

[itex]\phi[itex] R [itex]\psi[itex] [itex]\phi ~\mathcal{R}~ \psi[itex] Release: [itex]\phi[itex] releases [itex]\psi[itex] if [itex]\psi[itex] ever stops to hold. I.e. either [itex]\phi[itex] holds after a finite number of steps and on the way to this state, including it, [itex]\psi[itex] holds, or [itex]\psi[itex] 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>

[itex]\or[itex]

<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 [itex]\phi[itex] = true U [itex]\phi[itex]
• G [itex]\phi[itex] = [itex]\neg[itex] F [itex]\neg[itex][itex]\phi[itex]
• [itex]\phi[itex]R[itex]\psi[itex] = [itex]\neg[itex]([itex]\neg[itex][itex]\phi[itex]U[itex]\neg[itex][itex]\psi[itex])

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.

• Art and Cultures
• Countries of the World (http://www.academickids.com/encyclopedia/index.php/Countries)
• Space and Astronomy