Since there is only one outgoing transition in every state, we may add a A in front of each temporal operator and consider this way the CTL formulas A [(A F a) SB (A X a)] and A F (a & !A X a) instead. This way, we can conveniently use the model checker to verify the example. However, note that these formulas are in general not equivalent, but on the considered structure they are!

We then get the following:

〖A X a〗 = {s1;s2}

〖!A X a〗= {s0}

〖a & !A X a〗= {}

〖A F (a & !A X a)〗 = {}

〖A X a〗 = {s1;s2}

〖A F a〗 = {s0;s1;s2}

〖A [(A F a) SB (A X a)]〗 = {s0}

So, the only path s0->s1->s2->... satisfies [(F a) SB (X a)] but not F(a & !X a) which distinguishes the two formulas.

Comments on the discussion above: Of course, you can use in the state transition diagrams also variables that do not occur in the formula. However, this has no effect on the evaluation of the formulas and thus, you can also safely ignore them.

If you consider the structure {a}->{c}->{} with a self loop on the final state {}, you get no difference on the formulas since then both formulas are satisfied: F a is true initially, X a is not, and thus (Fa) SB (X a) is satisfied initially, and since a & !Xa holds initially also, we also have F(a & !X a).