Quelle est la différence entre LTL et CTL?

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.

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 restera$\Diamond\Box s$É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.$\Diamond\Box 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" .

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.