Эквивалентна ли эта формула CTL и что ее поддерживает?

Question

Мне интересно, эквивалентны ли приведенные ниже формулы CTL, и если да, то можете ли вы помочь мне убедить себя, что это так? A(p U ( A(q U r))) = A(A(p U q) U r)

Я не могу придумать какие-либо модели, которые противоречат этому, и мои внутренности говорят мне, что формулы эквивалентны, но я не могу найти никаких эквивалентов, которые поддерживают это утверждение. Я пытался переписать эквивалентность A(p U q) == не (E ((не q) U не (p или q)) или EG (не q)) во что-то полезное, но потерпел неудачу несколько раз.

Я просмотрел материалы своего курса, а также Google, но ничего не могу найти. Однако я нашел здесь другой вопрос с таким же вопросом об эквивалентности, но без ответа, поэтому я пытаюсь сделать вторую попытку.

Answer 1

Примечание: этот ответ может быть поздно.

Однако, так как вопрос поднимался много раз, я думаю, что он все еще полезен.

---

Вопрос: есть A[p U A[q U r]] эквивалентно A[A[p U q] U r]?

---

Ответ: нет.

Чтобы доказать, что неравенство стоит, достаточно предоставить одну структуру Крипке A[p U A[q U r]] проверено, но A[A[p U q] U r] нет (или наоборот).

Теперь для простоты мы предполагаем иметь дело со структурой Крипке, в которой каждое состояние имеет только одно возможное будущее состояние. Поэтому мы можем забыть о A Модификатор и рассмотрим LTL- версию данной задачи: есть [p U [q U r]] эквивалентно [[p U q] U r] ?,

Давай сломаться [p U [q U r]]:

• [q U r] верно для путей, которые соответствуют выражению {q}*{r}
• [p U [q U r]] верно на пути, которые Mach {p}*{[q U r]} = {p}*{q}*{r}

Как насчет [[p U q] U r]?

• [p U q] верно для путей, которые соответствуют выражению {p}*{q}
• [[p U q] U r] верно на пути, которые Mach {[p U q]}*{r} = {{p}*{q}}*{r}

Сейчас, {p}*{q}*{r} != {{p}*{q}}*{r},

По факту, {p}*{q}*{r} соответствует любому пути, в котором последовательность p сопровождается r и нет q по пути.

Тем не мение, {{p}*{q}}*{r} не. Если путь содержит последовательность p то возникновение q до r является обязательным.

Таким образом, две формулы не эквивалентны.

---

Практический ответ:

Давайте закодируем структуру Крипке, которая предоставляет тот же контрпример, используя NuSMV

MODULE main ()
VAR
  p: boolean;
  q: boolean;
  r: boolean;

INVAR !q;

INIT
  !q & p & !r

TRANS
  r -> next(r);

TRANS
  p & !r -> next(r);

CTLSPEC A[p U A[q U r]];
CTLSPEC A[A[p U q] U r];

и проверь это:

~$ NuSMV -int
NuSMV > reset; read_model -i test.smv; go; check_property
-- specification A [ p U A [ q U r ]  ]   is true
-- specification A [ A [ p U q ]  U r ]   is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  p = TRUE
  q = FALSE
  r = FALSE

Действительно, одно свойство проверено, а другое нет.