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) |
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).