logique temporelle linéaire

LTL est construit à partir de l'ensemble des variables propositionnelles AP , des opérateurs logiques ¬ et ∨, et des opérateurs modaux temporels X (certains ouvrages utilisent O ou N ) et U. Formellement, l'ensemble des formules LTL sur AP est défini inductivement comme suit :

• si alors p est une formule LTL ;
• si sont des formules LTL alors et sont des formules LTL.

X se lit « ne x t » et U se lit « u ntil ». Outre ces opérateurs fondamentaux, des opérateurs logiques et temporels supplémentaires, définis à partir des opérateurs fondamentaux, permettent d'écrire des formules LTL de manière concise. Les opérateurs logiques supplémentaires sont : ∧, →, ↔, vrai et faux . Voici les opérateurs temporels supplémentaires.

• G pour toujours ( g globalement)
• F pour finalement​
• R pour publication​
• W pour faible jusqu'à
• M pour m puissante libération

La grammaire hors contexte de LTL est la suivante : ::= ⊤ | ⊥ | p | (¬ φ ) | ( φ ∧ φ ) | ( φ ∨ φ ) | ( φ → φ ) | ( Xφ ) | ( G φ ) | ( F φ ) | ( φ U φ ) | ( φ W φ ) | ( φ R φ ) | ( φ M φ )

Une formule LTL peut être satisfaite par une séquence infinie de valeurs de vérité des variables de AP . Ces séquences peuvent être vues comme un mot sur un chemin d'une structure de Kripke (un ω-mot sur l'alphabet 2 ^AP ). Soit _w = a₀ _, a₁ _, a₂ _, ... un tel ω-mot. Soit w ( i ) = aᵢ _. Soit wᵢ = aᵢ _, aᵢ₊₁ _, ^{... ,} qui est un suffixe de w . Formellement, la relation de satisfaction ⊨ entre un mot et une formule LTL est définie comme suit :

• w ⊨ p si p ∈ w (0)
• w ⊨ ¬ w ⊭ w ⊨ w ⊨ w ⊨ si w ¹ ⊨ suivante , s'il existe i ≥ 0 tel que w ⁱ ⊨ k < i, w ^k ⊨ ( doit rester vrai jusqu'à ce queOn dit qu'un ω-mot w satisfait une formule LTL w ⊨ ω-langage L ( w | w ⊨ satisfiable s'il existe un ω-mot w tel que w ⊨ valide si, pour tout ω-mot w sur l'alphabet 2AP ^, on a 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 ¬ r libère (finalementG faux R F ¬

    Faible jusqu'à une forte libération

    Certains auteurs définissent également un opérateur binaire « until faible » , noté W , dont la sémantique est similaire à celle de l’opérateur « until », mais la condition d’arrêt n’est pas requise (similaire à la libération). Il est parfois utile car U et R peuvent tous deux être définis à l’aide de l’opérateur « until faible ».

    L' opérateur binaire de libération forte , noté M , est le dual de l'opérateur faible « jusqu'à ». Il est défini de manière similaire à l'opérateur « jusqu'à », de sorte que la condition de libération doit être vérifiée à un moment donné. Par conséquent, il est plus fort que l'opérateur de libération.

    La sémantique des opérateurs temporels est présentée graphiquement comme suit.

Soient φ, ψ et ρ des formules LTL. Les tableaux suivants répertorient certaines équivalences utiles qui étendent les équivalences standard entre les opérateurs logiques usuels.

Toutes les formules de LTL peuvent être transformées en forme normale négative , où

• Toutes les négations n'apparaissent que devant les propositions atomiques.
• Seuls les opérateurs logiques vrai , faux , ∧ et ∨ peuvent apparaître, et
• seuls les opérateurs temporels X , U et R peuvent apparaître.

