Проверьте эквивалентные формулы CTL

Question

Я делаю упражнение CTL, я пытаюсь проверить, эквивалентны ли следующие формулы или нет. Но я не уверен, правильно ли я поступаю.

EF (p or q) = EF(p) or EF(q) ? 
AF(p or q) = AF(p) or AF(q) ? 
A(p U ( A(q U r) )) = A(A(p U q) U r) ? 

Формула Firt: Эквивалент

Вторая формула: эквивалент

Третья формула: эквивалент

Это правильно? Если вы не правы, не могли бы вы привести один из возможных контрпримеров в модели Крипке?

Заранее спасибо.

Answer 1

Я попытаюсь использовать семантику CTL, определенную здесь: Википедия о CTL.

(Я) Для доказательства EF (p or q) = EF(p) or EF(q):

(M, s1) |= EF (p or q)*

<=> (Def. of EF)

There is s1->s2->... such that there is an i >= 1 such that (M, s_i) |= (p or q)

<=> (Def. of or)

There is s1->s2->... such that is an i >= 1 such that ((M, s_i) |= p OR ((M, s_i) |= q)

<=> (Equivalence rules for predicate logic)


(There is s1->s2->... such that is an i >= 1 such that ((M, s_i) |= p)
 OR 
(There is s1->s2->... such that is an i >= 1 such that ((M, s_i) |= q)

<=> (Def. of EF)

EF(p) or EF(q)

Таким образом, эквивалентность действительна.

---

(II),

AF(p or q) = AF(p) or AF(q)

Предположим структуру Крипке с тремя состояниями S0, S1, S2, пусть S0 будет начальным состоянием. В S0 нет p nor q держит, только в S1 p держит, только в S2 q держит.

Переходы:

S0 -> S1
S0 -> S2
S1 -> S1
S2 -> S2

S1 образует SCC, а S2 образует SCC. AF(p или q) выполняется для этой структуры Крипке, поскольку (p или q) выполняется для ВСЕХ состояний, кроме S0, и в конечном итоге каждая последовательность достигает S1 или S2. А как насчет AF (p) или AF(q)? AF(p) НЕ выполняется, поскольку существует последовательность S0 S2 S2 S2 ..., где p не появляется. AF (q) не выполняется, поскольку существует последовательность S0 S1 S1 S1 ..., где q не появляется.

Для (III): весело проведите время, доказывая это, возможно с методами, использованными выше:)