检查等效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) ? 

第一公式:等效

第二个公式:等效

第三个公式:等值

是对的吗？如果是错的，你能给我一个可能的反例在克里普克模型吗？

提前谢谢。

Answer 1

我将尝试使用这里定义的CTL的语义：维基百科。

(I)证明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 .没有p出现的地方。AF(q)不成立，因为有序列S0 S1 .没有Q出现的地方。

为了(III)：有乐趣地证明它，也许使用上面使用的技术:)