Logique temporelle linéaire

En logique, la logique temporelle linéaire (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 d'un chemin infini dans un système de transitions, par exemple une condition finira par être vraie, une condition sera vraie jusqu'à ce qu'une autre devienne vraie, etc. Cette logique est plus faible que la logique CTL*, qui permet d'exprimer des conditions sur des ramifications de chemins et pas seulement sur un seul chemin. LTL est aussi parfois appelée logique temporelle propositionnelle, abrégé LTP (PTL en anglais). La logique temporelle linéraire (LTL) est un fragment de S1S (pour second-order with 1 successor), la logique monadique du second ordre avec un successeur.

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

Syntaxe 
La LTL est construite à partir d'un ensemble fini de variables propositionnelles AP, opé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 est une formule de LTL ;
 si ψ et φ sont des formules de LTL alors ¬ψ, φ ∨ ψ, X ψ, et φ U ψ sont des formules de LTL.
X est lu comme suivant ( en anglais) et U est lu comme jusqu'à ( en anglais). On peut ajouter d'autres opérateurs, non nécessaires mais qui simplifient l'écriture de certaines formules.

Par exemple, les opérateurs logiques ∧, →, ↔, vrai et faux sont généralement ajoutés. Les opérateurs temporels ci-dessous le sont également :

 G pour toujours (globalement ( en anglais)) ;
 F pour finalement (dans le futur ( en anglais)) ;
 R pour libération ( en anglais) ;
 W pour faible jusqu'à ( en anglais).

Sémantique 
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)

On dit 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 peut se représenter comme suit :

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

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.

Automates de Büchi 
Toute formule LTL est équivalente à un automate de Büchi de taille au plus exponentielle en la taille de la formule. Pour LTL sur les traces finies, appelée LTLf, toute formule est équivalente à un automate fini non déterministe de taille au plus exponentielle en la taille de la formule.

Problèmes algorithmiques 
Le model checking et le problème de satisfiabilité est PSPACE-complet. La synthèse LTL et le problème de vérification d'un jeu avec un objectif LTL sont 2EXPTIME-complet.

Apprentissage par renforcement 
Les buts des agents sont parfois écrits en LTL, à la fois pour des approches avec modèles ou sans.

Extensions

Quantification du second ordre 
Dans le chapitre 3 de sa thèse, Sistla étend LTL en rajoutant des quantifications du second ordre. À l'époque LTL se nommait plutôt PTL (pour propositional temporal logic). Cette extension s'appelle QPTL (quantified propositional temporal logic). Par exemple  est une formule de QPTL qui se lit "il existe une façon de donner des valeurs à la proposition p sur toute la ligne temporelle, telle que quelle que soit la façon d'attribuer les valeurs à la proposition q sur toute la ligne temporelle, on a toujours que p est équivalent au fait que demain q". Sistla, dans le chapitre 3 de sa thèse, démontre que décider si une formule sous forme prénexe et avec une seule alternation de QPTL est vraie est EXPSPACE-complet.

Comme mentionné par Sistla et al., on peut réduire S1S qui est non-élémentaire à QPTL. La véracité d'une formule de QPTL est donc non-élémentaire. Plus précisément, Sistla et al. démontrent que le problème de véracité de QPTL restreint aux formules avec k alternations est kNEXPSPACE-complet.

Voir aussi 
 Logique linéaire
 Logique ternaire

Notes et références

Notes

Références 

 Liens externes
 Une présentation de la LTL
 Linear-Time Temporal Logic and Büchi Automata
 LTL Teaching slides, Free University of Bozen-Bolzano
 LTL to Buchi translation algorithms, Spot

Logique modale
Logique temporelle