Trace Equivalence vs LTL Equivalence

Estoy buscando un ejemplo sencillo de dos sistemas de transición que sean equivalentes a LTL, pero que no sean equivalentes de rastreo.

He leído la prueba de que Trace Equivalence es más fina que LTL Equivalence en el libro "Principles of Model Checking" (Baier / Katoen) pero no estoy seguro de entenderlo realmente. No puedo imaginarlo, ¿hay algún ejemplo simple que pueda visualizar la diferencia?

Al leer a Baier y Katoen detenidamente, están considerando sistemas de transición finitos e infinitos. Vea la página 20 de ese libro para las definiciones.

Primero, tome el sistema de transición simple :$EVEN$

Lema: Ninguna fórmula LTL reconoce el lenguaje Traces . Una cadena iff para even . Ver Wolper '81 . Puede probar esto mostrando primero que ninguna fórmula LTL con operadores "la próxima vez" puede distinguir las cadenas de la forma para , por una simple inducción.( E V E N ) c ∈ L e v e n c i = a $L_{even} =$$(EVEN)$$c \in L_{even}$$c_i = a$$i$p i ¬ p p ω i > $n$$p^i\neg p p^\omega$$i> n$

Considere el siguiente sistema de transición (infinito, no determinista) . Tenga en cuenta que hay dos estados iniciales diferentes:$NOTEVEN$

Sus trazas son precisamente .$\{a,\neg a\}^\omega - L_{even}$

Corolario del lema: Si entoncesE V E N ⊭ ¬ $NOTEVEN \vDash \phi$$EVEN \not\vDash \neg\phi$

Ahora, considere este sistema de transición simple :$TOTAL$

Sus huellas son claramente .$\{a,\neg a\}^\omega$

Por lo tanto, y no son trazas equivalentes. Supongamos que fueran LTL no equivalentes. Entonces tendríamos una fórmula LTL tal que y . Pero entonces, . Esto es una contradicción.T O T A L ϕ N O T E V E N ⊨ ϕ T O T A L ⊭ ϕ E V E N ⊨ ¬ $NOTEVEN$$TOTAL$$\phi$$NOTEVEN \vDash \phi$$TOTAL \not\vDash \phi$$EVEN\vDash \neg\phi$

Gracias a Sylvain por atrapar un error estúpido en la primera versión de esta respuesta.

Si su definición LTL incluye el "siguiente" operador, se aplica lo siguiente. Tiene dos conjuntos de huellas y . Deje que sea cualquier prefijo finito de una huella en . también debe ser un prefijo finito de una traza en , porque de lo contrario puede convertir esto en una fórmula que es solo una serie de operadores siguientes que detectan la diferencia. Por lo tanto, cada prefijo finito de una palabra debe ser un prefijo finito de una palabra y viceversa. Esto significa que si , debe haber una palabra en para que todos sus prefijos finitos aparezcan en peroB b B b $A$$B$$b$$B$$b$$A$A A ≠ B b A $B$$A$$A \not= B$$b$$A$$b$en sí mismo no aparece en . Si y son generados por sistemas de transición finita , creo que esto es imposible. Suponiendo sistemas de transición infinita, puede definirA $A$$A$$B$

y B = A ∖ { w } donde w es, por ejemplo, la palabra infinita 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$

Cualquier fórmula LTL que mantiene universalmente para se mantenga universalmente para B porque B es un subconjunto de A . Cualquier fórmula LTL que sea válida para B también es válida para A ; en aras de la contradicción, suponga que no, pero que $A$$B$$B$$A$$B$$A$$\varphi$ vale para cada elemento de (es decir, para cada elemento del universo, espere la palabra w ) pero no para w . Entonces ¬ φ se evalúa como verdadero en w pero no en cualquier otra palabra del universo (y LTL está cerrado bajo negación), y no existe una fórmula LTL que pueda ser verdadera solo para $B$$w$$w$$\neg\varphi$$w$$w$como todo autómata Buchi que acepta solo una palabra infinita debe ser estrictamente cíclico mientras que no lo es.$w$