So, you have the following FSM with state variables p,q and input variable a:

I = !q
R = a&p&!q&next(p)&next(q) |
a&q&next(p)&next(q) |
a&!p&!q&!next(p)&!next(q)

which leads to the following Kripke structure:

There are the following deadend states: p&q&!a | p&!q&!a | !p&q&!a | !p&!q&!a; note that one of them satisfies the initial condition. This formula can be simplified to !a, so that a transition relation that does not have transitions to deadend states would be

R' = R & next(a)

which yields as expected the following transitions

In the same way you can eliminate the transition from s3 (an unreachable state).