Quelle est la différence entre LTL et CTL?

12

J'ai déjà lu des exemples de formules dans CTL mais pas dans LTL et vice-versa, mais j'ai du mal à comprendre mentalement les formules LTL et vraiment quelle est, au fond, la différence.

Lâche anonyme
la source
1
Beaucoup de notes sur les interwebs traitent de ce problème. Avez googlé pour "la différence entre LTL et CTL"?
Dave Clarke
1
Essayez d'écrire des formules simples et d'évaluer leur sémantique sur les structures de Kripke.
Vijay D

Réponses:

21

Pour vraiment comprendre la différence entre LTL et CTL, vous devez étudier la sémantique des deux langues. Les formules LTL indiquent les propriétés qui seront interprétées à chaque exécution d'un programme. Pour chaque exécution possible (une exécution), qui peut être considérée comme une séquence d'événements ou d'états sur une ligne - et c'est pourquoi elle est appelée "temps linéaire" - la satisfiabilité est vérifiée lors de l'exécution sans possibilité de passer à une autre exécution lors de la vérification. D'un autre côté, la sémantique CTL vérifie une formule sur toutes les exécutions possibles et essaiera toutes les exécutions possibles ( opérateur A ) ou une seule exécution ( opérateur E ) lorsqu'elle fait face à une branche.

En pratique, cela signifie que certaines formules de chaque langue ne peuvent pas être énoncées dans l'autre langue. Par exemple, la propriété de réinitialisation (une propriété d'accessibilité importante pour la conception de circuits) indique qu'il est toujours possible qu'un état puisse être atteint pendant une analyse, même s'il n'est jamais réellement atteint ( réinitialisation AG EF ). LTL peut uniquement indiquer que l' état de réinitialisation est réellement atteint et non qu'il peut être atteint.

D'un autre côté, la formule LTL ne peut pas être traduite en CTL. Cette formule dénote la propriété de la stabilité: à chaque exécution du programme, s sera finalement vrai jusqu'à la fin du programme (ou pour toujours si le programme ne s'arrête jamais ). CTL ne peut fournir qu'une formule trop stricte ( AF AG ) ou trop permissive ( AF EG ). Le second est clairement faux. Ce n'est pas si simple pour le premier. Mais AF AG est erroné. Considérons un système qui boucle sur A1 , peut aller de A1 à B , puis ira à A2 au prochain mouvement. Ensuite, le système resterasÉtat A2 pour toujours. Alors "le système restera enfin dans un état A " est une propriété de type . Il est évident que cette propriété tient sur le système. Cependant, les AF AG ne peuvent pas capturer cette propriété car l'inverse est vrai: il y a une exécution dans laquelle le système sera toujours dans l'état à partir duquel une analyse passe finalement dans un état non A.s

Je ne sais pas si cela répond à votre question, mais j'aimerais ajouter quelques commentaires.

Il y a beaucoup de discussions sur la meilleure logique pour exprimer les propriétés de la vérification logicielle ... mais le vrai débat est ailleurs. Le LTL peut exprimer des propriétés importantes pour la modélisation de système logiciel (équité) lorsque le CTL doit avoir une nouvelle sémantique (une nouvelle relation de satisfiabilité) pour les exprimer. Mais les algorithmes CTL sont généralement plus efficaces et peuvent utiliser des algorithmes basés sur BDD. Donc ... il n'y a pas de meilleure solution. Jusqu'à présent, seulement deux approches différentes.

L'un des commentateurs suggère l'article de Vardi "Branching versus Linear Time: Final Showdown" .

Benoît Fraikin
la source
voir une discussion sur LTL vs CTL par Vardi: "Branching vs. Linear Time: Final Showdown"
Guy
merci beaucoup, c'est exactement le genre d'informations que je cherchais!
Coward anonyme
1

Si on donne un objet (par exemple trace en cas de LTL), vous ne considérez qu'un seul futur pour chaque point dans le temps, dans CTL vous en avez une pléthore.

En particulier, nextdonne une action unique en LTL mais (potentiellement) un ensemble complet en CTL.

Raphael
la source
6
Mais vous appliquez généralement la formule LTL à toutes les exécutions du système, plutôt qu'à une seule, réduisant ainsi l'écart entre le problème futur un / plusieurs. Il serait plus précis de dire que LTL traite du temps linéaire, alors que CTL traite du temps de branchement.
Dave Clarke
4
Dire, dans LTL, vous envisagez un avenir, c'est comme dire dans CTL que vous considérez un état. La satisfaction est définie de cette façon. Il ne s'agit pas du nombre de futurs, mais de la structure de l'avenir. Dans l'un, c'est une trace, dans l'autre, un arbre.
Vijay D
@Vijay - en effet, la structure est importante. Par exemple, vous ne pouvez pas simplement prendre une formule LTL, la transformer comme FGp -> AF AG p et obtenir une formule CTL équivalente (ces deux formules ne sont pas équivalentes; en outre, FGp n'est pas exprimable en CTL et AF AG p n'est pas exprimable en LTL ).
jkff
J'ai supposé que l'OP connaissait la définition formelle et demandait une sorte d'intuition, d'où mon essai. Cette réponse peut-elle être récupérée en disant "un avenir par modèle"?
Raphael
Je ne peux pas dire ce que le PO connaît. Par exemple, est-il clair pour eux ce qu'est un modèle dans chaque cas?
Vijay D