model-checking - CTL 公式直到包含含义

Question

当我使用 NuSMV 工具验证我的 CTL 是否正确时，我遇到了一个让我很困惑的问题。

我的模型是

这是NuSMV代码：

MODULE main
VAR
  state : {ROOT, A1, B1, C1, D1, F1, M1};

ASSIGN
  init(state) := ROOT;

  next(state) := case
    state = ROOT : A1;
    state = A1   : {B1, C1};
    state = B1   : D1;
    state = D1   : F1;
    TRUE : state;
  esac;

CTLSPEC
  AG( state=A1 -> AX ( A [ state=B1 U ( state=D1 -> EX state=F1 ) ] ) );
CTLSPEC
  AG( state=A1 -> AX ( A [ state=B1 U ( state=F1 -> EX state=C1 ) ] ) );
CTLSPEC
  AG( state=A1 -> AX ( A [ state=M1 U ( state=F1 -> EX state=C1 ) ] ) );

我的 CTL 公式如下：

1. "AG( A1 -> AX ( A [ B1 U ( D1 -> EX ( F1) ) ] ) )"
2. "AG( A1 -> AX ( A [ B1 U ( F1 -> EX ( C1) ) ] ) )"
3. "AG( A1 -> AX ( A [ M1 U ( F1 -> EX ( C1) ) ] ) )"

NuSMV 验证了上述三个公式，所有这些都证明是正确的。

所以我的问题是，为什么公式 2 和公式 3 是正确的？

Answer 1

这个问题很老，但我认为它仍然值得回答，因为这个问题可能会误导其他人。

M, s ⊨ A[φUψ] iff 对于所有路径 (s, s2,s3, s4, ...) st si Rt si+1 存在状态 sj st M, sj ⊨ ψ 和 M, si ⊨ φ 对于所有我<j。

因此，对于要验证的属性，在ψ触发之前， φ必须为真。

请注意，如果ψ立即触发，则φ的值不相关。

---

很容易看出，所有三个公式都经过了简单的验证，因为ψ它true处于从B1和开始的每条路径的第一个状态C1。之所以如此，是因为ψ它是一个蕴涵，在B1和C1中，有一个false前提。

由于我们知道A [ ANYTHING U TRUE ]任何状态都可以验证，因此我们得出结论，所有三个属性都是可满足的。