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 (next en anglais) et U est lu comme jusqu'à (until 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 (globally en anglais)) ;
• F pour finalement (dans le futur (in the future en anglais)) ;
• R pour libération (release en anglais) ;
• W pour faible jusqu'à (weak until 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 = a₀,a₁,a₂,... tel un mot-ω. Soit w(i) = a_i. Soit wⁱ = a_i,a_i+1,..., qui est un suffixe de w. Formellement, la relation de satisfaction $\vDash$ entre un mot et une formule de LTL est définie comme suit :

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

On dit qu'un mot-ω w satisfait une formule LTL ψ quand w $\vDash$ ψ.

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 :

Opérateur	Symbole alternatif	Explication	Diagramme
Opérateurs unaires :
X $\phi$	$\bigcirc \phi$	suivant (neXt) : $\phi$ doit être satisfaite dans l'état suivant.
G $\phi$	$\Box \phi$	Globalement : $\phi$ doit être satisfaite dans l'intégralité des états futurs.
F $\phi$	$\Diamond \phi$	Finalement : $\phi$ doit être satisfaite dans un état futur.
Opérateurs binaires:
$\psi$ U $\phi$	$\psi \;{\mathcal {U}}\,\phi$	Jusqu'à (Until) : $\psi$ doit être satisfaite dans tous les états jusqu'à un état où $\phi$ est satisfaite, non inclus.
$\psi$ R $\phi$	$\psi \;{\mathcal {R}}\,\phi$	Réaliser : $\phi$ doit être satisfaite dans tous les états tant que $\psi$ n'est pas satisfaite. Si $\psi$ n'est jamais satisfaite, $\phi$ doit être vraie partout.

Équivalences

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

Distributivité
X (Φ ∨ ψ) ≡ (X Φ) ∨ (X ψ)	X (Φ ∧ ψ)≡ (X Φ) ∧ (X ψ)	X (Φ U ψ)≡ (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 ψ ≡ Φ U (Φ U ψ)
Φ U ψ ≡ ψ ∨ ( Φ ∧ X(Φ U ψ) )	Φ W ψ ≡ ψ ∨ ( Φ ∧ X(Φ W ψ) )	Φ R ψ ≡ ψ ∧ (Φ ∨ X(Φ R ψ) )
G Φ ≡ Φ ∧ X(G Φ)	F Φ ≡ Φ ∨ X(F Φ)

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 $\exists p,\forall q,G(p\leftrightarrow Xq)$ 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

Références

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Linear temporal logic » (voir la liste des auteurs).

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