mu calculus to CTL model checking

Question

The ques is from Sept 2016 prob 4 S2.

S = nu.y. diamond(y) & (mu.x (avb) V box(x))

Here i replace mu.x to AF(avb). And i have avb = {s1,s3,s6,s8} // s3 and s8 holds for all the formula.

And i have to check for all the infinite paths of the state, the path must visit  these states.

So i have AF(avb)  = {s4,s6,s5,s7,s3,s8} //s7 holds as it visits s1 initially, s3 and s8 holds for all the formulas.

Is my understanding right?

since Y is not dependent on x diamond(y) is same. And i compute    AF(avb) &diamond(y).

Is this the final states where i should check for all the initial states to satisfy the property?

Please help

Answer 1

Yes, your thoughts are correct. But I think AF(avb) (or equivalently µx.(avbv[]x)) holds on states {s1;s3;s4;s6;s7;s8}. Anyway, after having computed these states, you can proceed with the outer fixpoint that does not mutually depend on the inner one.

The transition system is the following one:

and the computation goes like this:

  computing states of A F (a | b)

  i.e., computing states of mu Z. (a | b | [] Z)

• 〖a〗= {s1;s8}
• 〖b〗= {s1;s6}
• 〖a | b〗 = {s1;s6;s8}

    step 0 : Z = {}

• 〖Z〗= {}
• 〖[] Z〗 = {s3;s8}
• 〖a | b | [] Z〗 = {s1;s3;s6;s8}

    step 1 : Z = {s1;s3;s6;s8}

• 〖Z〗= {s1;s3;s6;s8}
• 〖[] Z〗 = {s3;s4;s7;s8}
• 〖a | b | [] Z〗 = {s1;s3;s4;s6;s7;s8}

    step 2 : Z = {s1;s3;s4;s6;s7;s8}

• 〖Z〗= {s1;s3;s4;s6;s7;s8}
• 〖[] Z〗 = {s3;s4;s7;s8}
• 〖a | b | [] Z〗 = {s1;s3;s4;s6;s7;s8}

    fixpoint reached!〖mu Z. (a | b | [] Z)〗 = {s1;s3;s4;s6;s7;s8}

Comments

But why not s5? s5 has one outgoing infinite path that visits s6.

---

It also has an outgoing path that does never visit a state in a|b: Look at the path s5;(s2;s0)^omega. Note that we are checking AF and not EF.

---

Got it.Thank you