Usually, the way to go is to translate a CTL* formula to CTL, and then the µ-calculus translation is straightforward. Alternatives are CTL^2, but let's not go into that, and of course, one can also directly translate CTL* to µ-calculus, but that is quite difficult.
So, let's consider the given formula AF[b SU (a&Xa)]. If we could duplicate the path quantifier, i.e., to obtain AFA[b SU (a&Xa)], we would be almost there. However, that is not equivalent, and therefore we cannot do this. Luckily, the LTL formula F[a SU b] means nothing else than Fb, since F[a SU b] means the following in LO1 (which is the semantics):
∃t0. 0≤t0 ∧ (∃t1. t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2<t1 → a[t2])) ∧ b[t1])
It means that there are t0 and t1 with t0≤t1 such that (1) ∀t2. (t0≤t2 ∧ t2<t1 → a[t2]) and (2) b[t1] holds. If such numbers exist, then we can also choose t0:=t1 which satisfies trivially (1). Hence, the above formula is equivalent to Fb.
So, we consider now the translation of the equivalent formula AF(a&Xa) to the µ-calculus. It may seem to be simple to translate this now to CTL, but it is not: At this point, you need to remember lecture slide 36 of the temporal logic chapter. While slide 35 proved that CTL can be translated to the alternation-free µ-calculus, slide 36 tells us that this inclusion is strict, since the formula AF(a&Xa) can be translated to the alternation-free µ-calculus, but not to CTL. Its equivalence to the given µ-calculus formula is proved also on slide 36.
