Linear Temporal Logic - Semantics

Semantics

An LTL formula can be satisfied by an infinite sequence of truth evaluations of variables in AP. These sequences can be viewed as a word on a path of a Kripke structure (an ω-word over alphabet 2AP). Let w = a₀,a₁,a₂,... be such an ω-word. Let w(i) = a_i. Let wi = a_i,a_i+1,..., which is a suffix of w. Formally, the satisfaction relation between a word and an LTL formula is defined as follows:

• w p if p ∈ w(0)
• w ¬ψ if w ψ
• w φ ∨ ψ if w φ or w ψ
• w X ψ if w1 ψ (in the next time step ψ must be true)
• w φ U ψ if there exists i ≥ 0 such that wi ψ and for all 0 ≤ k < i, wk φ (φ must remain true until ψ becomes true)

We say an ω-word w satisfies LTL formula ψ when w ψ. The ω-language L(ψ) defined by ψ is {w | w ψ}, which is the set of ω-words that satisfy ψ. A formula ψ is satisfiable if there exist a ω-word w such that w ψ. A formula ψ is valid if for each ω-word w over alphabet 2AP, w ψ.

The additional logical operators are defined as follows:

• φ ∧ ψ ≡ ¬(¬φ ∨ ¬ψ)
• φ → ψ ≡ ¬φ ∨ ψ
• φ ↔ ψ ≡ (φ → ψ) ∧ ( ψ → φ)
• true ≡ p ∨ ¬p, where p ∈ AP
• false ≡ ¬true

The additional temporal operators R, F, and G are defined as follows:

• φ R ψ ≡ ¬(¬φ U ¬ψ) ( ψ remains true until once φ becomes true. φ may never become true)
• F ψ ≡ true U ψ (eventually ψ becomes true)
• G ψ ≡ false R ψ ≡ ¬F ¬ψ (ψ always remains true)

Weak until

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). It is sometimes useful since both U and R can be defined in terms of the weak until:

• φ W ψ ≡ (φ U ψ) ∨ G φ ≡ φ U (ψ ∨ G φ) ≡ ψ R (ψ ∨ φ)
• φ U ψ ≡ Fψ ∧ (φ W ψ)
• φ R ψ ≡ ψ W (ψ ∧ φ)

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

†The symbols are used in the literature to denote these operators.