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:
“What’s this, Aurora Leigh,
You write so of the poets and not laugh?
Those virtuous liars, dreamers after dark,
Exaggerators of the sun and moon,
And soothsayers in a tea-cup? I write so
Of the only truth-tellers, now left to God,—
The only speakers of essential truth,
Opposed to relative, comparative,
And temporal truths;...
The only teachers who instruct mankind,
From just a shadow on a charnel-wall.”
—Elizabeth Barrett Browning (1806–1861)
“Neither Aristotelian nor Russellian rules give the exact logic of any expression of ordinary language; for ordinary language has no exact logic.”
—Sir Peter Frederick Strawson (b. 1919)