Logique temporelle linéaire

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

En logique, la logique temporelle linéaire[1],[2] (LTL) est une logique temporelle modale avec des modalités se référant au temps. En LTL, on peut coder des formules sur l'avenir de chaînes, par exemple, une condition finira par être vraie, une condition sera vraie jusqu'à ce qu'une autre devienne vraie, etc. Cette logique est une partie de la CTL* plus complexe, qui permet en outre de ramification temps et quantificateurs. LTL est aussi parfois appelée logique temporelle propositionnelle, abrégé LTP (PTL en anglais)[3]. La logique temporelle linéraire est (LTL) est une fragement de S1S.

LTL a d'abord été proposé pour la vérification formelle des programmes informatiques par Amir Pnueli en 1977[4].

Syntaxe[modifier | modifier le code]

La LTL est construite à partir d'un ensemble fini de variables propositionnelles APopérateurs logiques ¬ et ∨, et des opérateurs temporels modaux X (certaines notations utilisent O ou N) et U. Formellement, l'ensemble des formules de LTL sur AP est inductivement défini comme suit :

  • si p ∈ AP alors p une formule de LTL ;
  • si ψ et φ sont des formules de LTL alors ¬ψ, φ ∨ ψ, X ψ, et φ U ψ sont des formules de LTL.[5]

X est lu comme suivant (next en anglais) et U est lu comme jusqu'à (until en anglais). Autre que ces opérateurs fondamentaux, il existe des opérateurs logiques et temporels supplémentaires. Ces opérateurs sont ∧, →, ← →, vrai et faux. Ci-dessous sont les opérateurs temporels supplémentaires.

  • G pour toujours (globalement (globally en anglais))
  • F pour éventuellement (dans le futur (in the future en anglais))
  • R pour la réalisation (release en anglais)
  • W pour faible jusqu'à (weakly until en anglais)

Sémantique[modifier | modifier le code]

Une formule de LTL peut être satisfaite par une suite infinie d'évaluations de vérité des variables dans AP. Soit w = a0,a1,a2,... tel un mot-ω. Soit w(i) = ai. Soit wi = ai,ai+1,..., qui est un suffixe de w. Formellement, la relation de satisfaction entre un mot et une formule de LTL est définie comme suit:

  • w p si p ∈ w(0)
  • w ¬ψ si w ψ
  • w φ ∨ ψ si w φ ou w ψ
  • w X ψ si w1 ψ (ψ doit être vrai à l'étape suivante)
  • w φ U ψ s'il existe i ≥ 0 tel que wi ψ et pour tout 0 ≤ k < i, wk φ (φ doit rester vrai jusqu'à ce que ψ devienne vrai)

Nous disons qu'un mot-ω w satisfait une formule LTL ψ quand w ψ.

Les opérateurs logiques supplémentaires sont définis comme suit:

  • φ ∧ ψ ≡ ¬(¬φ ∨ ¬ψ)
  • φ → ψ ≡ ¬φ ∨ ψ
  • φ ↔ ψ ≡ (φ → ψ) ∧ ( ψ → φ)
  • vrai ≡ p ∨ ¬p, où p ∈ AP
  • faux ≡ ¬vrai

Les opérateurs temporels supplémentaires R, F et G sont définis comme suit:

  • φ R ψ ≡ ¬(¬φ U ¬ψ)
  • F ψ ≡ vrai U ψ (ψ devient éventuellement vrai)
  • G ψ ≡ faux R ψ ≡ ¬F ¬ψ (ψ reste toujours vrai)


La sémantique des opérateurs temporels sont picturalement présentés comme suit.

Text Symbolique† Explication Diagramme
Opérateurs unaires:
X suivant: doit tenir à l'état suivant. LTL next operator
G Globalement: doit tenir dans l'intégralité de l'état suivant. LTL always operator
F Finalement: doit éventuellement tenir (quelque part dans l'état suivant). LTL eventually operator
Opérateurs binaires:
U Jusqu'à:  doit détenir au moins jusqu'à ce que . LTL until operator
R Réaliser: doit être vrai jusqu'à et y compris le point où  devient vrai; si  ne devient jamais vrai, doit rester vrai pour toujours. LTL release operator (which stops)

LTL release operator (which does not stop)

†Les symboles suivants sont utilisés dans la littérature pour désigner ces opérateurs.

Équivalences[modifier | modifier le code]

Soit Φ, ψ, et ρ des formules de LTL. Les tableaux suivants présentent certaines des équivalences utiles.

Distributivité
X (Φ ∨ ψ) ≡ (X Φ) ∨ (X ψ) X (Φ ∧ ψ)≡ (X Φ) ∧ (X ψ) XU ψ)≡ (X Φ) U (X ψ)
F (Φ ∨ ψ) ≡ (F Φ) ∨ (F ψ) G (Φ ∧ ψ)≡ (G Φ) ∧ (G ψ)
ρ U (Φ ∨ ψ) ≡ (ρ U Φ) ∨ (ρ U ψ) (Φ ∧ ψ) U ρ ≡ (Φ U ρ) ∧ (ψ U ρ)
Négation
¬X Φ ≡ X ¬Φ ¬G Φ ≡ F ¬Φ ¬F Φ ≡ G ¬Φ
¬ (Φ U ψ) ≡ (¬Φ R ¬ψ) ¬ (Φ R ψ) ≡ (¬Φ U ¬ψ)
Propriétés temporelles spéciales
F Φ ≡ F F Φ G Φ ≡ G G Φ Φ U ψ ≡ Φ UU ψ)
Φ U ψ ≡ ψ ∨ ( Φ ∧ XU ψ) ) Φ W ψ ≡ ψ ∨ ( Φ ∧ XW ψ) ) Φ R ψ ≡ ψ ∧ (Φ ∨ XR ψ) )
G Φ ≡ Φ ∧ X(G Φ) F Φ ≡ Φ ∨ X(F Φ)

Forme normale négative[modifier | modifier le code]

Article détaillé : Forme normale négative.

Toutes les formules de LTL peuvent être transformées en forme normale négative, où

  • toutes les négations apparaissent seulement en face des propositions atomiques,
  • seuls les opérateurs logiques vrai, faux, ∧ et ∨ peuvent apparaître, et
  • seuls les opérateurs logiques X, U, et R peuvent apparaître.

Voir aussi[modifier | modifier le code]

Références[modifier | modifier le code]

  1. Logic in Computer Science: Modelling and Reasoning about Systems: page 175
  2. Linear-time Temporal Logic
  3. (en) Dov M. Gabbay, A. Kurucz, F. Wolter, M. Zakharyaschev, Many-dimensional modal logics: theory and applications, Elsevier, (ISBN 978-0-444-50826-3, lire en ligne), p. 46
  4. Amir Pnueli, The temporal logic of programs.
  5. Sec. 5.1 of Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press [1]
Liens externes