sociology - 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 $p 1, p 2,...$ , the usual logic connectives $\neg,\or,\and,\rightarrow$ 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 $φ$	$\circ \phi$	Next: $φ$ 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 $φ$	$\Box \phi$	Globally: $φ$ 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 $φ$	$\Diamond \phi$	Finally: $φ$ 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:
$φ$ U $ψ$	$\phi ~\mathcal{U}~ \psi$	Until: $φ$ has to hold until at some position $ψ$ holds. At that position $φ$ 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>
$φ$ R $ψ$	$\phi ~\mathcal{R}~ \psi$	Release: $φ$ releases $ψ$ if $ψ$ ever stops to hold. I.e. either $φ$ holds after a finite number of steps and on the way to this state, including it, $ψ$ holds, or $ψ$ 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> $\or$ <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 $φ$ = true U $φ$
G $φ$ = $\neg$ F $\neg$ $φ$
$φ$ R $ψ$ = $\neg$ ( $\neg$ $φ$ U $\neg$ $ψ$ )

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.

Linear temporal logic

See also