Logique temporelle linéaire

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[5].

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).

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 ${\displaystyle \vDash }$ entre un mot et une formule de LTL est définie comme suit :

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

On dit qu'un mot-ω w satisfait une formule LTL ψ quand w ${\displaystyle \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[N 1]	Explication	Diagramme
Opérateurs unaires :
X ${\displaystyle \phi }$	${\displaystyle \bigcirc \phi }$	suivant (neXt) : ${\displaystyle \phi }$ doit être satisfaite dans l'état suivant.
G ${\displaystyle \phi }$	${\displaystyle \Box \phi }$	Globalement : ${\displaystyle \phi }$ doit être satisfaite dans l'intégralité des états futurs.
F ${\displaystyle \phi }$	${\displaystyle \Diamond \phi }$	Finalement : ${\displaystyle \phi }$ doit être satisfaite dans un état futur.
Opérateurs binaires:
${\displaystyle \psi }$ U ${\displaystyle \phi }$	${\displaystyle \psi \;{\mathcal {U}}\,\phi }$	Jusqu'à (Until) : ${\displaystyle \psi }$ doit être satisfaite dans tous les états jusqu'à un état où ${\displaystyle \phi }$ est satisfaite, non inclus.
${\displaystyle \psi }$ R ${\displaystyle \phi }$	${\displaystyle \psi \;{\mathcal {R}}\,\phi }$	Réaliser : ${\displaystyle \phi }$ doit être satisfaite dans tous les états tant que ${\displaystyle \psi }$ n'est pas satisfaite. Si ${\displaystyle \psi }$ n'est jamais satisfaite, ${\displaystyle \phi }$ doit être vraie partout.

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

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.

Toute formule LTL est équivalente à un automate de Büchi de taille au plus exponentielle en la taille de la formule[6]. 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[7].

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[8].

Les buts des agents sont parfois écrits en LTL, à la fois pour des approches avec modèles[9] - [10] ou sans[11] - [12] - [13].

• Logique linéaire
• Logique ternaire