Mu calculus

Question

Dear all,

I am trying to get a better understanding of mu calculus and in order to do that I am using online tools. This is the example I tried:

When I solve it in the notebook, I get the fixpoint on {s1;s2;s8;s9}. But I am struggling to understand the tool solution, particularly at step 1 [ <> x ] why s0 and s4 is included (we see that they get removed during step 0) when clearly at step 1 [x] = {s1;s2;s3;s5;s6;s8;s9}. 
My intuition for nu x. <>x is "Start with x = all states and remove the states one by one which do not have a successor".

Could you please clarify this?

With kind regards,

Dardan 

Comments

Hi, I think s0 and s4 are included as they are predecessors of s1 and s5 respectively.

Answer 1

As you said, we have [|x|] = {s1;s2;s3;s5;s6;s8;s9} in this step.

<>x is satisfied by precisely the states that have at least one successor in the set of states satisfying x. Hence, all states but s3, s6, s7 satisfy <>x in this steps.

Comments

Thank you for your clarification. But I am still confused about why we have s0 and s4 added in step 1.
What I precisely mean:

STEP 1 : x = {s1;s2;s3;s5;s6;s8;s9}
[x] = {s1;s2;s3;s5;s6;s8;s9}
[ <>x] = {S0;s1;s2;S4;s5;s8;s9}

Why s0 and s4 came into play(into [ <>x]), when we do not have them in x. Am I looking in the wrong place or applying <>x wrongly.

Kind regards, Dardan

---

Yes. We don't have them in x. <>phi just means “does this state have a successor that satisfies phi”. Here, we don't have phi but x, and we fixed so that it represents a certain set of states. Now, we look at *all* states and check which of them have a transition to the given set. s0 has successor s1, s3, s4 has successor s5, and so on …