En utilisant les équivalences ci-dessus pour la propagation de la négation, il est possible d'obtenir la forme normale. Cette forme normale permet l'apparition de R , vrai , faux et ∧ dans la formule, qui ne sont pas des opérateurs fondamentaux de LTL. Notons que la transformation vers la forme normale de négation n'augmente pas la longueur de la formule. Cette forme normale est utile pour la traduction d'une formule LTL vers un automate de Büchi .

On peut montrer que LTL est équivalent à la logique monadique du premier ordre d'ordre , FO[<] — un résultat connu sous le nom langages sans étoile .

La logique arborescente de calcul (CTL) et la logique temporelle linéaire (LTL) sont toutes deux des sous-ensembles de la CTL* , mais sont incomparables. Par exemple,

• Aucune formule dans CTL ne peut définir le langage défini par la formule LTL F ( G p).
• Aucune formule dans LTL ne peut définir le langage qui est défini par les formules CTL AG ( p → ( EX q ∧ EX ¬q) ) ou AG ( EF (p)).

La vérification de modèles et la satisfaisabilité par rapport à une formule LTL sont des problèmes PSPACE-complets . La synthèse LTL et le problème de la vérification des jeux par rapport à une condition gagnante LTL sont 2EXPTIME-complets .

Vérification de modèles de logique temporelle linéaire par automates

Les formules LTL sont couramment utilisées pour exprimer les contraintes, les spécifications ou les processus qu'un système doit suivre. Le domaine de la vérification de modèles vise à vérifier formellement si un système satisfait à une spécification donnée. Dans le cas de la vérification de modèles par automates, le système étudié et la spécification sont exprimés sous forme de machines à états finis (ou automates) distinctes, puis comparés afin d'évaluer si le système garantit la propriété spécifiée. En informatique, ce type de vérification de modèles est souvent utilisé pour vérifier la structure correcte d'un algorithme.

Pour vérifier les spécifications LTL lors d'exécutions infinies du système, une technique courante consiste à obtenir un automate de Büchi équivalent au modèle (qui accepte un ω-mot si et seulement si c'est le modèle) et un autre équivalent à la négation de la propriété (qui accepte un ω-mot si et seulement si il satisfait la propriété niée) (cf. Logique temporelle linéaire vers automate de Büchi ). Dans ce cas, s'il y a chevauchement dans l'ensemble des ω-mots acceptés par les deux automates, cela implique que le modèle accepte certains comportements qui violent la propriété souhaitée. S'il n'y a pas de chevauchement, aucun comportement violant la propriété n'est accepté par le modèle. Formellement, l'intersection des deux automates de Büchi non déterministes est vide si et seulement si le modèle satisfait la propriété spécifiée.

Exprimer les propriétés importantes dans la vérification formelle

Deux principaux types de propriétés peuvent être exprimés à l'aide de la logique temporelle linéaire : les propriétés de sûreté stipulent généralement qu'un événement indésirable ne se produit jamais ( G ¬ϕ ) , tandis que les propriétés de vivacité stipulent qu'un événement bénéfique se produit continuellement ( GF ψ ou G ( ϕ → F ψ )). Par exemple, une propriété de sûreté peut exiger qu'un rover autonome ne tombe jamais d'une falaise, ou qu'un logiciel n'autorise jamais une connexion réussie avec un mot de passe incorrect. Une propriété de vivacité peut exiger que le rover continue toujours à collecter des échantillons de données, ou qu'un logiciel envoie régulièrement des données de télémétrie.

Plus généralement, les propriétés de sûreté sont celles pour lesquelles tout contre-exemple possède un préfixe fini tel que, même prolongé en un chemin infini, il demeure un contre-exemple. En revanche, pour les propriétés de vivacité, tout chemin fini peut être prolongé en un chemin infini satisfaisant la formule.

Langage de spécification

L'une des applications de la logique temporelle linéaire est la spécification des préférences dans le langage de définition du domaine de planification à des fins de planification basée sur les préférences .

La logique temporelle linéaire paramétrique étend la LTL avec des variables sur la modalité jusqu'à.