What is Linear temporal logic?

In logic, linear temporal logic or linear-time temporal logic 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.In terms of expressive power, linear temporal logic is a fragment of first-order logic.

LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977.