Editing Linear temporal logic

{{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>

==Syntax==
LTL is built up from a finite set of [[propositional variable]]s ''AP'', the [[logical connective|logical operators]] ¬ and ∨, and the [[Temporal logic|temporal]] [[modal operator]]s '''X''' (some literature uses '''O''' or '''N''') and '''U'''. 
Formally, the set of LTL formulas over ''AP'' is inductively defined as follows:
* if {{math|''p'' ∈ ''AP''}} then ''p'' is an LTL formula;
* if {{mvar|ψ}} and {{mvar|φ}} are LTL formulas then {{math|¬{{var|ψ}}, {{var|φ}} ∨ {{var|ψ}}, '''X''' {{var|ψ}}}}, and {{math|{{var|φ}} '''U''' {{var|ψ}}}} are LTL formulas.<ref>Sec. 5.1 of [[Christel Baier]] and [[Joost-Pieter Katoen]], ''[[Principles of Model Checking]]'', MIT Press {{cite web|url=http://mitpress.mit.edu/catalog/item/default.asp?tid%3D11481%26ttype%3D2 |title=Principles of Model Checking - the MIT Press |access-date=2011-05-17 |url-status=dead |archive-url=https://web.archive.org/web/20101204043002/http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 |archive-date=2010-12-04 }}</ref>

'''X''' is read as ne'''x'''t and '''U''' is read as '''u'''ntil.
Other than these fundamental operators, there are additional logical and temporal operators defined in terms of the fundamental operators, in order to write LTL formulas succinctly.
The additional logical operators are ∧, →, ↔, '''true''', and '''false'''.
Following are the additional temporal operators.

* '''G''' for always ('''g'''lobally)
* '''F''' for '''f'''inally
* '''R''' for '''r'''elease
* '''W''' for '''w'''eak until
* '''M''' for '''m'''ighty release

==Semantics==

An LTL formula can be ''[[satisfiability|satisfied]]'' by an infinite sequence of truth valuations of variables in ''AP''.
These sequences can be viewed as a word on a path of a [[Kripke structure]] (an [[ω-language|ω-word]] over [[Alphabet (formal languages)|alphabet]] 2<sup>''AP''</sup>).
Let ''w'' = a<sub>0</sub>,a<sub>1</sub>,a<sub>2</sub>,... be such an ω-word. Let ''w''(''i'') = ''a<sub>i</sub>''. Let ''w''<sup>i</sup> = ''a<sub>i</sub>'',''a''<sub>''i''+1</sub>,..., which is a suffix of ''w''. Formally, the satisfaction relation ⊨ between a word and an LTL formula is defined as follows:
* ''w'' ⊨ ''p'' if ''p'' ∈ ''w''(0)
* ''w'' ⊨ ¬{{var|ψ}} if ''w'' ⊭ {{var|ψ}}
* ''w'' ⊨ {{var|φ}} ∨ {{var|ψ}} if ''w'' ⊨ {{var|φ}} or ''w'' ⊨ {{var|ψ}}
* {{math|''w'' ⊨ '''X''' {{var|ψ}}}} if ''w''<sup>1</sup> ⊨ {{var|ψ}} (in the ne'''x'''t time step {{var|ψ}} must be true)
* {{math|''w'' ⊨ {{var|φ}} '''U''' {{var|ψ}}}} if there exists ''i'' ≥ 0 such that ''w''<sup>''i''</sup> ⊨ {{var|ψ}} and for all 0 ≤ ''k'' < i, ''w''<sup>''k''</sup> ⊨ {{var|φ}}  ({{var|φ}} must remain true '''u'''ntil {{var|ψ}} becomes true)

We say an ω-word ''w'' satisfies an LTL formula {{var|ψ}} when ''w'' ⊨ {{var|ψ}}. 
The [[ω-language]] ''L''({{var|ψ}}) defined by {{var|ψ}} is {''w'' | ''w'' ⊨ {{var|ψ}}}, which is the set of ω-words that satisfy {{var|ψ}}.
A formula {{var|ψ}} is ''satisfiable'' if there exist an ω-word ''w'' such that ''w'' ⊨ {{var|ψ}}. 
A formula {{var|ψ}} is ''valid'' if for each ω-word ''w'' over alphabet 2<sup>''AP''</sup>, we have ''w'' ⊨ {{var|ψ}}.

The additional logical operators are defined as follows:
* {{var|φ}} ∧ {{var|ψ}} ≡ ¬(¬{{var|φ}} ∨ ¬{{var|ψ}})
* {{var|φ}} → {{var|ψ}} ≡ ¬{{var|φ}} ∨ {{var|ψ}}
* {{var|φ}} ↔ {{var|ψ}} ≡ ({{var|φ}} → {{var|ψ}}) ∧ ( {{var|ψ}} → {{var|φ}})
* '''true''' ≡ ''p'' ∨ ¬''p'', where ''p'' ∈ ''AP''
* '''false''' ≡ ¬'''true'''
The additional temporal operators '''R''', '''F''', and '''G''' are defined as follows:
* {{var|ψ}} '''R''' {{var|φ}} ≡ ¬(¬{{var|ψ}} '''U''' ¬{{var|φ}}) ( {{var|φ}} remains true until and including once {{var|ψ}} becomes true. If {{var|ψ}} never becomes true, {{var|φ}} must remain true forever. {{var|ψ}} '''r'''eleases {{var|φ}}.)
* {{math|'''F''' {{var|ψ}} ≡  '''true''' '''U''' {{var|ψ}}}}  (eventually {{var|ψ}} becomes true)
*'''G''' {{var|ψ}} ≡  '''false''' '''R''' {{var|ψ}} ≡ ¬'''F''' ¬{{var|ψ}} ({{var|ψ}} always remains true)

=== Weak until and strong release ===

Some authors also define a ''weak until'' binary operator, denoted '''W''', with semantics similar to that of the until operator but the stop condition is not required to occur (similar to release).<ref>Sec. 5.1.5 "Weak Until, Release, and Positive Normal Form" of Principles of Model Checking.</ref> It is sometimes useful since both '''U''' and '''R''' can be defined in terms of the weak until:
* {{math|''ψ'' '''W''' ''φ'' ≡ (''ψ'' '''U''' ''φ'') ∨ '''G''' ''ψ'' ≡ ''ψ'' '''U''' (''φ'' ∨ '''G''' ''ψ'') ≡  ''φ'' '''R''' (''φ'' ∨ ''ψ'')}}
* {{math|''ψ'' '''U''' ''φ'' ≡ '''F'''''φ''  ∧ (''ψ'' '''W''' ''φ'')}}
* {{math|''ψ'' '''R''' ''φ'' ≡ ''φ'' '''W''' (''φ'' ∧ ''ψ'')}}

The ''strong release'' binary operator, denoted '''M''', is the dual of weak until. It is defined similar to the until operator, so that the release condition has to hold at some point. Therefore, it is stronger than the release operator.
* {{math|''ψ'' '''M''' ''φ'' ≡ ¬(¬''ψ'' '''W''' ¬''φ'') ≡ (''ψ'' '''R''' ''φ'') ∧ '''F''' ''ψ'' ≡ ''ψ'' '''R''' (''φ'' ∧ '''F''' ''ψ'') ≡ ''φ'' '''U''' (''ψ'' ∧ ''φ'')}}

The semantics for the temporal operators are pictorially presented as follows.

{| class="wikitable"
|-
!Textual
!Symbolic
!Explanation
!Diagram
|-
| colspan="4" | [[Unary operation|Unary operators]]:
|-
|'''X''' ''φ''
|<math>\bigcirc \varphi</math>
|ne'''X'''t: ''φ'' has to hold at the next state.
|[[File:Ltlnext.svg|LTL next operator]]
|-
|'''F''' ''φ''
|<math>\Diamond \varphi</math>
|'''F'''inally: ''φ'' eventually has to hold (somewhere on the subsequent path).
|[[File:Ltleventually.svg|LTL eventually operator]]
|-
|'''G''' ''φ''
|<math>\Box \varphi</math>
|'''G'''lobally: ''φ'' has to hold on the entire subsequent path.
|[[File:Ltlalways.svg|LTL always operator]]
|-
| colspan="4" | [[Binary operator]]s:
|-
|''ψ'' '''U''' ''φ''
|<math>\psi\;\mathcal{U}\,\varphi</math>
|'''U'''ntil: ''ψ'' has to hold ''at least'' until ''φ'' becomes true, which must hold at the current or a future position.
|[[File:Ltluntil.svg|LTL until operator]]
|-
|''ψ'' '''R''' ''φ''
|<math>\psi\;\mathcal{R}\,\varphi</math>
|'''R'''elease: ''φ'' has to be true until and including the point where ''ψ'' first becomes true; if ''ψ'' never becomes true, ''φ'' must remain true forever.
|[[File:Ltlrelease-stop.svg|LTL release operator (which stops)]]<br>
[[File:Ltlrelease-nostop.svg|LTL release operator (which does not stop)]]
|-
|''ψ'' '''W''' ''φ''
|<math>\psi\;\mathcal{W}\,\varphi</math>
|'''W'''eak until: ''ψ'' has to hold ''at least'' until ''φ''; if ''φ'' never becomes true, ''ψ'' must remain true forever.
|[[File:Ltluntil.svg|LTL weak until operator (which stops)]]<br>
[[File:Ltlweakuntil2.svg|LTL weak until operator (which does not stop)]]
|- 
|''ψ'' '''M''' ''φ''
|<math>\psi\;\mathcal{M}\,\varphi</math>
|Strong release: ''φ'' has to be true until and including the point where ''ψ'' first becomes true, which must hold at the current or a future position.
|[[File:Ltlrelease-stop.svg|LTL strong release operator]]
|}

==Equivalences==
Let φ, ψ, and ρ be LTL formulas. The following tables list some of the useful equivalences that extend standard equivalences among the usual logical operators.

{| class="wikitable"
|-
! colspan="3" | Distributivity 
|-
| '''X''' (φ ∨ ψ) ≡  ('''X''' φ) ∨ ('''X''' ψ)|| '''X''' (φ ∧ ψ) ≡  ('''X''' φ) ∧ ('''X''' ψ)  || '''X''' (φ '''U''' ψ)≡  ('''X''' φ) '''U''' ('''X''' ψ)
|-
| '''F''' (φ ∨ ψ) ≡  ('''F''' φ) ∨ ('''F''' ψ)|| '''G''' (φ ∧ ψ) ≡  ('''G''' φ) ∧ ('''G''' ψ)  || 
|-
| ρ '''U''' (φ ∨ ψ) ≡  (ρ '''U''' φ) ∨ (ρ '''U''' ψ)|| (φ ∧ ψ) '''U''' ρ ≡  (φ '''U''' ρ) ∧ (ψ '''U''' ρ)  || 
|}

{| class="wikitable"
|-
! colspan="4" | Negation propagation
|-
| '''''X''' is self-dual'' || '''''F''' and '''G''' are dual'' || '''''U''' and '''R''' are dual''  || '''''W''' and '''M''' are dual''
|-
| ¬'''X''' φ ≡ '''X''' ¬φ  || ¬'''F''' φ ≡ '''G''' ¬φ          || ¬ (φ '''U''' ψ) ≡ (¬φ '''R''' ¬ψ) || ¬ (φ '''W''' ψ) ≡ (¬φ '''M''' ¬ψ)
|-
|                          || ¬'''G''' φ ≡ '''F''' ¬φ          || ¬ (φ '''R''' ψ) ≡ (¬φ '''U''' ¬ψ) || ¬ (φ '''M''' ψ) ≡ (¬φ '''W''' ¬ψ)
|}
 
{| class="wikitable"
|-
! colspan="3" | Special temporal properties
|-
| '''F''' φ ≡ '''F''' '''F''' φ || '''G''' φ ≡ '''G''' '''G''' φ || φ '''U''' ψ ≡  φ '''U''' (φ '''U''' ψ)
|-
| φ '''U''' ψ ≡  ψ ∨ ( φ ∧ '''X'''(φ '''U''' ψ) ) || φ '''W''' ψ ≡  ψ ∨ ( φ ∧ '''X'''(φ '''W''' ψ) ) || φ '''R''' ψ ≡ ψ ∧ (φ ∨ '''X'''(φ '''R''' ψ) )
|-
| '''G''' φ ≡ φ ∧ '''X'''('''G''' φ) ||'''F''' φ ≡ φ ∨ '''X'''('''F''' φ) || 
|}

==Negation normal form==

All the formulas of LTL can be transformed into ''negation normal form'', where
* all negations appear only in front of the atomic propositions,
* only other logical operators '''true''', '''false''', ∧, and ∨ can appear, and
* only the temporal operators '''X''', '''U''', and '''R''' can appear.
Using the above equivalences for negation propagation, it is possible to derive the normal form. This normal form allows '''R''', '''true''', '''false''', and ∧ to appear in the formula, which are not fundamental operators of LTL. Note that the transformation to the negation normal form does not blow up the length of the formula. This normal form is useful in [[Linear temporal logic to Büchi automaton|translation from an LTL formula to a Büchi automaton]].

==Relations with other logics==
LTL can be shown to be equivalent to the [[monadic first-order logic of order]], FO[<]&mdash;a result known as [[Kamp's theorem]]&mdash;<ref>{{cite book|url=https://books.google.com/books?id=TLpcI2axv8kC&pg=PA22 |title=Automata, Languages and Programming: 37th International Colloquium, ICALP ... - Google Books |date=2010-06-30 |access-date=2014-07-30|isbn=9783642141614 |last1=Abramsky |first1=Samson |author1link = Samson Abramsky|last2=Gavoille |first2=Cyril |last3=Kirchner |first3=Claude |last4=Spirakis |first4=Paul |publisher=Springer }}</ref> or equivalently to [[star-free language]]s.<ref>{{cite book|editor1=[[Orna Grumberg]] |editor2=[[Helmut Veith]] |title=25 years of model checking: history, achievements, perspectives|year=2008|publisher=Springer|isbn=978-3-540-69849-4|chapter=From [[Alonzo Church|Church]] and Prior to [[Property Specification Language|PSL]]|author=Moshe Y. Vardi|author-link=Moshe Y. Vardi }} [http://www.cs.rice.edu/~vardi/papers/25mc.ps.gz preprint]</ref>

[[Computation tree logic]] (CTL) and linear temporal logic (LTL) are both a subset of [[CTL*]], but are incomparable. For example,
* No formula in CTL can define the language that is defined by the LTL formula '''F'''('''G''' p).
*No formula in LTL can define the language that is defined by the CTL formulas '''AG'''( p → ('''EX'''q ∧ '''EX'''¬q) ) or  '''AG'''('''EF'''(p)).

== Computational problems ==
[[Model checking]] and satisfiability against an LTL formula are [[PSPACE-complete]] problems. LTL synthesis and the problem of verification of games against an LTL winning condition is [[2-EXPTIME|2EXPTIME-complete]].<ref> A. Pnueli and R. Rosner. "On the synthesis of a reactive module" In Proceedings of the 16th ACM SIGPLAN-SIGACT [[Symposium on Principles of programming languages]] (POPL '89). Association for Computing Machinery, New York, NY, USA, 179–190. https://doi.org/10.1145/75277.75293</ref>

==Applications==

;Automata-theoretic linear temporal logic model checking
:LTL formulas are commonly used to express constraints, specifications, or processes that a system should follow. The field of model checking aims to formally verify whether a system meets a given specification. In the case of automata-theoretic model checking, both the system of interest and a specification are expressed as separate [[finite-state machines]], or automata, and then compared to evaluate whether the system is guaranteed to have the specified property. In computer science, this type of model checking is often used to verify that an algorithm is structured correctly. 

:To check LTL specifications on infinite system runs, a common technique is to obtain a [[Büchi automaton]] that is equivalent to the model (accepts an ω-word precisely if it is the model) and another one that is equivalent to the negation of the property (accepts an ω-word precisely it satisfies the negated property) (cf. [[Linear temporal logic to Büchi automaton]]). In this case, if there is an overlap in the set of ω-words accepted by the two automata, it implies that the model accepts some behaviors which violate the desired property. If there is no overlap, there are no property-violating behaviors which are accepted by the model. Formally, the intersection of the two non-deterministic Büchi automata is empty if and only if the model satisfies the specified property.<ref>Moshe Y. Vardi. ''An Automata-Theoretic Approach to Linear Temporal Logic.''  Proceedings of the 8th Banff Higher Order Workshop (Banff'94).  [[Lecture Notes in Computer Science]], vol. 1043, pp. 238–266, Springer-Verlag, 1996. {{ISBN|3-540-60915-6}}.</ref>

;Expressing important properties in formal verification
:There are two main types of properties that can be expressed using linear temporal logic: '''[[safety property|safety]]''' properties usually state that ''something bad never happens'' ('''G'''&not;''&varphi;''), while '''[[liveness]]''' properties state that ''something good keeps happening'' ('''GF'''''&psi;'' or '''G'''(''&varphi;'' →'''F'''''&psi;'')).<ref>Bowen Alpern, [[Fred B. Schneider]], ''Defining Liveness'', [[Information Processing Letters]], Volume 21, Issue 4, 1985, Pages 181-185, ISSN 0020-0190, https://doi.org/10.1016/0020-0190(85)90056-0</ref> For example, a safety property may require that an autonomous rover never drives over a cliff, or that a software product never allows a successful login with an incorrect password. A liveness property may require that the rover always continues to collect data samples, or that a software product repeatedly sends telemetry data.

:More generally, safety properties are those for which every [[counterexample]] has a finite prefix such that, however it is extended to an infinite path, it is still a counterexample. For liveness properties, on the other hand, every finite path can be extended to an infinite path that satisfies the formula.

;Specification language
:One of the applications of linear temporal logic is the specification of [[preference]]s in the [[Planning Domain Definition Language]] for the purpose of [[preference-based planning]].{{citation needed|date=January 2011}}

==Extensions==
Parametric linear temporal logic extends LTL with variables on the until-modality.<ref>{{Cite book|last1=Chakraborty|first1=Souymodip|last2=Katoen|first2=Joost-Pieter|date=2014|editor-last=Diaz|editor-first=Josep|editor2-last=Lanese|editor2-first=Ivan|editor3-last=Sangiorgi|editor3-first=Davide|chapter=Parametric LTL on Markov Chains|title=[[Theoretical Computer Science (journal)|Theoretical Computer Science]]|volume=7908|series=Lecture Notes in Computer Science|language=en|publisher=Springer Berlin Heidelberg|pages=207–221|doi=10.1007/978-3-662-44602-7_17|arxiv=1406.6683|bibcode=2014arXiv1406.6683C|isbn=978-3-662-44602-7|s2cid=12538495 }}</ref>

==See also==
{{Commons category|Linear temporal logic}}
*[[Action language]]
*[[Metric temporal logic]]
*[[Safety and liveness properties]]

==References==
{{reflist}}

== External links ==
* [http://www.dcs.qmul.ac.uk/~pm/SaR/2004ltl.pdf A presentation of LTL]
* [http://www.cmi.ac.in/~madhavan/papers/pdf/isical97.pdf Linear-Time Temporal Logic and Büchi Automata]
*[http://www.inf.unibz.it/~artale/FM/slide3.pdf LTL Teaching slides] of professor [[Alessandro Artale]] at the [[Free University of Bozen-Bolzano]]
*[https://web.archive.org/web/20090830133455/http://spot.lip6.fr/wiki/LtlTranslationAlgorithms LTL to Buchi translation algorithms] a genealogy, from the website of [http://spot.lip6.fr/ Spot] a library for model checking.

[[Category:Computer-related introductions in 1977]]
[[Category:Temporal logic]]