CTL等值检验

Question

有人告诉我，以下CTL公式是不等价的。然而，我找不到一个模型，其中一个是真实的，另一个不是，CTL是一个计算时间逻辑。

公式1：AF p OR AF q

公式2：AF( p OR q )

第一个说法是:对于从开始状态开始的所有路径，都有一个p保持的未来；对于从开始状态开始的所有路径，都有一个Q保持的未来。

第二:对于从开始状态开始的所有路径，都有一个p或q保持的未来。

Answer 1

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

我假设您熟悉M. Huth和M. Ryan在“计算机科学教科书中的逻辑”(见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或q)在s0持有。然而，AF p或AF q对s0不满意。为了证明这一点，我们必须证明s0不满足AF p *和* s0不满足AF q。

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

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