The formula µZ.(b | !a & [] Z) is equivalent to A[!a SU b] and holds in states s2;s3;s5;s6;s7;s8 which you can easily check by considering the paths leaving the states.
The answers to your questions are as follows:
1. To check whether S4 |- []Z holds, we have to check whether Z holds on all successor states of S4, i.e., on states S0 and S7. Since Z represents the entire formula µZ.(b | !a & [] Z), i.e., A[!a SU b], it does not hold on state S0, but it does hold on state S7. If we would first check whether Z holds on state S7, we would have to produce the proof tree for this, and would find out that S7 satisfies Z, so that we still have to check whether it also holds on S4. Since it does not hold on S4, it is better to check this first, since Z does not hold on S4, and therefore, there is no need to check for S7 anymore. Knowing that Z does not hold on S4, i.e., one of the successors of S0, is sufficient to conclude that S4 |- []Z does not hold.
2. As explained above, there is no need to check whether Z holds on S7 after we found out that it does not hold on S4. The latter is sufficient to conclude that S4 |- []Z does not hold. If you would have checked first whether S7 satisfies Z, you would still have to check whether it also holds on S4.
3. Whether a fixpoint is a least or greatest one does not matter for the choice of initial states, nor does it matter much for the proof tree construction. It matters only if we encounter a loop in which case the greatest fixpoint holds, but the least one does not hold.
