For this formula, it is important to understand that if Fa holds at some point t1, then it also holds at any previous point t<=t1. If we have to make sure that Fa holds until b holds, then it must also hold at least right before the point of time where b holds. If b should hold already at the initial point of time, then that is also fine.
Hence, find that [F a SU b] <-> b | F((X b) & (F a)) is valid. Since we can express the WU by SU, we also get [F a WU b] <-> [F a SU b] | G F a, and thus, we have
[F a WU b] <-> b | F((X b) & (F a)) | G F a
We can still modify the formula a bit in that we replace F a with a | X F a and multiply out:
[F a WU b] <-> b | F(a & X b) | F X(b & F a) | G F a
Okay, what all that? Because now, we can drive in an outermost E-quantifier and will get the following formula:
E[F a WU b] <-> b | EF(a & EX b) | EF EX(b & EF a) | EGF a
This formula is almost a CTL* formula, it is just the expression EGFa which is not expressible in CTL. That it is sign that the entire formula may not be expressible in CTL, and indeed, this is the case: Note that for the special case of b=false, we get
E[F a WU false] <-> EGF a
and since EGFa cannot be expressed in CTL, it is also not possible to express E[F a WU b] (assuming that we could would lead to a contradiction).
Hence, the CTL formula given above must be definitely incorrect, since E[F a WU b] cannot be expressed in CTL.
That is different with a SU: Looking at the above transformations, we get
[F a SU b] <-> b | F(a & X b) | F X(b & F a)
and thus, we get the following CTL formula
E[F a SU b] <-> b | EF(a & EX b) | EF EX(b & EF a)
