Lets consider a new operator $B$ where $a B b$ means "in every execution, if $b$ holds some time, then $a$ does so before it" and we're asked to define it in CTL.
My working: the system can only fail if $b$ holds. If $b$ doesn't hold, we're in the clear - so one possible path could be $(¬ □ b)$. The only other path that could hold is one where $a$ happens before $b$, so $(a$ $U$ $b)$ is another path. Overall we're left with $∀((a U b) ∨ (¬ □ b))$. For every path either $a$ happens before $b$ OR $b$ never happens.
Is the way I reasoned about this question correct? Are there any holes in my logic that I should re-consider? Please reply as a comment if possible, and many thanks in advance for any input.