World Library  
Flag as Inappropriate
Email this Article

Linear temporal logic

Article Id: WHEBN0000710307
Reproduction Date:

Title: Linear temporal logic  
Author: World Heritage Encyclopedia
Language: English
Subject: Computation tree logic, Temporal logic, Generalized Büchi automaton, Temporal logic in finite-state verification, Modal logic
Collection: 1977 Works, Temporal Logic
Publisher: World Heritage Encyclopedia
Publication
Date:
 

Linear temporal logic

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. Subsequently LTL is sometimes called propositional temporal logic, abbreviated PTL.[3] Linear temporal logic (LTL) is a fragment of S1S.

LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977.[4]

Contents

  • Syntax 1
  • Semantics 2
  • Equivalences 3
  • Negation normal form 4
  • Relations with other logics 5
  • Applications 6
  • See also 7
  • References 8

Syntax

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 a LTL formula;
  • if ψ and φ are LTL formulas then ¬ψ, φ ∨ ψ, X ψ, and φ U ψ are LTL formulas.[5]

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 eventually (in the future)
  • R for release
  • W for weakly until

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 (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 \vDash between a word and an LTL formula is defined as follows:

  • w \vDash p if p ∈ w(0)
  • w \vDash ¬ψ if w \nvDash ψ
  • w \vDash φ ∨ ψ if w \vDash φ or w \vDash ψ
  • w \vDash X ψ if w1 \vDash ψ (in the next time step ψ must be true)
  • w \vDash φ U ψ if there exists i ≥ 0 such that wi \vDash ψ and for all 0 ≤ k < i, wk \vDash φ (φ must remain true until ψ becomes true)

We say an ω-word w satisfies LTL formula ψ when w \vDash ψ. The ω-language L(ψ) defined by ψ is {w | w \vDash ψ}, which is the set of ω-words that satisfy ψ. A formula ψ is satisfiable if there exist a ω-word w such that w \vDash ψ. A formula ψ is valid if for each ω-word w over alphabet 2AP, w \vDash ψ.

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 once φ becomes true. φ may never become true)
  • F ψ ≡ true U ψ (eventually ψ becomes true)
  • G ψ ≡ false R ψ ≡ ¬F ¬ψ (ψ always remains true)
Weak until

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).[6] 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 semantics for the temporal operators are pictorially presented as follows.

Textual Symbolic† Explanation Diagram
Unary operators:
X \phi \bigcirc \phi neXt: \phi has to hold at the next state. LTL next operator
G \phi \Box \phi Globally: \phi has to hold on the entire subsequent path. LTL always operator
F \phi \Diamond \phi Finally: \phi eventually has to hold (somewhere on the subsequent path). LTL eventually operator
Binary operators:
\psi U \phi \psi\mathcal{U}\phi Until: \psi has to hold at least until \phi, which holds at the current or a future position. LTL until operator
\psi R \phi \psi\mathcal{R}\phi Release: \phi has to be true until and including the point where \psi first becomes true; if \psi never becomes true, \phi must remain true forever. LTL release operator (which stops)

LTL release operator (which does not stop)

†The symbols are used in the literature to denote these operators.

Equivalences

Let Φ, ψ, and ρ be LTL formulas. The following tables list some of the useful equivalences which extend standard equivalences among the usual logical operators.

Distributivity
X (Φ ∨ ψ) ≡ (X Φ) ∨ (X ψ) X (Φ ∧ ψ)≡ (X Φ) ∧ (X ψ) XU ψ)≡ (X Φ) U (X ψ)
F (Φ ∨ ψ) ≡ (F Φ) ∨ (F ψ) G (Φ ∧ ψ)≡ (G Φ) ∧ (G ψ)
ρ U (Φ ∨ ψ) ≡ (ρ U Φ) ∨ (ρ U ψ) (Φ ∧ ψ) U ρ ≡ (Φ U ρ) ∧ (ψ U ρ)
Negation propagation
¬X Φ ≡ X ¬Φ ¬G Φ ≡ F ¬Φ ¬F Φ ≡ G ¬Φ
¬ (Φ U ψ) ≡ (¬Φ R ¬ψ) ¬ (Φ R ψ) ≡ (¬Φ U ¬ψ)
Special Temporal properties
F Φ ≡ F F Φ G Φ ≡ G G Φ Φ U ψ ≡ Φ UU ψ)
Φ U ψ ≡ ψ ∨ ( Φ ∧ XU ψ) ) Φ W ψ ≡ ψ ∨ ( Φ ∧ XW ψ) ) Φ R ψ ≡ ψ ∧ (Φ ∨ XR ψ) )
G Φ ≡ Φ ∧ X(G Φ) F Φ ≡ Φ ∨ X(F Φ)

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[<]—a result known as Kamp's theorem[7] or equivalently star-free languages.[8]

Computation tree logic (CTL) and Linear temporal logic (LTL) are both a subset of CTL*, but are not equivalent to each other. 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 formula AG( p → (EXq ∧ EX¬q) ).

However, a subset of CTL* exists that is a proper subset of both CTL and LTL.

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 that is equivalent to the model and another one that is equivalent to the negation of the property (cf. Linear temporal logic to Büchi automaton). The intersection of the two non-deterministic Büchi automata is empty if the model satisfies the property.[9]

Expressing important properties in formal verification

There are two main types of properties that can be expressed using linear temporal logic: safety properties usually state that something bad never happens (G\neg\phi), while liveness properties state that something good keeps happening (GF\psi or G(\phi \rightarrowF\psi)). 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 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.

See also

References

  1. ^ Logic in Computer Science: Modelling and Reasoning about Systems: page 175
  2. ^ Linear-time Temporal Logic
  3. ^  
  4. ^ Amir Pnueli, The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46–57. doi:10.1109/SFCS.1977.32
  5. ^ Sec. 5.1 of Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press [1]
  6. ^ Sec. 5.1.5 "Weak Until, Release, and Positive Normal Form" of Principles of Model Checking.
  7. ^ "Automata, Languages and Programming: 37th International Colloquium, ICALP ... - Google Books". Books.google.com. 2010-06-30. Retrieved 2014-07-30. 
  8. ^ Moshe Y. Vardi (2008). "From   preprint
  9. ^ 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.
External links
  • A presentation of LTL
  • Linear-Time Temporal Logic and Büchi Automata
  • LTL Teaching slides of professor Alessandro Artale at the Free University of Bozen-Bolzano
  • LTL to Buchi translation algorithms a genealogy, from the website of Spot a library for model-checking.
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
 
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
 
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.
 


Copyright © World Library Foundation. All rights reserved. eBooks from Project Gutenberg are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.