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?