Equivalences
Let Φ, ψ, and ρ be LTL formulas. The following tables list some of the useful equivalences which extend standard equivalences among the usual logical operators.
| Distributivity | ||
|---|---|---|
| X (Φ ∨ ψ) ≡ (X Φ) ∨ (X ψ) | X (Φ ∧ ψ)≡ (X Φ) ∧ (X ψ) | X (Φ U ψ)≡ (X Φ) U (X ψ) |
| F (Φ ∨ ψ) ≡ (F Φ) ∨ (F ψ) | G (Φ ∧ ψ)≡ (G Φ) ∧ (G ψ) | |
| ρ U (Φ ∨ ψ) ≡ (ρ U Φ) ∨ (ρ U ψ) | (Φ ∧ ψ) U ρ ≡ (Φ U ρ) ∧ (ψ U ρ) | |
| Negation propagation | ||
|---|---|---|
| ¬X Φ ≡ X ¬Φ | ¬G Φ ≡ F ¬Φ | ¬F Φ ≡ G ¬Φ |
| ¬ (Φ U ψ) ≡ (¬Φ R ¬ψ) | ¬ (Φ R ψ) ≡ (¬Φ U ¬ψ) | |
| 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 Φ) | |
Read more about this topic: Linear Temporal Logic