Ê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 GraphSearch.
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.
Publications associées (1)
Concepts associés (10)
Vérification de modèles
thumb|308x308px|Principe du model checking. En informatique, la vérification de modèles, ou model checking en anglais, est le problème suivant : vérifier si le modèle d'un système (souvent informatique ou électronique) satisfait une propriété. Par exemple, on souhaite vérifier qu'un programme ne se bloque pas, qu'une variable n'est jamais nulle, etc. Généralement, la propriété est écrite dans un langage, souvent en logique temporelle. La vérification est généralement faite de manière automatique.
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.
Computation tree logic
Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized. It is used in formal verification of software or hardware artifacts, typically by software applications known as model checkers, which determine if a given artifact possesses safety or liveness properties. For example, CTL can specify that when some initial condition is satisfied (e.
Cours associés (3)
CS-550: Formal verification
We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u
PHYS-101(f): General physics : mechanics
Le but du cours de physique générale est de donner à l'étudiant les notions de base nécessaires à la compréhension des phénomènes physiques. L'objectif est atteint lorsque l'étudiant est capable de pr
MATH-105(a): Advanced analysis II
Etudier les concepts fondamentaux d'analyse et le calcul différentiel et intégral des fonctions réelles de plusieurs variables.
Séances de cours associées (32)
Protocoles : Description officielle et types de séances
Couvre les protocoles, les descriptions officielles avec les types de session, les types de message et la logique linéaire.
Stratégie gagnante en Java
Couvre la mise en œuvre d'une stratégie gagnante en Java.
ODEs linéaires de deuxième ordre
Couvre la solution des ODE linéaires de second ordre avec des coefficients constants et explore la méthode de variation des paramètres.