CTL fomula until contains implication

Question

when I use NuSMV tools to verify if my CTL is right, I encounter a problem that make me so confused.

My model is

and here's the NuSMV code:

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 ) ] ) );

My CTL formula is as follows:

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 verified the above three formulas all of which turns out to be true .

So my question is that why the formula 2 and formula 3 turn out to be true?

Answer 1

This question is old, but I think it's still worth an answer, as the issue might be misleading for other people.

M, s ⊨ A[ϕUψ] iff for all paths (s, s2,s3, s4, . ..) s.t. si Rt si+1 there is a state sj s.t. M, sj ⊨ ψ and M, si ⊨ ϕ for all i < j.

So, for the property to be verified, ϕ must be true up until when ψ fires.

Notice that if ψ fires immediately then the value of ϕ is not relevant.

---

It is easy to see that all three formulas are trivially verified because ψ is true in the first state of each path starting from B1 and C1. This is the case because ψ is an implication which, in states B1 and C1, has a false premise.

Since we know that A [ ANYTHING U TRUE ] is verified for any state, we conclude that all three properties are satisfiable.