In logic, linear temporal logic or linear-time temporal logic [1] [2] (LTL) is a modal temporal logic 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. LTL is sometimes called propositional temporal logic, abbreviated PTL. [3] In terms of expressive power, linear temporal logic (LTL) is a fragment of first-order logic. [4] [5]
LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977. [6]
LTL is built up from a finite set of propositional variables AP, the logical operators ¬ and ∨, and the temporal modal operators X (some literature uses O or N) and U. Formally, the set of LTL formulas over AP is inductively defined as follows:
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, in order to write LTL formulas succinctly. The additional logical operators are ∧, →, ↔, true, and false. Following are the additional temporal operators.
An LTL formula can be 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 ω-word over alphabet 2AP). Let w = a0,a1,a2,... be such an ω-word. Let w(i) = ai. Let wi = ai,ai+1,..., which is a suffix of w. Formally, the satisfaction relation ⊨ between a word and an LTL formula is defined as follows:
We say an ω-word w satisfies an LTL formula ψ when w ⊨ ψ. The ω-language L(ψ) defined by ψ is {w | w ⊨ ψ}, 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 2AP, we have w ⊨ ψ.
The additional logical operators are defined as follows:
The additional temporal operators R, F, and G are defined as follows:
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). [8] It is sometimes useful since both U and R can be defined in terms of the weak until:
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.
The semantics for the temporal operators are pictorially presented as follows.
Textual | Symbolic | Explanation | Diagram |
---|---|---|---|
Unary operators: | |||
Xφ | neXt: φ has to hold at the next state. | ![]() | |
Fφ | Finally: φ eventually has to hold (somewhere on the subsequent path). | ![]() | |
Gφ | Globally: φ has to hold on the entire subsequent path. | ![]() | |
Binary operators: | |||
ψUφ | Until: ψ has to hold at least until φ becomes true, which must hold at the current or a future position. | ![]() | |
ψRφ | Release: φ has to be true until and including the point where ψ first becomes true; if ψ never becomes true, φ must remain true forever. | ![]() | |
ψWφ | Weak until: ψ has to hold at least until φ; if φ never becomes true, ψ must remain true forever. | ![]() | |
ψMφ | 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. | ![]() |
Let φ, ψ, and ρ be LTL formulas. The following tables list some of the useful equivalences that extend standard equivalences among the usual logical operators.
Distributivity | ||
---|---|---|
X (φ ∨ ψ) ≡ (X φ) ∨ (X ψ) | X (φ ∧ ψ) ≡ (X φ) ∧ (X ψ) | X (φ U ψ)≡ (X φ) U (X ψ) |
F (φ ∨ ψ) ≡ (F φ) ∨ (F ψ) | G (φ ∧ ψ) ≡ (G φ) ∧ (G ψ) | |
ρ U (φ ∨ ψ) ≡ (ρ U φ) ∨ (ρ U ψ) | (φ ∧ ψ) U ρ ≡ (φ U ρ) ∧ (ψ U ρ) |
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 ¬ψ) |
Special temporal properties | ||
---|---|---|
F φ ≡ FF φ | G φ ≡ GG φ | φ U ψ ≡ φ U (φ U ψ) |
φ U ψ ≡ ψ ∨ ( φ ∧ X(φ U ψ) ) | φ W ψ ≡ ψ ∨ ( φ ∧ X(φ W ψ) ) | φ R ψ ≡ ψ ∧ (φ ∨ X(φ R ψ) ) |
G φ ≡ φ ∧ X(G φ) | F φ ≡ φ ∨ X(F φ) |
All the formulas of LTL can be transformed into negation normal form, where
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 translation from an LTL formula to a Büchi automaton.
LTL can be shown to be equivalent to the monadic first-order logic of order, FO[<]—a result known as Kamp's theorem — [9] or equivalently to star-free languages. [10]
Computation tree logic (CTL) and linear temporal logic (LTL) are both a subset of CTL*, but are incomparable. For example,
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 2EXPTIME-complete. [11]
Parametric linear temporal logic extends LTL with variables on the until-modality. [14]
In logic, disjunction, also known as logical disjunction or logical or or logical addition or inclusive disjunction, is a logical connective typically notated as and read aloud as "or". For instance, the English language sentence "it is sunny or it is warm" can be represented in logic using the disjunctive formula , assuming that abbreviates "it is sunny" and abbreviates "it is warm".
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 quantified variables over non-logical objects, and allows the use of sentences that contain variables, so that rather than propositions such as "Socrates is a man", one can have expressions in the form "there exists x such that x is Socrates and x is a man", where "there exists" is a quantifier, while x is a variable. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.
Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions and relations between propositions, including the construction of arguments based on them. Compound propositions are formed by connecting propositions by logical connectives. Propositions that contain no logical connectives are called atomic propositions.
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.
In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. It is sometimes also used to refer to tense logic, a modal logic-based system of temporal logic introduced by Arthur Prior in the late 1950s, with important contributions by Hans Kamp. It has been further developed by computer scientists, notably Amir Pnueli, and logicians.
Modal logic is a kind of logic used to represent statements about necessity and possibility. It plays a major role in philosophy and related fields as a tool for understanding concepts such as knowledge, obligation, and causation. For instance, in epistemic modal logic, the formula can be used to represent the statement that is known. In deontic modal logic, that same formula can represent that is a moral obligation.
Property Specification Language (PSL) is a temporal logic extending linear temporal logic with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of regular expressions and syntactic sugaring. It is widely used in the hardware design and verification industry, where formal verification tools and/or logic simulation tools are used to prove or refute that a given PSL formula holds on a given design.
Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers, which determine if a given artifact possesses safety or liveness properties. For example, CTL can specify that when some initial condition is satisfied, then all possible executions of a program avoid some undesirable condition. In this example, the safety property could be verified by a model checker that explores all possible transitions out of program states satisfying the initial condition and ensures that all such executions satisfy the property. Computation tree logic belongs to a class of temporal logics that includes linear temporal logic (LTL). Although there are properties expressible only in CTL and properties expressible only in LTL, all properties expressible in either logic can also be expressed in CTL*.
Independence-friendly logic is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form and , where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of IF sentences can characterize the same classes of structures as existential second-order logic.
In theoretical computer science, the modal μ-calculus is an extension of propositional modal logic by adding the least fixed point operator μ and the greatest fixed point operator ν, thus a fixed-point logic.
CTL* is a superset of computational tree logic (CTL) and linear temporal logic (LTL). It freely combines path quantifiers and temporal operators. Like CTL, CTL* is a branching-time logic. The formal semantics of CTL* formulae are defined with respect to a given Kripke structure.
An interpretation is an assignment of meaning to the symbols of a formal language. Many formal languages used in mathematics, logic, and theoretical computer science are defined in solely syntactic terms, and as such do not have any meaning until they are given some interpretation. The general study of interpretations of formal languages is called formal semantics.
In automata theory, a semi-deterministic Büchi automaton is a special type of Büchi automaton. In such an automaton, the set of states can be partitioned into two subsets: one subset forms a deterministic automaton and also contains all the accepting states.
In automata theory, a generalized Büchi automaton is a variant of a Büchi automaton. The difference with the Büchi automaton is the accepting condition, which is determined by a set of sets of states. A run is accepted by the automaton if it visits at least one state of every set of the accepting condition infinitely often. Generalized Büchi automata are equivalent in expressive power to Büchi automata; a transformation is given here.
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 translate an LTL formula to a BA. This transformation is normally done in two steps. The first step produces a generalized Büchi automaton (GBA) from a LTL formula. The second step translates this GBA into a BA, which involves a relatively easy construction. Since LTL is strictly less expressive than BA, the reverse construction is not always possible.
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 linear-time logic that assumes both the interleaving and fictitious-clock abstractions. It is defined over a point-based weakly-monotonic integer-time semantics.
In model checking, the Metric Interval Temporal Logic (MITL) is a fragment of Metric Temporal Logic (MTL). This fragment is often preferred to MTL because some problems that are undecidable for MTL become decidable for MITL.
In model checking, a field of computer science, timed propositional temporal logic (TPTL) is an extension of propositional linear temporal logic (LTL) in which variables are introduced to measure times between two events. For example, while LTL allows to state that each event p is eventually followed by an event q, TPTL furthermore allows to give a time limit for q to occur.
In model checking, a branch of computer science, linear time properties are used to describe requirements of a model of a computer system. Example properties include "the vending machine does not dispense a drink until money has been entered" or "the computer program eventually terminates". Fairness properties can be used to rule out unrealistic paths of a model. For instance, in a model of two traffic lights, the liveness property "both traffic lights are green infinitely often" may only be true under the unconditional fairness constraint "each traffic light changes colour infinitely often".
Principles of Model Checking is a textbook on model checking, an area of computer science that automates the problem of determining if a machine meets specification requirements. It was written by Christel Baier and Joost-Pieter Katoen, and published in 2008 by MIT Press.