Équivalence de trace vs équivalence LTL

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?

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$

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 > $L_{even} =$$(EVEN)$$c \in L_{even}$$c_i = a$$i$$n$$p^i\neg p p^\omega$$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$

Ses traces sont précisément .$\{a,\neg a\}^\omega - L_{even}$

Corollaire au lemme: Si alors E V E N ⊭ ¬ $NOTEVEN \vDash \phi$$EVEN \not\vDash \neg\phi$

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

Ses traces sont clairement .$\{a,\neg a\}^\omega$

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.$NOTEVEN$$TOTAL$$\phi$$NOTEVEN \vDash \phi$$TOTAL \not\vDash \phi$$EVEN\vDash \neg\phi$

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

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 mais$A$$B$$b$$B$$b$$A$$B$$A$$A \not= B$$b$$A$ 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éfinir$b$$A$$A$$B$

et B = A ∖ { w } où w est par exemple le mot infini a b a 2 b 2 a 3 b 3 a 4 b 4 ⋯ .$A = \{a,b\}^\omega$$B = A \setminus \{w\}$$w$$aba^2b^2a^3b^3a^4b^4\cdots$

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 $A$$B$$B$$A$$B$$A$$\varphi$$B$$w$$w$$\neg\varphi$$w$$w$comme tout automate Buchi qui n'accepte qu'un seul mot infini doit être strictement cyclique alors que ne l'est pas.$w$