Linear temporal logic

In logic, linear temporal logic or linear-time temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will be true until another fact becomes true, etc. It is a fragment of the more complex CTL*, which additionally allows branching time and quantifiers. LTL is sometimes called propositional temporal logic, abbreviated PTL. In terms of expressive power, linear temporal logic (LTL) is a fragment of first-order logic. LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977. LTL is built up from a finite set of propositional variables AP, the logical operators ¬ and ∨, and the temporal modal operators X (some literature uses O or N) and U. Formally, the set of LTL formulas over AP is inductively defined as follows: if p ∈ AP then p is an LTL formula; if ψ and φ are LTL formulas then ¬ψ, φ ∨ ψ, X ψ, and φ U ψ are LTL formulas. X is read as next and U is read as until. Other than these fundamental operators, there are additional logical and temporal operators defined in terms of the fundamental operators, in order to write LTL formulas succinctly. The additional logical operators are ∧, →, ↔, true, and false. Following are the additional temporal operators. G for always (globally) F for finally R for release W for weak until M for mighty release An LTL formula can be satisfied by an infinite sequence of truth valuations 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 = a0,a1,a2,... be such an ω-word. Let w(i) = ai. Let wi = ai,ai+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 an LTL formula when w ⊨ .