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

Question

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

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

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

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

Answer 1

Модель немного сложна. Во-первых, следует отметить, что AF (p OR q) означает AF p OR AF q. Итак, мы ищем модель, в которой AF (p OR q) имеет значение true, но 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 OR AF q не выполняется при s0. Чтобы доказать это, мы должны показать, что s0 не удовлетворяетAF р * и * s0 не удовлетворяетAF д.

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

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