ctl - CTL 等价检查

Question

我被告知以下 CTL 公式不等价。但是，我找不到一个模型是正确的，而另一个不是。CTL 是一种计算时间逻辑。

公式 1： AF p OR AF q
公式 2： AF( p OR q )

第一个说：对于从开始状态开始的所有路径，都有一个 p 成立的未来，或者对于从开始状态开始的所有路径，都有一个 q 成立的未来。

第二：对于从开始状态开始的所有路径，都有一个 p OR q 成立的未来。

Answer 1

该模型有点棘手。首先，应该注意AF(p OR q)意味着AF p OR AF q。因此，我们正在寻找一个模型，其中AF (p OR q)为真，但AF p OR AF q为假。

我假设您熟悉 M. Huth 和 M. Ryan 在计算机科学教科书中的 Logic 中描述的 Kripke 模型符号（参见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 处成立。然而，在 s0 处不满足AF p OR AF q 。为了证明这一点，我们必须证明s0 不满足 AF p *和* s0 不满足 AF q。

AF p在 s0 不满足，因为我们可以选择路径 s0 -> s2 -> s2 -> s2 -> ...

同样，AF q在 s1 不满足，因为我们可以选择路径 s0 -> s1 -> s1 -> s1 -> ...