Editing Temporal logic (section)

==Temporal operators==
Temporal logic has two kinds of operators: [[logical operator]]s and modal operators.<ref>{{cite web |url=http://plato.stanford.edu/entries/logic-temporal/ |title=Temporal Logic |date=February 7, 2020 |website=Stanford Encyclopedia of Philosophy |access-date=April 19, 2022}}</ref> Logical operators are usual truth-functional operators (<math>\neg,\lor,\land,\rightarrow</math>). The modal operators used in linear temporal logic and computation tree logic are defined as follows.

{| class="wikitable"
|-
! Textual
! Symbolic
! Definition
! Explanation
! Diagram
|-
! colspan="4" | [[Binary operator]]s
|-
|{{mvar|&phi;}} '''U''' {{mvar|&psi;}}
|<math>\phi ~\mathcal{U}~ \psi</math>
|<math>(B\,\mathcal{U}\,C)(\phi)= \ (\exists i:C(\phi_i)\land(\forall j<i:B(\phi_j)))</math>
|'''U'''ntil: {{mvar|&psi;}} holds at the current or a future position, and {{mvar|&phi;}} has to hold until that position. At that position {{mvar|&phi;}} 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>
|-
|{{mvar|&phi;}} '''R''' {{mvar|&psi;}}
|<math>\phi ~\mathcal{R}~ \psi</math>
|<math>(B\,\mathcal{R}\,C)(\phi)= \ (\forall i:C(\phi_i)\lor(\exists j<i:B(\phi_j)))</math>
|'''R'''elease: {{mvar|&phi;}} releases {{mvar|&psi;}} if {{mvar|&psi;}} is true up until and including the first position in which {{mvar|&phi;}} 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:8
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
 from:6 till:8

 bar:q color:red width:10 align:left fontsize:S
 from:1 till:3
 from:5 till:6
 from:7 till:8

 bar:pRq color:red width:10 align:left fontsize:S
 from:1 till:3
 from:7 till:8
</timeline>
|-
! colspan="4" | [[Unary operator]]s
|-
|'''N''' {{mvar|&phi;}}
|<math>\bigcirc \phi</math>
|<math>\mathcal{N}B(\phi_i)=B(\phi_{i+1})</math>
|'''N'''ext: {{mvar|&phi;}} 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>
|-
|'''F''' {{mvar|&phi;}}
|<math>\Diamond \phi</math>
|<math>\mathcal{F}B(\phi)=(true\,\mathcal{U}\,B)(\phi)</math>
|'''F'''uture: {{mvar|&phi;}} 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>
|-
|'''G''' {{mvar|&phi;}}
|<math>\Box \phi</math>
|<math>\mathcal{G}B(\phi)=\neg\mathcal{F}\neg B(\phi)</math>
|'''G'''lobally: {{mvar|&phi;}} 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>
|-
|'''A''' {{mvar|&phi;}}
|<math>\forall \phi</math>
|<math>(\mathcal{A}B)(\psi)= \ (\forall \phi:\phi_0=\psi\to B(\phi))</math>
|'''A'''ll: {{mvar|&phi;}} has to hold on all paths starting from the current state.
|
|-
|'''E''' {{mvar|&phi;}}
|<math>\exists \phi</math>
|<math>(\mathcal{E}B)(\psi)= \ (\exists \phi:\phi_0=\psi\land B(\phi))</math>
|'''E'''xists: there exists at least one path starting from the current state where {{mvar|&phi;}} holds.
|
|}

Alternate symbols:

* operator '''R''' is sometimes denoted by '''V'''
* The operator '''W''' is the ''weak until'' operator: <math>f \mathbf W g</math> is equivalent to <math>f \mathbf U g \lor \mathbf G f</math>

Unary operators are [[well-formed formula]]s whenever {{math|B({{var|&phi;}})}} is well-formed. Binary operators are well-formed formulas whenever {{math|B({{var|&phi;}})}} and {{math|C({{var|&phi;}})}} are well-formed.

In some logics, some operators cannot be expressed. For example, '''N''' operator cannot be expressed in [[temporal logic of actions]].