Translating AF(a & X a) to mu-calculus is indeed not that trivial. It was asked here because it appears in the lecture slides (Temporal Logic Chapter, slide 36-37). There, you also find how that is translated to mu-calculus, we just unwind the formulas until we find a fixpoint:
EG[φ∨Xφ]
= E[(φ∨Xφ)∧XG(φ∨Xφ)]
= E[(φ∧XG(φ∨Xφ))∨(Xφ∧XG(φ∨Xφ))]
= E[φ∧XG(φ∨Xφ)]∨E[Xφ∧XG(φ∨Xφ)]
= φ∧EXEG[φ∨Xφ]∨EX(φ∧EG[φ∨Xφ])
Replacing EG[φ∨Xφ] now with y yields a fixpoint equation y= φ∧EXy ∨ EX(φ∧y) which finally gives us the mu-calculus formula νy.(φ∧EXy ∨ EX(φ∧y)).
