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. Subsequently LTL is sometimes called propositional temporal logic, abbreviated PTL.Linear temporal logic (LTL) is a fragment of first-order 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. Subsequently LTL is sometimes called propositional temporal logic, abbreviated PTL.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: 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 to write LTL formulas succinctly.The additional logical operators are ∧, →, ↔, true, and false.Following are the additional temporal operators. 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 = 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 ⊨ {displaystyle vDash } between a word and an LTL formula is defined as follows: We say an ω-word w satisfies an LTL formula ψ when w ⊨ {displaystyle vDash } ψ. The ω-language L(ψ) defined by ψ is {w | w ⊨ {displaystyle vDash } ψ}, which is the set of ω-words that satisfy ψ.A formula ψ is satisfiable if there exist an ω-word w such that w ⊨ {displaystyle vDash } ψ. A formula ψ is valid if for each ω-word w over alphabet 2AP, w ⊨ {displaystyle vDash } ψ.