Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Logique temporelle linéaire
Résumé
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.
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).
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.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.