Équivalence de trace vs équivalence LTL

17

Je cherche un exemple simple de deux systèmes de transition qui sont équivalents LTL, mais pas équivalents trace.

J'ai lu la preuve que l'équivalence de trace est plus fine que l'équivalence LTL dans le livre "Principles of Model Checking" (Baier / Katoen) mais je ne suis pas sûr de bien la comprendre. Je ne peux pas l'imaginer, y a-t-il peut-être un exemple simple qui peut visualiser la différence?

magnétique
la source
3
Puis-je recommander d'élargir l'acronyme dans le titre. Cela aidera les autres à trouver la question et les réponses et pourrait également aider à porter votre question à l'attention de ceux qui peuvent fournir de bonnes réponses.
Marc Hamann
1
sans parler des recherches google :)
Suresh Venkat
5
@Marc: L'utilisation de l'acronyme LTL est absolument standard - les logiciens modaux aiment leurs noms brefs (pensez B, D4.3, KL, etc.). Je pense que le titre ne devrait pas être développé, étant donné que nous avons le tag.
Charles Stewart
1
La question n'est pas encore très bien définie: autorisez-vous des structures Kripke infinies? Considérez-vous les traces mixtes (maximales) finies et infinies, ou autorisez-vous uniquement les traces infinies? Je pose la question parce que l'AFAICR Baier & Katoen ne considère que le cas des structures Kripke finies et des traces infinies, ce qui exclut la réponse de Dave ci-dessous.
Sylvain
1
@atticae: avec des structures Kripke totales finies (et donc des traces infinies), je m'attendrais à ce que l'équivalence LTL et l'équivalence de trace soient la même chose ... J'y penserai.
Sylvain

Réponses:

9

En lisant attentivement Baier et Katoen, ils envisagent des systèmes de transition finis et infinis. Voir page 20 de ce livre pour les définitions.

Tout d'abord, prenons le système de transition simple :EVEN

MÊME

Lemme: Aucune formule LTL ne reconnaît le langage Traces ( E V E N ) . Une chaîne c L e v e n si siff c i = a pour même i . Voir Wolper '81 . Vous pouvez le prouver en montrant d'abord qu'aucune formule LTL avec n opérateurs "la prochaine fois" ne peut distinguer les chaînes de la forme p i ¬ p p ω pour i > nLeven=(EVEN)cLevenci=ainpi¬ppωi>n, par une simple induction.

Considérons le système suivant de transition (infini, non-déterministe) . Notez qu'il existe deux états initiaux différents:NOTEVEN

entrez la description de l'image ici

Ses traces sont précisément .{a,¬a}ωLeven

Corollaire au lemme: Si alors E V E N ¬ ϕNOTEVENϕEVEN¬ϕ

Maintenant, considérons ce système de transition simple :TOTAL

Total TS

Ses traces sont clairement .{a,¬a}ω

Ainsi, et T O T A L ne sont pas des traces équivalentes. Supposons qu'ils soient LTL inéquivalents. Nous aurions alors une formule LTL ϕ telle que N O T E V E N ϕ et T O T A L ϕ . Mais alors, E V E N ¬ ϕ . C'est une contradiction.NOTEVENTOTALϕNOTEVENϕTOTALϕEVEN¬ϕ

Merci à Sylvain d'avoir attrapé un bug stupide dans la première version de cette réponse.

Mark Reitblatt
la source
Hmm, ce n'est pas parfaitement clair. Dois-je rendre les étapes autour de la contradiction plus explicites? Les systèmes de transition ne sont pas aussi jolis qu'ils pourraient l'être ...
Mark Reitblatt
Vous interprétez mal le langage : le système que vous proposez est équivalent à la formule a G ( ( a X ¬ a ) ( ¬ a X a ) ) . Le système correct doit avoir un choix non déterministes au départ, un état marqué au q 0 entre aller à un état q 1 marqué par une et une q 2 non marqué par un . Les deux q 1 etLevenaG((aX¬a)(¬aXa))aq0q1aq2aq1 ont des transitions revenant à q 0 . q2q0
Sylvain
@Sylvain tu as raison. J'ai essayé de simplifier et j'ai fini par le casser! Laissez-moi arranger ça.
Mark Reitblatt
Ne pouvez-vous pas "inverser" l'argument, de sorte que les deux systèmes que vous comparez à la fin soient et T O T A L au lieu de N O T E V E N et T O T A L ? EVENTOTALNOTEVENTOTAL
Sylvain
1
@Mark Reitblatt: De quoi justifiez-vous cette phrase à la fin "Mais alors, ."? Je ne vois pas d'argumentation qui mène à ce point, qui est essentiel pour montrer la contradiction. EVEN¬ϕ
magnétique
3

Si votre définition LTL inclut l'opérateur "suivant", alors ce qui suit s'applique. Vous avez deux séries de traces et B . Que b soit préfixe fini d'une trace dans B . b doit également être un préfixe fini d'une trace dans A , car sinon vous pouvez le convertir en une formule qui n'est qu'une série d'opérateurs suivants qui détecte la différence. Par conséquent, chaque préfixe fini d'un mot B doit être un préfixe fini d'un mot A et vice versa. Cela signifie que si A B , il doit y avoir un mot en b pour que tous ses préfixes finis apparaissent dans A maisABbBbABAABbA en ellemême ne figure pas dans A . Si A et B sont générés pardessystèmes de transitionfinis, je pense que cela est impossible. En supposant des systèmes de transition infinis, vous pouvez définirbAAB

et B = A { w } w est par exemple le mot infini a b a 2 b 2 a 3 b 3 a 4 b 4 .A={a,b}ωB=A{w}waba2b2a3b3a4b4

Toute formule de LTL qui détient universellement pour tiendra universellement pour B parce que B est un sous - ensemble de A . Toute formule LTL valable pour B vaut également pour A ; pour des raisons de contradiction, ne supposez pas, mais que φ est valable pour chaque élément de B (c'est-à-dire pour chaque élément de l'univers, attendez-vous au mot w ) mais pas pour w . Alors ¬ φ est évalué comme vrai sur w mais pas sur aucun autre mot de l'univers (et LTL est fermé sous négation), et il n'y a pas de formule LTL qui ne peut être vraie que pour wABBABAφBww¬φwwcomme tout automate Buchi qui n'accepte qu'un seul mot infini doit être strictement cyclique alors que ne l'est pas.w

antti.huima
la source
Ce sont des traces finies. En supposant que vous les étendez à des traces infinies avec à la fin, la formule ¬ ( b X ( b X G a ) ) accepte le deuxième ensemble mais rejette le premier. aω¬(bX(bXGa))
Mark Reitblatt
Vous avez raison, j'ai écrit une nouvelle réponse :) LOL, je me suis souvenu de mes jours en cs théorique que LTL n'avait pas le prochain opérateur :)
antti.huima
Je pense que cela fait l'affaire.
Dave Clarke
Je pense que ça marche aussi.
Mark Reitblatt
Cette réponse n'est pas satisfaisante. L'OP demandait des systèmes de transition, mais la réponse concerne les langues et se justifie en termes d'automates Buchi et de langues -régulières, qui ne sont pas dans le texte référencé. ω
Mark Reitblatt