Overview
Linear Temporal Logic (LTL) is a propositional temporal logic for describing how truth values evolve along a single execution trace. A trace is usually represented as an infinite sequence of states indexed by the natural numbers.
From a modal perspective, always and eventually behave like box and diamond modalities over the future ordering of time. This ordering is transitive and linear. Standard LTL nevertheless contains more structure than an ordinary transitive modal logic: time is normally discrete, the next-time operator refers to the immediate successor, and the binary until operator relates an interval of states to a future endpoint.
LTL was introduced into program verification by Amir Pnueli. The later work of Dov M. Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi established the central role of until in expressing responsiveness and fairness properties.
Syntax
Let \mathit{AP} be a set of atomic propositions. LTL formulas are generated by
\varphi ::= p \mid \neg\varphi \mid (\varphi\land\psi) \mid \mathsf{X}\varphi \mid (\varphi\mathbin{\mathsf{U}}\psi),
where p\in\mathit{AP}.
The temporal operators are:
\mathsf{X}\varphi: \varphi holds at the next position; \varphi\mathbin{\mathsf{U}}\psi: \varphi holds until \psi becomes true.
The usual future modalities are definable from until:
\mathsf{F}\varphi := \top\mathbin{\mathsf{U}}\varphi,
\mathsf{G}\varphi := \neg\mathsf{F}\neg\varphi.
Thus, \mathsf{F}\varphi means that \varphi is true eventually, whereas \mathsf{G}\varphi means that \varphi remains true always.
Weak until is defined by
\varphi\mathbin{\mathsf{W}}\psi := (\varphi\mathbin{\mathsf{U}}\psi) \lor \mathsf{G}\varphi.
Unlike strong until, weak until does not require \psi ever to become true.
Semantics
An LTL model is an infinite word \sigma_0\sigma_1\sigma_2\ldots \in (2^{\mathit{AP}})^\omega.
Each \sigma_i contains the propositions true at time i. The satisfaction relation is defined by
\sigma,i\models p \quad\Longleftrightarrow\quad p\in\sigma_i,
\sigma,i\models\mathsf{X}\varphi \quad\Longleftrightarrow\quad \sigma,i+1\models\varphi,
and
\sigma,i\models \varphi\mathbin{\mathsf{U}}\psi
if and only if there is some j\geq i such that
\sigma,j\models\psi
and
\sigma,k\models\varphi
for every k with i\leq k<j.
A trace satisfies \varphi, written \sigma\models\varphi, when \sigma,0\models\varphi.
For model checking, traces are generated by a transition system. The system satisfies an LTL formula when every trace beginning in an initial state satisfies that formula.
Until and Fixpoints
The until operator satisfies the recursive equation
\varphi\mathbin{\mathsf{U}}\psi \equiv \psi\lor \bigl( \varphi\land \mathsf{X}(\varphi\mathbin{\mathsf{U}}\psi) \bigr).
It may therefore be understood as a least fixpoint: \mu Z. \bigl( \psi\lor(\varphi\land\mathsf{X}Z) \bigr).
Similarly, \mu Z.(\varphi\lor\mathsf{X}Z)
and \nu Z.(\varphi\land\mathsf{X}Z).
These are semantic characterizations. Standard LTL does not itself contain explicit fixpoint variables or the binders \mu and \nu.
Examples
The response property
\mathsf{G} \bigl( \mathit{request} \rightarrow \mathsf{F}\mathit{grant} \bigr)
states that every request is eventually followed by a grant.
The safety property
\mathsf{G}\neg\mathit{error}
states that an error never occurs.
The recurrence property
\mathsf{G}\mathsf{F}\,\mathit{scheduled}
requires a process to be scheduled infinitely often.
Finally,
\mathit{safe} \mathbin{\mathsf{U}} \mathit{finished}
requires the system to remain safe until it eventually finishes.
Expressive Power
Gabbay, Pnueli, Shelah, and Stavi showed that adding until provides the expressive strength required to describe first-order properties of \omega-ordered time when formulas are evaluated at the initial point.
In the broader temporal language, until is paired with its past-time counterpart since. Gabbay’s separation theorem states, for standard linear time structures, that formulas combining past and future operators can be transformed into Boolean combinations of pure-past, present, and pure-future formulas.
Over the natural numbers, past-time operators do not add expressive power for specifications evaluated at the beginning of a trace, although they may provide exponentially more concise formulas. Over more general linear orders, the exact expressive-completeness results depend on structural properties of the time order and may require additional Stavi connectives.
Model Checking and Complexity
Every LTL formula can be translated into a Büchi automaton accepting exactly its satisfying traces. To check whether a transition system satisfies \varphi, the system is combined with an automaton for \neg\varphi. An accepting run of the product represents a counterexample.
LTL satisfiability and validity are PSPACE-complete. The combined model-checking problem is also PSPACE-complete. Standard automata-theoretic algorithms are linear in the size of the transition system and exponential in the size of the formula.
Every satisfiable LTL formula has an ultimately periodic model of the form
uv^\omega.
Consequently, infinite satisfying traces and counterexamples can be represented by a finite prefix followed by a finite loop.
Relations to Other Logics
LTL describes individual execution traces. CTL instead combines temporal operators with explicit path quantifiers, while CTL* contains both styles of temporal reasoning.
The modal \mu-calculus contains explicit least- and greatest-fixpoint operators and subsumes the fixpoint patterns used to characterize LTL operators.
Common variants include finite-trace LTL, past-time LTL, Metric Temporal Logic, and HyperLTL.
References
- Amir Pnueli: The Temporal Logic of Programs. 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46–57.
- Dov M. Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi: On the Temporal Analysis of Fairness. POPL, 1980, pp. 163–173.
- Dov M. Gabbay, Ian Hodkinson, and Mark Reynolds: Temporal Logic: Mathematical Foundations and Computational Aspects, Volume 1. Oxford University Press, 1994.
- A. Prasad Sistla and Edmund M. Clarke: The Complexity of Propositional Linear Temporal Logics. Journal of the ACM 32(3), 1985, pp. 733–749.
- Moshe Y. Vardi and Pierre Wolper: An Automata-Theoretic Approach to Automatic Program Verification. LICS, 1986, pp. 332–344.