At first, we compute the omega-automaton which has the following transition relation:
(q0 <-> b | a & next(q0)) & (q1 <-> !b & (!a | next(q1)))
As the automaton has the initial states !(q0|q1), i.e., !q0&!q1, we compute the transitions of the initial state as follows:
!q0&!q1 & (q0 <-> b | a & next(q0)) & (q1 <-> !b & (!a | next(q1)))
which is simplified as shown in the solutions using propositional logic laws to the following formula
!q0&!q1&a&!b&!next(q0)&!next(q1)
This means that from state !q0&!q1, there is only a transition to the same state with input a&!b. In the associated Kripke structure, the states are labeled with q0,q1,a,b and it therefore has the transitions listed in the solution which means that the above formula states that there are only transitions from state {a} to anyone of the states {a},{b},{},{a,b} so that there is only one infinite path starting in the initial state which is looping on state {a}.
