Editing Linear temporal logic (section)

==Equivalences==
Let φ, ψ, and ρ be LTL formulas. The following tables list some of the useful equivalences that extend standard equivalences among the usual logical operators.

{| class="wikitable"
|-
! colspan="3" | Distributivity 
|-
| '''X''' (φ ∨ ψ) ≡  ('''X''' φ) ∨ ('''X''' ψ)|| '''X''' (φ ∧ ψ) ≡  ('''X''' φ) ∧ ('''X''' ψ)  || '''X''' (φ '''U''' ψ)≡  ('''X''' φ) '''U''' ('''X''' ψ)
|-
| '''F''' (φ ∨ ψ) ≡  ('''F''' φ) ∨ ('''F''' ψ)|| '''G''' (φ ∧ ψ) ≡  ('''G''' φ) ∧ ('''G''' ψ)  || 
|-
| ρ '''U''' (φ ∨ ψ) ≡  (ρ '''U''' φ) ∨ (ρ '''U''' ψ)|| (φ ∧ ψ) '''U''' ρ ≡  (φ '''U''' ρ) ∧ (ψ '''U''' ρ)  || 
|}

{| class="wikitable"
|-
! colspan="4" | Negation propagation
|-
| '''''X''' is self-dual'' || '''''F''' and '''G''' are dual'' || '''''U''' and '''R''' are dual''  || '''''W''' and '''M''' are dual''
|-
| ¬'''X''' φ ≡ '''X''' ¬φ  || ¬'''F''' φ ≡ '''G''' ¬φ          || ¬ (φ '''U''' ψ) ≡ (¬φ '''R''' ¬ψ) || ¬ (φ '''W''' ψ) ≡ (¬φ '''M''' ¬ψ)
|-
|                          || ¬'''G''' φ ≡ '''F''' ¬φ          || ¬ (φ '''R''' ψ) ≡ (¬φ '''U''' ¬ψ) || ¬ (φ '''M''' ψ) ≡ (¬φ '''W''' ¬ψ)
|}
 
{| class="wikitable"
|-
! colspan="3" | Special temporal properties
|-
| '''F''' φ ≡ '''F''' '''F''' φ || '''G''' φ ≡ '''G''' '''G''' φ || φ '''U''' ψ ≡  φ '''U''' (φ '''U''' ψ)
|-
| φ '''U''' ψ ≡  ψ ∨ ( φ ∧ '''X'''(φ '''U''' ψ) ) || φ '''W''' ψ ≡  ψ ∨ ( φ ∧ '''X'''(φ '''W''' ψ) ) || φ '''R''' ψ ≡ ψ ∧ (φ ∨ '''X'''(φ '''R''' ψ) )
|-
| '''G''' φ ≡ φ ∧ '''X'''('''G''' φ) ||'''F''' φ ≡ φ ∨ '''X'''('''F''' φ) || 
|}