Question

how is s2 an unreachable state when there are incoming edges to it?

Answer 1

s2 is a reachable state in the Kripke structure, the the state s2 in the FSM is not reachable.

Comments

Is that so? s3 is {q,a} an initial state, and the self-loop of the FSM-state s1 {q} induces a transition to s2 {q}. As s2 {q} is a deadend, we delete it from the initial states. On the final graph, transition s3→s2 is no more

---

Yes, finally the transition s3->s2 is gone. But first, the state s2 exists and as an initial state, it is reachable by definition (since reachable states are mu x. (Init or <:>x) which includes the initial states). Hence, s2 of the Kripke structure is reachable. But we want to clean up the structure by removing all finite paths, and because of this, the state s2 is removed. It is a (reachable) deadend state.