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

第一个公式：等效

第二个公式：等价

第三个公式：等价

这样对吗？如果错了，你能给我一个 Kripke 模型中可能的反例吗？

提前致谢。

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)

所以等价是有效的。

---

(二)

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

假设具有三个状态 S0、S1、S2 的 Kripke 结构，设 S0 为初始状态。在 S0 中都不p nor q成立，在 S1 中仅p成立，在 S2 中仅q成立。

过渡是：

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

S1 形成 SCC，S2 形成 SCC。AF(p or q) 适用于这个 Kripke 结构，因为 (p 或 q) 适用于除 S0 之外的所有状态，最终每个序列都到达 S1 或 S2。AF(p) 或 AF(q) 呢？AF(p) 不成立，因为存在序列 S0 S2 S2 S2 ... 其中没有 p 出现。AF(q) 不成立，因为有序列 S0 S1 S1 S1 ... 没有出现 q。

对于（III）：玩得开心证明它，也许用上面使用的技术:)