Mu Calculus - clarification

Question

If we are supposed to convert The CTL Formula to Mu calculus, I see that in few solution papers, infinity (phi_inf -> newx.<>x)) is ignored. In some other papers, infinity is not ignored. Are either of the methods acceptable?

Answer 1

To be precise the formula for the infinite paths is required. If the Kripke structure does not have deadend states, it is trivially true, and can therefore be omitted. Otherwise, you may also omit it in that you fix the mistakes made by the "wrong µ-calculus" formulas manually. The results just differ by the deadend states.

Comments

Thank you for the clarification.

---

However I need one clarification here with your answer, the infinity needs to be used for 2 different questions i) CTL Model checking - where Kripke Structure is provided(Here we can identify the deadends as the Kripke Structure is given in the exam) ii) In Translation Logic, while converting the "formula to Mew calculus", we are using infinity for certain types like EFphi, AGphi etc. In translation logic questions we wont be provided with a Kripke structure in the exam, so how we do identify the deadends? Are you saying that for both type of questions i and ii(i.e Translation logic and CTL model checking), we are suposed to use Infinity to be on the safe side?