Okay, let's also give an answer to this open question: Translating E[Fφ∧Gψ] to µ-calculus with the mentioned technique can be done as follows for state formulas φ and ψ:
y
= E[Fφ∧Gψ]
= E[(φ∨XFφ)∧ψ∧XGψ]
= E[φ∧ψ∧XGψ ∨ ψ∧XFφ∧XGψ]
= φ∧ψ∧EXEGψ ∨ ψ∧EXE[Fφ∧Gψ]
= φ∧EGψ ∨ ψ∧EXE[Fφ∧Gψ]
= φ∧EGψ ∨ ψ∧EXy
Thus, y is a fixpoint of f(y) := φ∧EGψ ∨ ψ∧EXy, and in particular, it is the least fixpoint, i.e., E[Fφ∧Gψ] = µy.(φ∧EGψ ∨ ψ∧EXy). We may write that also in pure µ-calculus: E[Fφ∧Gψ] = µy.(φ∧(nu x.ψ∧<>x) ∨ ψ∧<>y) as well as in CTL E[ψ SU (φ∧EGψ)].
The translation of EG[φ∧XXφ] can be simplified, since G[φ∧XXφ] is equivalent to Gφ, so that EG[φ∧XXφ] = EGφ = nu z.φ∧EXz. Using the above technique will also work for state formulas φ:
y
= EG[φ∧XXφ]
= E(φ∧XXφ∧XG[φ∧XXφ])
= E(φ∧XXφ∧XG[φ∧XXφ])
= φ∧EXE(Xφ∧G[φ∧XXφ])
= φ∧EXz
It remains to translate E(Xφ∧G[φ∧XXφ]) to µ-calculus:
z
= E(Xφ∧G[φ∧XXφ])
= E(Xφ∧φ∧XXφ∧XG[φ∧XXφ])
= E(φ∧X(φ∧Xφ∧G[φ∧XXφ]))
= φ∧EX(φ∧z))
So, we get z = nu z.φ∧EX(φ∧z), and therefore EG[φ∧XXφ] = φ∧EX(nu z.φ∧EX(φ∧z))).
Finally, consider EG[φ∨XXφ] for state formulas φ:
y
= EG[φ∨XXφ]
= E[(φ∨XXφ) ∧ XG[φ∨XXφ] ]
= E[φ∧XG[φ∨XXφ] ∨ XXφ∧XG[φ∨XXφ]]
= E[φ∧XG[φ∨XXφ] ∨ X(Xφ∧G[φ∨XXφ])]
= φ∧EXEG[φ∨XXφ] ∨ EX(Xφ∧G[φ∨XXφ])
= φ∧EXy ∨ EXz
and the translation of z = E(Xφ∧G[φ∨XXφ]) is done as follows:
z
= E(Xφ∧G[φ∨XXφ])
= E(Xφ∧(φ∨XXφ)∧XG[φ∨XXφ])
= E(Xφ∧φ∧XG[φ∨XXφ] ∨ Xφ∧XXφ∧XG[φ∨XXφ])
= E(φ∧X(φ∧G[φ∨XXφ]) ∨ X(φ∧Xφ∧G[φ∨XXφ]))
= φ∧EX(φ∧EG[φ∨XXφ]) ∨ EX(φ∧z))
= φ∧EX(φ∧y) ∨ EX(φ∧z))
So that we conclude that EG[φ∨XXφ] = nu y. φ∧EXy ∨ EX(nu z. φ∧EX(φ∧y) ∨ EX(φ∧z))).
As said, this is a general translation technique, which usually makes a bigger effort than having a closer look at the formulas. Usually, formulas can be rewritten at first (like in the second example above) which can simplify the translation a lot. Think twice before going too deep in one direction.