You are wondering how the states satisfying E[b SB a] are computed. To that end, you first have to check the fixpoint formulation of this CTL formula which is µZ.(!a & (phioo & b | <>Z)). It is based on the recursion E[b SB a] = !a & (b | EXE[b SB a]) where phioo means states having infinite outgoing paths.

Every state of the structure has an outgoing transition, so all states have an outgoing infinite path, and phi00 = {s0;s1;s2;s3;s4;s5;s6;s7}. Now, let's first compute the states of E[b SB a] by µ-calculus by our model checker:

computing states of E[b SB a], i.e., µZ.(!a & (phioo & b | <>Z))

〖a〗= {s0;s2;s4;s6}
〖!a〗= {s1;s3;s5;s7}
〖b〗= {s0;s1;s3;s5;s7}
〖phioo & b〗=〖b〗= {s0;s1;s3;s5;s7}
step 0 : Z = {} (this is X0 in the example solution)
〖Z〗= {}
〖<>Z〗 = {}
〖phioo & b | <>Z〗 = {s0;s1;s3;s5;s7}
〖!a & (phioo & b | <>Z)〗 = {s1;s3;s5;s7}
step 1 : Z = {s1;s3;s5;s7} (this is X1 in the example solution)
〖Z〗= {s1;s3;s5;s7}
〖<>Z〗 = {s0;s1;s2;s3;s4;s5;s7}
〖phioo & b | <>Z〗 = {s0;s1;s2;s3;s4;s5;s7}
〖!a & (phioo & b | <>Z)〗 = {s1;s3;s5;s7}
fixpoint reached -->〖Z〗= {s1;s3;s5;s7} (this is X2 in the example solution)

Now, I understand you want to do that less formal, and more comprehensively, which is great!

So, E[b SB a] means all states having an outgoing path where b holds before a holds, and b must eventually hold. In particular, this is true in the states where b&!a holds (just b as you said it not sufficient!), i.e., {s1;s3;s5;s7}. These states are found by the model checker in step 0.

From these states, we work `backwards', i.e., add existential predecessors that satisfy !a&!b as long as new ones are added. This is done in step 1: Existential predecessors of {s1;s3;s5;s7} are {s0;s1;s2;s3;s4;s5;s7} but none of them satisfies !a&!b, so no new states are added and we already got our fixpoint as {s1;s3;s5;s7}.

Remarks:

- The fixpoint calculation in µ-calculus is a bit different, since it starts with Z={}, but the next step is where you would really want to start.
- µZ.(!a & (phioo & b | <>Z)) can be rewritten to µZ.(!a & b & phioo | !a & !b & <>Z)) so that you can see that we start with !a & b & phioo and continue adding existential predecessors that satisfy !a & !b.