Equivalência de Rastreio vs Equivalência de LTL

Estou procurando um exemplo fácil de dois sistemas de transição equivalentes a LTL, mas não equivalentes a traços.

Li a prova de que a Equivalência de traços é mais refinada do que a Equivalência de LTL no livro "Princípios de verificação de modelos" (Baier / Katoen), mas não tenho certeza se realmente entendi. Eu sou incapaz de imaginá-lo, talvez haja um exemplo simples que possa visualizar a diferença?

Lendo Baier e Katoen de perto, eles estão considerando sistemas de transição finitos e infinitos. Veja a página 20 desse livro para definições.

Primeiro, use o sistema de transição simples $EVEN$ :

Lema: Nenhuma fórmula LTL reconhece o idioma Traços ( E V E N ) . Uma string c ∈ L e v e n se s c i = a para i i . Veja Wolper '81 . Você pode provar isso mostrando primeiro que nenhuma fórmula LTL com n operadores "da próxima vez" pode distinguir as seqüências de caracteres da forma p i ¬ p p ω para i > $L_{even} =$$(EVEN)$$c \in L_{even}$$c_i = a$$i$$n$$p^i\neg p p^\omega$$i> n$, por uma simples indução.

Considere o seguinte (não-determinística infinito,) sistema de transição . Observe que existem dois estados iniciais diferentes:$NOTEVEN$

Seus traços são precisamente .$\{a,\neg a\}^\omega - L_{even}$

$NOTEVEN \vDash \phi$$EVEN \not\vDash \neg\phi$

Agora, considere este sistema de transição simples :$TOTAL$

Seus traços são claramente .$\{a,\neg a\}^\omega$

Portanto, e não são equivalentes ao rastreamento. Suponha que eles sejam LTL diferentes. Então teríamos uma fórmula LTL tal que e . Mas então, . Isso é uma contradição.T O T A G φ N S T E V E N ⊨ φ T S T A G ⊭ φ E V E N ⊨ ¬ $NOTEVEN$$TOTAL$$\phi$$NOTEVEN \vDash \phi$$TOTAL \not\vDash \phi$$EVEN\vDash \neg\phi$

Agradeço a Sylvain por capturar um bug estúpido na primeira versão desta resposta.

Se sua definição de LTL incluir o operador "next", o seguinte se aplicará. Você tem dois conjuntos de traços e . Deixe ser qualquer prefixo finito de um rastreio em . também deve ser um prefixo finito de um rastreio em , porque, caso contrário, você pode convertê-lo em uma fórmula que é apenas uma série de próximos operadores que detectam a diferença. Portanto, todo prefixo finito de uma palavra precisa ser um prefixo finito de uma palavra e vice-versa. Isso significa que, se , deve haver uma palavra em para que todos os seus prefixos finitos apareçam em mas$A$$B$$b$$B$$b$$A$$B$$A$$A \not= B$$b$$A$$b$em si não aparece em . Se e são gerados por sistemas de transição finitos , acho que isso é impossível. Assumindo sistemas de transição infinitos, você pode definir$A$$A$$B$

$A = \{a,b\}^\omega$ e onde é, por exemplo, a palavra infinita .$B = A \setminus \{w\}$$w$$aba^2b^2a^3b^3a^4b^4\cdots$

Qualquer fórmula LTL que detém universalmente para vai realizar universalmente para porque é um subconjunto de . Qualquer fórmula LTL que se aplica a também se aplica a ; por uma questão de contradição, não assuma, mas isso vale para todo elemento de (isto é, para todo elemento do universo que se espera pela palavra ), mas não para . Então avaliado como verdadeiro em mas não em qualquer outra palavra do universo (e LTL é fechado sob negação), e não existe uma fórmula LTL que possa ser verdadeira apenas para$A$$B$$B$$A$$B$$A$$\varphi$$B$$w$$w$$\neg\varphi$$w$$w$como todo autômato Buchi que aceita apenas uma palavra infinita deve ser estritamente cíclico, enquanto não é.$w$