Model Checking CTL and µ-Calculus

Question

Please could someone explain in exam 2018.08.21 question 5.e:

how is it computed [|inf -> a|] = {s0;s1;s5;s6;s7}?

Thanks in advance.

Answer 1

We got the following

• [| a |] = {s1;s5;s6;s7}
• [| inf |] = [| nu y.<>y |] = {s1;s2;s3;s4;s5;s6;s7}
• [| !inf |] = {s0}
• [| inf->a |] = [| !inf | a |] = {s0;s1;s5;s6;s7}