Thanks for the clarification on the fact every state formula is also a path formula.

"States s2 has also one outgoing path where never b holds, but initially z does not hold on that path."

- Little confused, isn't s2 has an infinite path satisfying b?

"Finally, state s1 does satisfy the formula, since the path s0,s2,s2,... satisfies Fb and initially, we have z on that path, i.e., on s0 the variable z holds."

- Doesn't s0 satisfy the formula?