Translation to mu-calculus

Question

The question 9b, from 2018 Feb 14th exam, asks to translate E F X ([b SU a]).
The solution says:

(0) E F X ([b SU a])

(1) = E X F ([b SU a]) 

(2) = E X E F (E[b SU a])

      // E[b SU a] = µx.(φinf ∧ a) ∨ b ∧ <>x

(3) = <>(µy.((E [b SU a] = µx.a ∨ b ∧ <>x) ∨ <>y))

1) I was not able to find the equivalences E F X φ = E X F φ and E X F φ = E X E F (Eφ), how are they created?
2) How is performed the translation from (2) to (3)?

Thanks!

Answer 1

• E F X φ = E X F φ: both sides just mean that φ need to happen at one point at one path but not at the first point in time
• E X F [φ1 SU φ2] = E X E F (E[φ1 SU φ2]): The three quantifiers (X, F, SU) happen strictly after each other. Hence, there is no difference whether we take one path where there three things happen in exactly this order or whether we take a path to the first event, then from there to the second, and then from there to the third. Note that this doesn't if multiple quantifiers talk about the same points in time (e.g. EGF a is different from EGEF a)
• The last step is not printed in an correct way. It should look like: <>(µy.((E [b SU a] ) ∨ <>y))= <>(µy.(( µx.a ∨ b ∧ <>x) ∨ <>y)). We basically just take the formula from the comment above this step and add first the µ-Formula for EF and then an outer <> for EX.