Linear temporal logic

From Academic Kids

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.

See also

Navigation

Academic Kids Menu

  • Art and Cultures
    • Art (http://www.academickids.com/encyclopedia/index.php/Art)
    • Architecture (http://www.academickids.com/encyclopedia/index.php/Architecture)
    • Cultures (http://www.academickids.com/encyclopedia/index.php/Cultures)
    • Music (http://www.academickids.com/encyclopedia/index.php/Music)
    • Musical Instruments (http://academickids.com/encyclopedia/index.php/List_of_musical_instruments)
  • Biographies (http://www.academickids.com/encyclopedia/index.php/Biographies)
  • Clipart (http://www.academickids.com/encyclopedia/index.php/Clipart)
  • Geography (http://www.academickids.com/encyclopedia/index.php/Geography)
    • Countries of the World (http://www.academickids.com/encyclopedia/index.php/Countries)
    • Maps (http://www.academickids.com/encyclopedia/index.php/Maps)
    • Flags (http://www.academickids.com/encyclopedia/index.php/Flags)
    • Continents (http://www.academickids.com/encyclopedia/index.php/Continents)
  • History (http://www.academickids.com/encyclopedia/index.php/History)
    • Ancient Civilizations (http://www.academickids.com/encyclopedia/index.php/Ancient_Civilizations)
    • Industrial Revolution (http://www.academickids.com/encyclopedia/index.php/Industrial_Revolution)
    • Middle Ages (http://www.academickids.com/encyclopedia/index.php/Middle_Ages)
    • Prehistory (http://www.academickids.com/encyclopedia/index.php/Prehistory)
    • Renaissance (http://www.academickids.com/encyclopedia/index.php/Renaissance)
    • Timelines (http://www.academickids.com/encyclopedia/index.php/Timelines)
    • United States (http://www.academickids.com/encyclopedia/index.php/United_States)
    • Wars (http://www.academickids.com/encyclopedia/index.php/Wars)
    • World History (http://www.academickids.com/encyclopedia/index.php/History_of_the_world)
  • Human Body (http://www.academickids.com/encyclopedia/index.php/Human_Body)
  • Mathematics (http://www.academickids.com/encyclopedia/index.php/Mathematics)
  • Reference (http://www.academickids.com/encyclopedia/index.php/Reference)
  • Science (http://www.academickids.com/encyclopedia/index.php/Science)
    • Animals (http://www.academickids.com/encyclopedia/index.php/Animals)
    • Aviation (http://www.academickids.com/encyclopedia/index.php/Aviation)
    • Dinosaurs (http://www.academickids.com/encyclopedia/index.php/Dinosaurs)
    • Earth (http://www.academickids.com/encyclopedia/index.php/Earth)
    • Inventions (http://www.academickids.com/encyclopedia/index.php/Inventions)
    • Physical Science (http://www.academickids.com/encyclopedia/index.php/Physical_Science)
    • Plants (http://www.academickids.com/encyclopedia/index.php/Plants)
    • Scientists (http://www.academickids.com/encyclopedia/index.php/Scientists)
  • Social Studies (http://www.academickids.com/encyclopedia/index.php/Social_Studies)
    • Anthropology (http://www.academickids.com/encyclopedia/index.php/Anthropology)
    • Economics (http://www.academickids.com/encyclopedia/index.php/Economics)
    • Government (http://www.academickids.com/encyclopedia/index.php/Government)
    • Religion (http://www.academickids.com/encyclopedia/index.php/Religion)
    • Holidays (http://www.academickids.com/encyclopedia/index.php/Holidays)
  • Space and Astronomy
    • Solar System (http://www.academickids.com/encyclopedia/index.php/Solar_System)
    • Planets (http://www.academickids.com/encyclopedia/index.php/Planets)
  • Sports (http://www.academickids.com/encyclopedia/index.php/Sports)
  • Timelines (http://www.academickids.com/encyclopedia/index.php/Timelines)
  • Weather (http://www.academickids.com/encyclopedia/index.php/Weather)
  • US States (http://www.academickids.com/encyclopedia/index.php/US_States)

Information

  • Home Page (http://academickids.com/encyclopedia/index.php)
  • Contact Us (http://www.academickids.com/encyclopedia/index.php/Contactus)

  • Clip Art (http://classroomclipart.com)
Toolbox
Personal tools