Editing Linear temporal logic (section)

=== Weak until and strong release ===

Some authors also define a ''weak until'' binary operator, denoted '''W''', with semantics similar to that of the until operator but the stop condition is not required to occur (similar to release).<ref>Sec. 5.1.5 "Weak Until, Release, and Positive Normal Form" of Principles of Model Checking.</ref> It is sometimes useful since both '''U''' and '''R''' can be defined in terms of the weak until:
* {{math|''ψ'' '''W''' ''φ'' ≡ (''ψ'' '''U''' ''φ'') ∨ '''G''' ''ψ'' ≡ ''ψ'' '''U''' (''φ'' ∨ '''G''' ''ψ'') ≡  ''φ'' '''R''' (''φ'' ∨ ''ψ'')}}
* {{math|''ψ'' '''U''' ''φ'' ≡ '''F'''''φ''  ∧ (''ψ'' '''W''' ''φ'')}}
* {{math|''ψ'' '''R''' ''φ'' ≡ ''φ'' '''W''' (''φ'' ∧ ''ψ'')}}

The ''strong release'' binary operator, denoted '''M''', is the dual of weak until. It is defined similar to the until operator, so that the release condition has to hold at some point. Therefore, it is stronger than the release operator.
* {{math|''ψ'' '''M''' ''φ'' ≡ ¬(¬''ψ'' '''W''' ¬''φ'') ≡ (''ψ'' '''R''' ''φ'') ∧ '''F''' ''ψ'' ≡ ''ψ'' '''R''' (''φ'' ∧ '''F''' ''ψ'') ≡ ''φ'' '''U''' (''ψ'' ∧ ''φ'')}}

The semantics for the temporal operators are pictorially presented as follows.

{| class="wikitable"
|-
!Textual
!Symbolic
!Explanation
!Diagram
|-
| colspan="4" | [[Unary operation|Unary operators]]:
|-
|'''X''' ''φ''
|<math>\bigcirc \varphi</math>
|ne'''X'''t: ''φ'' has to hold at the next state.
|[[File:Ltlnext.svg|LTL next operator]]
|-
|'''F''' ''φ''
|<math>\Diamond \varphi</math>
|'''F'''inally: ''φ'' eventually has to hold (somewhere on the subsequent path).
|[[File:Ltleventually.svg|LTL eventually operator]]
|-
|'''G''' ''φ''
|<math>\Box \varphi</math>
|'''G'''lobally: ''φ'' has to hold on the entire subsequent path.
|[[File:Ltlalways.svg|LTL always operator]]
|-
| colspan="4" | [[Binary operator]]s:
|-
|''ψ'' '''U''' ''φ''
|<math>\psi\;\mathcal{U}\,\varphi</math>
|'''U'''ntil: ''ψ'' has to hold ''at least'' until ''φ'' becomes true, which must hold at the current or a future position.
|[[File:Ltluntil.svg|LTL until operator]]
|-
|''ψ'' '''R''' ''φ''
|<math>\psi\;\mathcal{R}\,\varphi</math>
|'''R'''elease: ''φ'' has to be true until and including the point where ''ψ'' first becomes true; if ''ψ'' never becomes true, ''φ'' must remain true forever.
|[[File:Ltlrelease-stop.svg|LTL release operator (which stops)]]<br>
[[File:Ltlrelease-nostop.svg|LTL release operator (which does not stop)]]
|-
|''ψ'' '''W''' ''φ''
|<math>\psi\;\mathcal{W}\,\varphi</math>
|'''W'''eak until: ''ψ'' has to hold ''at least'' until ''φ''; if ''φ'' never becomes true, ''ψ'' must remain true forever.
|[[File:Ltluntil.svg|LTL weak until operator (which stops)]]<br>
[[File:Ltlweakuntil2.svg|LTL weak until operator (which does not stop)]]
|- 
|''ψ'' '''M''' ''φ''
|<math>\psi\;\mathcal{M}\,\varphi</math>
|Strong release: ''φ'' has to be true until and including the point where ''ψ'' first becomes true, which must hold at the current or a future position.
|[[File:Ltlrelease-stop.svg|LTL strong release operator]]
|}