+1 vote

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 

in * TF "Emb. Sys. and Rob." by (150 points)
Hi, I think s0 and s4 are included as they are predecessors of s1 and s5 respectively.

1 Answer

+1 vote
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.
by (24.7k points)
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 …

Related questions

0 votes
1 answer
0 votes
1 answer
asked Aug 24, 2020 in * TF "Emb. Sys. and Rob." by nimteaj (770 points)
0 votes
1 answer
+2 votes
1 answer
asked Aug 16, 2018 in * TF "Emb. Sys. and Rob." by cjcbusatto (180 points)
0 votes
1 answer
Imprint | Privacy Policy
...