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 S1S.
LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977.
Read more about Linear Temporal Logic: Syntax, Semantics, Equivalences, Negation Normal Form, Relations With Other Logics, Applications
Famous quotes containing the words temporal and/or logic:
“Listen to any musical phrase or rhythm, and grasp it as a whole, and you thereupon have present in you the image, so to speak, of the divine knowledge of the temporal order.”
—Josiah Royce (1855–1916)
“The usefulness of madmen is famous: they demonstrate society’s logic flagrantly carried out down to its last scrimshaw scrap.”
—Cynthia Ozick (b. 1928)