Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
Concept
Linear temporal logic
Summary
In logic, linear temporal logic or linear-time temporal logic (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.
In terms of expressive power, linear temporal logic (LTL) is a fragment of first-order logic.
LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977.
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:
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, in order 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
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:
w ⊨ p if p ∈ w(0)
w ⊨ ¬ if w ⊭
w ⊨ ∨ if w ⊨ or w ⊨
w ⊨ X if w1 ⊨ (in the next time step must be true)
w ⊨ U if there exists i ≥ 0 such that wi ⊨ and for all 0 ≤ k < i, wk ⊨ ( must remain true until becomes true)
We say an ω-word w satisfies an LTL formula when w ⊨ .
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.