CTL*, which additionally allows branching time and quantifiers. LTL is sometimes called propositional temporal logic (PTL).In terms of expressive power, LTL is a fragment of first-order logic.

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