In
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premis ...
, linear temporal logic or linear-time temporal logic (LTL) is a
modal temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
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''.
In terms of
expressive power, linear temporal logic (LTL) is a fragment of
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quanti ...
.
LTL was first proposed for the
formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal met ...
of computer programs by
Amir Pnueli in 1977.
Syntax
LTL is built up from a finite set of
propositional variable
In mathematical logic, a propositional variable (also called a sentential variable or sentential letter) is an input variable (that can either be true or false) of a truth function. Propositional variables are the basic building-blocks of propos ...
s ''AP'', the
logical operators ¬ and ∨, and the
temporal modal operator
A modal connective (or modal operator) is a logical connective for modal logic. It is an operator which forms propositions from propositions. In general, a modal operator has the "formal" property of being non- truth-functional in the following se ...
s X (some literature uses O or N) and U.
Formally, the set of LTL formulas over ''AP'' is inductively defined as follows:
* if p ∈ ''AP'' then p is an LTL formula;
* if ψ and φ are LTL formulas then ¬ψ, φ ∨ ψ, X ψ, and φ U ψ are LTL formulas.
X is read as next and U is read as until.
Other than these fundamental operators, there are additional logical and temporal operators defined in terms of the fundamental operators to write LTL formulas succinctly.
The additional logical operators are ∧, →, ↔, true, and false.
Following are the additional temporal operators.
* G for always (globally)
* F for finally
* R for release
* W for weak until
* M for mighty release
Semantics
An LTL formula can be ''
satisfied'' by an infinite sequence of truth evaluations of variables in ''AP''.
These sequences can be viewed as a word on a path of a
Kripke structure : ''This article describes Kripke structures as used in model checking. For a more general description, see Kripke semantics''.
A Kripke structure is a variation of the transition system, originally proposed by Saul Kripke, used in model checkin ...
(an
ω-word over
alphabet
An alphabet is a standardized set of basic written graphemes (called letters) that represent the phonemes of certain spoken languages. Not all writing systems represent language in this way; in a syllabary, each character represents a s ...
2
''AP'').
Let ''w'' = a
0,a
1,a
2,... be such an ω-word. Let ''w''(''i'') = ''a
i''. Let ''w''
i = ''a
i'',''a''
''i''+1,..., 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'' ⊨ ¬ if ''w'' ⊭
* ''w'' ⊨ ∨ if ''w'' ⊨ or ''w'' ⊨
* ''w'' ⊨ X if ''w''
1 ⊨ (in the next time step must be true)
* ''w'' ⊨ U if there exists ''i'' ≥ 0 such that ''w''
''i'' ⊨ and for all 0 ≤ ''k'' < i, ''w''
k ⊨ ( must remain true until becomes true)
We say an ω-word ''w'' satisfies an LTL formula when ''w'' ⊨ .
The
ω-language
In formal language theory within theoretical computer science, an infinite word is an infinite-length sequence (specifically, an ω-length sequence) of symbols, and an ω-language is a set of infinite words. Here, ω refers to the first ordina ...
''L''() defined by is , which is the set of ω-words that satisfy .
A formula is ''satisfiable'' if there exist an ω-word ''w'' such that ''w'' ⊨ .
A formula is ''valid'' if for each ω-word ''w'' over alphabet 2
''AP'', ''w'' ⊨ .
The additional logical operators are defined as follows:
* ∧ ≡ ¬(¬ ∨ ¬)
* → ≡ ¬ ∨
* ↔ ≡ ( → ) ∧ ( → )
* true ≡ p ∨ ¬p, where p ∈ ''AP''
* false ≡ ¬true
The additional temporal operators R, F, and G are defined as follows:
* R ≡ ¬(¬ U ¬) ( remains true until and including once becomes true. If never becomes true, must remain true forever.)
*F ≡ true U (eventually becomes true)
*G ≡ false R ≡ ¬F ¬ ( 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). It is sometimes useful since both U and R can be defined in terms of the weak until:
* ''ψ'' W ''φ'' ≡ (''ψ'' U ''φ'') ∨ G ''ψ'' ≡ ''ψ'' U (''φ'' ∨ G ''ψ'') ≡ ''φ'' R (''φ'' ∨ ''ψ'')
* ''ψ'' U ''φ'' ≡ F''φ'' ∧ (''ψ'' W ''φ'')
* ''ψ'' 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.
* ''ψ'' M ''φ'' ≡ ¬(¬''ψ'' W ¬''φ'') ≡ (''ψ'' R ''φ'') ∧ F ''ψ'' ≡ ''ψ'' R (''φ'' ∧ F ''ψ'') ≡ ''φ'' U (''ψ'' ∧ ''φ'')
The semantics for the temporal operators are pictorially presented as follows.
Equivalences
Let φ, ψ, and ρ be LTL formulas. The following tables list some of the useful equivalences that extend standard equivalences among the usual logical operators.
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 size of the formula. This normal form is useful in
translation from LTL to 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— or equivalently
star-free language A regular language is said to be star-free if it can be described by a regular expression constructed from the letters of the alphabet, the empty set symbol, all boolean operators – including complementation – and concatenation but no K ...
s.
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 → (EXq ∧ EX¬q) ) or AG(EF(p)).
Computational problems
Model checking and satisfiability against an LTL formula are
PSPACE-complete In computational complexity theory, a decision problem is PSPACE-complete if it can be solved using an amount of memory that is polynomial in the input length ( polynomial space) and if every other problem that can be solved in polynomial space can ...
problems. LTL synthesis and the problem of verification of games against an LTL winning condition is
2EXPTIME-complete.
Applications
;Automata-theoretic linear temporal logic model checking
:An important way to model check is to express desired properties (such as the ones described above) using LTL operators and actually check if the model satisfies this property. One technique is to obtain a
Büchi automaton
In computer science and automata theory, a deterministic Büchi automaton is a theoretical machine which either accepts or rejects infinite inputs. Such a machine has a set of states and a transition function, which determines which state the machi ...
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 formal verification,
finite state model checking needs to find a Büchi automaton (BA) equivalent to a given linear temporal logic (LTL) formula, i.e., such that the LTL formula and the BA recognize the same ω-language. There are algorithms that ...
). The intersection of the two non-deterministic Büchi automata is empty if and only if the model satisfies the property.
;Expressing important properties in formal verification
:There are two main types of properties that can be expressed using linear temporal logic:
safety
Safety is the state of being "safe", the condition of being protected from harm or other danger. Safety can also refer to the control of recognized hazards in order to achieve an acceptable level of risk.
Meanings
There are two slightly di ...
properties usually state that ''something bad never happens'' (G¬''ϕ''), while
liveness properties state that ''something good keeps happening'' (GF''ψ'' or G(''ϕ'' →F''ψ'')). More generally, safety properties are those for which every
counterexample
A counterexample is any exception to a generalization. In logic a counterexample disproves the generalization, and does so rigorously in the fields of mathematics and philosophy. For example, the fact that "John Smith is not a lazy student" is ...
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 prefix of a counterexample 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
preferences in the
Planning Domain Definition Language for the purpose of
preference-based planning.
Extensions
Parametric linear temporal logic extends LTL with variables on the until-modality.
See also
*
Action language
In computer science, an action language is a language for specifying state transition systems, and is commonly used to create formal models of the effects of actions on the world. Action languages are commonly used in the artificial intelligence ...
*
Metric temporal logic Metric temporal logic (MTL) is a special case of temporal logic. It is an extension of temporal logic in which temporal operators are replaced by time-constrained versions like ''until'', ''next'', ''since'' and ''previous'' operators. It is a line ...
*
Safety and liveness properties
References
{{reflist
;External links
A presentation of LTLLinear-Time Temporal Logic and Büchi AutomataLTL Teaching slidesof professor
Alessandro Artale at the
Free University of Bozen-BolzanoLTL to Buchi translation algorithmsa genealogy, from the website o
Spota library for model-checking.
Computer-related introductions in 1977
Temporal logic