1

我想知道下面的 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)) 或 EG (not q)) 改写成有用但多次失败的东西。

我浏览了我的课程资料以及谷歌，但我找不到任何东西。但是，我确实在这里找到了另一个具有相同等价问题但没有答案的问题，因此我正在尝试进行第二次尝试。

4

1 回答 1

0

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

但是，由于这个问题被多次提出，我认为它仍然有用。

问题：A[p U A[q U r]]相当于A[A[p U q] U r]？

答案：没有。

为了证明不等式成立，提供单个Kripke 结构stA[p U A[q U r]]已验证但未验证（或相反）A[A[p U q] U r]就足够了。

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

让我们分解[p U [q U r]]：

  • [q U r]在匹配表达式的路径上为真{q}*{r}
  • [p U [q U r]]在马赫的路径上是真的{p}*{[q U r]} = {p}*{q}*{r}

怎么样[[p U q] U r]？

  • [p U q]在匹配表达式的路径上为真{p}*{q}
  • [[p U q] U r]在马赫的路径上是真的{[p U q]}*{r} = {{p}*{q}}*{r}

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

事实上，{p}*{q}*{r}匹配任何路径，其中有一个序列，p并且r没有q沿途。

然而，{{p}*{q}}*{r}没有。如果路径包含 的序列p，则qbefore的出现r是强制性的。

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

动手回答：

让我们使用NuSMV对提供相同反例的Kripke 结构进行编码

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

事实上，一个属性得到验证，而另一个没有。

于 2016-06-13T17:38:07.743 回答