[DOUBT] Translation of formula to Mu-calculus

Question

While looking at paper solutions to translate formulas to Mu-calculus, I observed the (nu y. <>y) -> part is considered in the answers provided in the paper dated 27.08.2019 (indicated in the left image).

However, in 31.08.2021 (right image), we omit the  (nu y. <>y) -> part because of the implies.

Is it an accepted answer in the exam if we solve it either way? Thanks in advance.

Answer 1

Formally, the Phi_Inf formula is required in the µ-calculus formulas, but one can also do without if the results are corrected afterwards in that the finally deadend states are added to all A-formulas and are removed from all E-formulas. In the example solutions we are therefore a bit sloppy with this formula. To be save, please add Phi-inf, or explain where it should be added if not written there explicitly.

Comments

Thanks for the clarification.