For G[a WU b], we may simply apply the standard translation to LTL (pages 83-83), but we may also skip the GF-constraints for positive occurrences of weak and negative occurrences of strong temporal operators (page 94). In our case, both operators are weak and have positive occurrences, so that no GF-constraints are generated.
G[a WU b]
= AE({p},true,p<->b|a&Xp,Gp)
= AE({p,q},true,(p<->b|a&Xp)&(q<->p&Xq),q)
= AE({p,q},q,(p<->b|a&Xp)&(q<->p&Xq),true)
What is different to the lecture slides? Maybe I don't get what you mean?
Remark: It has already been pointed out that we may already take AE({p},true,p<->b|a&Xp,Gp) as a two-state safety automaton as the result.
