Эквивалентность трассировки и эквивалентность LTL

Я ищу простой пример двух систем перехода, которые эквивалентны LTL, но не эквивалентны трассе.

Я прочитал доказательство того, что Эквивалентность трассировки является более тонкой, чем Эквивалентность LTL, в книге «Принципы проверки моделей» (Baier / Katoen), но я не уверен, что действительно понимаю ее. Я не могу изобразить это, может быть, есть простой пример, который может визуализировать разницу?

Внимательно читая Байера и Катоена, они рассматривают как конечные, так и бесконечные переходные системы. См. Страницу 20 этой книги для определений.

Сначала возьмем простую систему переходов :$EVEN$

Лемма: ни одна формула LTL не распознает язык Traces ( E V E N ) . Строка c ∈ L e v e n тогда и только тогда, когда c i = a для четного i . Смотри Wolper '81 . Вы можете доказать это, сначала показав, что никакая формула LTL с n операторами «в следующий раз» не может различить строки вида p i ¬ p p ω при i > $L_{even} =$$(EVEN)$$c \in L_{even}$$c_i = a$$i$$n$$p^i\neg p p^\omega$$i> n$, по простой индукции.

Рассмотрим следующий (бесконечное, недетерминированное) перехода системы . Обратите внимание, что есть два разных начальных состояния:$NOTEVEN$

Его следы точно .$\{a,\neg a\}^\omega - L_{even}$

Следствие из леммы: если то E V E N ⊭ ¬ $NOTEVEN \vDash \phi$$EVEN \not\vDash \neg\phi$

Теперь рассмотрим эту простую систему переходов :$TOTAL$

Его следы явно .$\{a,\neg a\}^\omega$

Таким образом, и T O T A $NOTEVEN$$TOTAL$ не являются следовыми эквивалентами. Предположим, они были неэквивалентными в литах. Тогда у нас будет формула LTL такая, что N O T E V E N ⊨ ϕ и T O T A L ⊭ ϕ . Но тогда E V E N ⊨ ¬ ϕ . Это противоречие.$\phi$$NOTEVEN \vDash \phi$$TOTAL \not\vDash \phi$$EVEN\vDash \neg\phi$

Спасибо Сильвену за обнаружение глупой ошибки в первой версии этого ответа.

Если ваше определение LTL включает в себя оператор «следующий», то применяется следующее. У вас есть два набора следов и B . Пусть б любой конечный префикс следа в B . $A$$B$$b$$B$$b$ также должен быть конечным префиксом трассы в , потому что в противном случае вы можете преобразовать его в формулу, представляющую собой просто последовательность операторов next, которая обнаруживает разницу. Поэтому каждый конечный префикс B- слова должен быть конечным префиксом A- слова и наоборот. Это означает, что если A ≠ B , в b должно быть слово, чтобы все его конечные префиксы появлялись в A, но$A$$B$$A$$A \not= B$$b$$A$ сама по себе не появляется в A . Если A и B порождаютсяконечнымипереходными системами, я думаю, что это невозможно. Предполагая бесконечные переходные системы, вы можете определить$b$$A$$A$$B$

и B = A ∖ { w }, где w , например, бесконечное слово$A = \{a,b\}^\omega$$B = A \setminus \{w\}$$w$ .$aba^2b^2a^3b^3a^4b^4\cdots$

Любая формула LTL , что имеет место универсальна для будет держать универсальна для B , потому что В является подмножество А . Любая формула LTL, которая верна для B, верна и для A ; ради противоречия предположим, что нет, но что $A$$B$$B$$A$$B$$A$$\varphi$ выполняется для каждого элемента из (т. е. для каждого элемента во вселенной ожидается слово w ), но не для w . Тогда ¬ φ оценивается как истинное на w, но не на любом другом слове вселенной (и LTL закрыт при отрицании), и нет формулы LTL, которая может быть истинной только для $B$$w$$w$$\neg\varphi$$w$$w$так как каждый автомат Бучи, который принимает только одно бесконечное слово, должен быть строго циклическим, тогда как - нет.$w$