CTL Проверка эквивалентности

Question

Мне сказали, что следующие формулы CTL не эквивалентны. Тем не менее, я не могу найти модель, в которой одна верна, а другая нет. CTL - это вычислительная временная логика.

Формула 1: AF p OR AF q
Формула 2: AF( p OR q )

Первый говорит: для всех путей, начинающихся с начального состояния, существует будущее, в котором p содержит OR, для всех путей, начинающихся с начального состояния, существует будущее, в котором q сохраняется.

Второе: для всех путей, начинающихся с начального состояния, существует будущее, в котором выполняется p ИЛИ q.

Answer 1

Модель немного сложнее. Во-первых, следует отметить, что AF(p OR q) подразумевает AF p OR AF q. Итак, мы ищем модель, в которой AF(p OR q) истинно, но AF p OR AF q ложно.

Я предполагаю, что вы знакомы с нотацией модели Крипке, описанной в учебнике по логике в компьютерных науках М. Хутом и М. Райаном (см. http://www.cs.bham.ac.uk/research/projects/lics/).

Пусть M = (S, R, L) - модель с S = {s0, s1, s2} в качестве множества возможных состояний, R = {(s0,s1), (s0,s2), (s1,s1), (s1,s2), (s2,s2)} как отношение перехода, а L - функция маркировки, определенная следующим образом: L(s0) = {} (пустой набор), L(s1) = {p} и L(s2) = {q}.

Предположим, что начальное состояние s0. Ясно, что AF(p OR q) выполняется при s0. Однако AF p ИЛИ AF q не выполняется при s0. Чтобы доказать это, мы должны показать, что s0 не удовлетворяет AF p *и* s0 не удовлетворяет AF q.

AF p не выполняется в s0, так как мы можем выбрать путь s0 -> s2 -> s2 -> s2 -> ...

Точно так же AF q не выполняется в s1, так как мы можем выбрать путь s0 -> s1 -> s1 -> s1 -> ...