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

17

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

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

magnattic
источник
3
Могу ли я порекомендовать расширить акроним в названии. Это поможет другим найти вопрос и ответы, а также поможет донести ваш вопрос до тех, кто может дать хорошие ответы.
Марк Хаманн
1
не говоря уже о поиске в Google :)
Суреш Венкат
5
@Marc: Использование аббревиатуры LTL абсолютно стандартно - модальные логики любят их краткие имена (например, B, D4.3, KL и т. Д.). Я думаю, что заголовок не должен быть расширен, учитывая, что у нас есть тег.
Чарльз Стюарт
1
Вопрос все еще не очень хорошо определен: вы допускаете бесконечные структуры Крипке? Вы рассматриваете смешанные (максимальные) конечные и бесконечные следы или допускаете только бесконечные? Я спрашиваю, потому что AFAICR Baier & Katoen рассматривают только случай конечных структур Крипке и бесконечных следов, которые исключают ответ Дейва ниже.
Сильвен
1
@atticae: с конечными полными структурами Крипке (и, следовательно, с бесконечными трассами), я ожидаю, что эквивалентность LTL и эквивалентность трасс будут одним и тем же ... Я подумаю об этом.
Сильвен

Ответы:

9

Внимательно читая Байера и Катоена, они рассматривают как конечные, так и бесконечные переходные системы. См. Страницу 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 > nLeven=(EVEN)cLevenci=ainпя¬ппωя>N, по простой индукции.

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

введите описание изображения здесь

Его следы точно .{a,¬a}ω-LеvеN

Следствие из леммы: если то E V E N ¬ ϕNОTЕВЕNφЕВЕN¬φ

Теперь рассмотрим эту простую систему переходов :TОTAL

Всего ТС

Его следы явно .{a,¬a}ω

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

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

Марк Рейтблатт
источник
Хм, это не совсем понятно. Должен ли я сделать шаги вокруг противоречия более явными? Системы перехода также не так хороши, как могли бы быть ...
Марк Рейтблатт
Вы неправильно интерпретируете язык: предлагаемая вами система эквивалентна формуле a G ( ( a X ¬ a ) ( ¬ a X a ) ) . У правильной системы должен быть недетерминированный выбор в начальном состоянии с меткой q 0 между переходом в состояние q 1, помеченное буквой a, и одним q 2, не помеченным буквой a . Оба q 1 иLevenaG((aX¬a)(¬aXa))aq0q1aq2aq1 имеет переходы, возвращающиеся к q 0 . q2q0
Сильвен
@ Сильвен, ты прав. Я попытался упростить, и я закончил тем, что сломал это! Позвольте мне исправить это.
Марк Рейтблатт
Разве вы не можете «перевернуть» аргумент, чтобы две системы, которые вы сравниваете в конце, были и T O T A L вместо N O T E V E N и T O T A L ? EVENTOTALNOTEVENTOTAL
Сильвен
1
@Mark Reitblatt: Из чего вы исходите из этого предложения в конце «Но тогда, .»? Я не могу видеть аргументацию, которая приводит к этому пункту, который необходим, чтобы показать противоречие. EVEN¬ϕ
Magnattic
3

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

и B = A { w }, где w , например, бесконечное словоA={a,b}ωB=A{w}w .aba2b2a3b3a4b4

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

antti.huima
источник
Это конечные следы. Предполагая , что вы расширить их бесконечные следы с в конце концов, формулу ¬ ( б X ( б X G ) )aω¬(bX(bXGa)) принимает второй сет , но отвергает первый.
Марк Рейтблатт
Вы правы, я написал новый ответ :) LOL, я вспомнил из своих дней в теоретической CS, что LTL не имеет следующего оператора :)
antti.huima
Я думаю, что это делает трюк.
Дейв Кларк,
Я думаю, что это тоже работает.
Марк Рейтблатт
Этот ответ не является удовлетворительным. ОП спрашивал о переходных системах, но ответ о языках и оправдан с точки зрения автоматов Бучи и ω регулярных языков, на которые нет ссылок в тексте.
Марк Рейтблатт