When we translate the formula [a SB (F b)] & PF[c WU a], we abbreviate its subformulas
q0 = F b // leaving [a SB q0] & PF[c WU a]
q1 = [a SB q0] // leaving q1 & PF[c WU a]
q2 = [c WU a] // leaving q1 & PF q2
q3 = PF q2 // leaving q1 & (q2|q3)
Remark: The abbreviations are done by adding a part to the transistion relation and adding a fairness constraint to the acceptance condition (see page 83 ff of the chapter on temporal logic). For the abbreviation of the formula PF q2, which is a past temporal operator, consider page 84 of the chapter on temporal logic: PF q2 is initially false, so we have to add !q3 to the initial condition, and the transition relation we need to add is (Xq3 <-> q2|q3), leaving q2|q3.
The initial states are therefore !q3 & (q1 & (q2|q3)).
