Editing Linear temporal logic (section)

{{Short description|Modal temporal logic with modalities referring to time}}
In [[logic]], '''linear temporal logic''' or '''linear-time temporal logic'''<ref>[https://books.google.com/books?id=eUggAwAAQBAJ&q=%22temporal+logic%22 Logic in Computer Science: Modelling and Reasoning about Systems]: page 175</ref><ref>{{Cite web |url=http://www-step.stanford.edu/tutorial/temporal-logic/temporal-logic.html |title=Linear-time Temporal Logic |access-date=2012-03-19 |archive-url=https://web.archive.org/web/20170430084134/http://www-step.stanford.edu/tutorial/temporal-logic/temporal-logic.html |archive-date=2017-04-30 |url-status=dead }}</ref> ('''LTL''') is a [[modal logic|modal]] [[temporal logic]] with modalities referring to time. In LTL, one can encode [[formula (logic)|formulae]] about the future of [[path (graph theory)|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 [[quantifier (logic)|quantifier]]s. LTL is sometimes called '''propositional temporal logic''' ('''PTL''').<ref name="Gabbay2003">{{cite book|author1=Dov M. Gabbay|author2= A. Kurucz|author3= F. Wolter|author4= M. Zakharyaschev|title=Many-dimensional modal logics: theory and applications|url=https://books.google.com/books?id=P8jZwiExZYEC&pg=PA46|year=2003|publisher=Elsevier|isbn=978-0-444-50826-3|page=46|author1-link= Dov M. Gabbay}}</ref>
In terms of [[expressive power (computer science)|expressive power]], LTL is a fragment of [[first-order logic]].<ref>{{Cite web|url=http://www.lsv.fr/~gastin/Verif/DiekertGastin-FO-07.pdf|title=First-order Definable Languages|last=Diekert|first=Volker|location=University of Stuttgart}}</ref><ref>{{cite thesis |type=PhD |last=Kamp |first=Hans |authorlink = Hans Kamp|date=1968 |title=Tense Logic and the Theory of Linear Order |publisher=University of California Los Angeles}}</ref>

LTL was first proposed for the [[formal verification]] of computer programs by [[Amir Pnueli]] in 1977.<ref>[[Amir Pnueli]], The temporal logic of programs. ''Proceedings of the 18th Annual [[Symposium on Foundations of Computer Science]] (FOCS)'', 1977, 46–57. {{doi|10.1109/SFCS.1977.32}}</ref>