这个 CTL 公式是否等价，是什么让它成立？

Question

我想知道下面的 CTL 公式是否等价，如果等价，您能帮我说服自己吗？ A(p U ( A(q U r) )) = A(A(p U q) U r)

我想不出任何与之相矛盾的模型，我的直觉告诉我这些公式是等价的，但我找不到任何支持该陈述的等价物。我试图重写等价 A(p U q) == not(E ((not q) U not(p or q)) or EG (not q)) 变成有用但失败了几次的东西。

我已经查看了我的课程 material 以及 google，但我找不到任何东西。不过我确实找到了 another question here that has the same equivalence question but with no answer，所以我想再试一次。

Answer 1

注意：这个答案可能会迟到。

不过，既然提了这个问题multiple times，我觉得还是有用的。

问题：A[p U A[q U r]]是否等同于A[A[p U q] U r]？

回答：否。

要证明不等式成立，提供一个克里普克结构 s.t就足够了。 A[p U A[q U r]] 已验证，但 A[A[p U q] U r] 未（或相反）。

现在，为简单起见，我们假设处理克里普克结构，其中每个状态只有一个可能的未来状态。因此，我们可以忘记 A 修饰符并考虑给定问题的 LTL 版本： 是 [p U [q U r]] 等价于 [[p U q] U r]?。

我们来分解一下[p U [q U r]]:

[q U r] 在 paths 上是 true 匹配表达式 {q}*{r}
[p U [q U r]] true 在 paths 上 {p}*{[q U r]} = {p}*{q}*{r}

[[p U q] U r]呢？

[p U q] 在 paths 上是 true 匹配表达式 {p}*{q}
[[p U q] U r] 是 true 在 paths 上 {[p U q]}*{r} = {{p}*{q}}*{r}

现在，{p}*{q}*{r} != {{p}*{q}}*{r}.

事实上，{p}*{q}*{r}匹配任何路径，其中p的序列后跟r并且没有q一路走来

然而，{{p}*{q}}*{r} 没有。如果路径包含 p 序列，则必须在 r 之前出现 q。

因此，这两个公式不等价。

动手回答：

让我们编码一个 Kripke 结构，它使用 NuSMV[提供相同的反例

MODULE main ()
VAR
  p: boolean;
  q: boolean;
  r: boolean;

INVAR !q;

INIT
  !q & p & !r

TRANS
  r -> next(r);

TRANS
  p & !r -> next(r);

CTLSPEC A[p U A[q U r]];
CTLSPEC A[A[p U q] U r];

并检查它：

~$ NuSMV -int
NuSMV > reset; read_model -i test.smv; go; check_property
-- specification A [ p U A [ q U r ]  ]   is true
-- specification A [ A [ p U q ]  U r ]   is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample 
Trace Type: Counterexample 
-> State: 1.1 <-
  p = TRUE
  q = FALSE
  r = FALSE

确实，一个属性已验证，但另一个未验证。

这个 CTL 公式是否等价，是什么让它成立？

Is this CTL formula equivalent and what makes it hold?

logic

transitivity

ctl