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 は上記の 3 つの公式を検証し、すべてが真であることが判明しました。

では、私の質問は、なぜ式 2 と式 3 が真になるのかということです。