Still, defining the reachable states as (1) initial states, and (2) existential successor states of reachable states, we should have s0,s1,s4,s5,s6,s7 as reachable states (of the structure you find in my answer).

For reactive systems, we ignore finite paths, and that is a reason to clean up structures in that all finite paths are removed. However, that is another question independent of which states are reachable at first. We should therefore ask rather which states are reachable after removing finite paths.

I would define reachable states as mu y. (Init | <:>y) and the "cleaned up reachable states" as (mu y. (Init | <:>y)) & (nu z.<>z). That would give us

States(mu y. (Init | <:>y)) = {s0;s1;s4;s5;s6;s7}

States(nu z.<>z) = {s1;s3;s5;s7}

States((mu y. (Init | <:>y)) & (nu z.<>z)) = {s1;s5;s7}