Linear temporal logic

From Free net encyclopedia

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

1 Syntax
2 Semantics
3 Relations with other logics
4 See also
5 External link

[edit]

Syntax

LTL is built up from a set of proposition variables <math>p_1, p_2, ...</math>, the usual logic connectives <math>\neg,\or,\and,\rightarrow</math> and the following temporal modal operators:

N for next;
G for always;
F for eventually;
U for until;
R for release.

The first three operators are unary, so that N <math>\phi</math> is a well-formed formula whenever <math>\phi</math> is a well-formed formula. The last two operators are binary, so that <math>\phi</math> U <math>\psi</math> is a well-formed formula whenever <math>\phi</math> and <math>\psi</math> are well-formed formulas.

[edit]

Semantics

An LTL formula can be evaluated over a 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.

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:30 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:2 till:3 from:5 till:6 bar:Np color:red width:10 align:left fontsize:S from:1 till:2 from:4 till:5 </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:30 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:1 till:3 from:4 till:6 bar:Gp color:red width:10 align:left fontsize:S from:4 till:6 </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:30 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:2 till:3 from:4 till:5 bar:Fp color:red width:10 align:left fontsize:S from:0 till:5 </timeline>
Binary operators:
<math>\phi</math> U <math>\psi</math>	<math>\phi ~\mathcal{U}~ \psi</math>	Until: <math>\psi</math> holds at the current or a future position, and <math>\phi</math> has to hold until that position. At that position <math>\phi</math> does not have to hold any more.	<timeline> ImageSize = width:240 height:94 PlotArea = left:30 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:1 till:3 bar:q color:red width:10 align:left fontsize:S from:3 till:5 bar:pUq color:red width:10 align:left fontsize:S from:1 till:5 </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> is true until the first position in which <math>\phi</math> is true (or forever if such a position does not exist).	<timeline> ImageSize = width:240 height:100 PlotArea = left:30 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:2 till:4 bar:q color:red width:10 align:left fontsize:S from:1 till:3 from:5 till:6 bar:pRq color:red width:10 align:left fontsize:S from:1 till:3 from:5 till:6 </timeline>

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.

[edit]