Editing Linear temporal logic (section)

==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}}