Global model checking

Question

For above problem trying solve b ^ vx. diamond(x), below is my solution , i didnt understand  how it is {S0,s4}

Answer 1

It is b ∧ nu x. <>x, not b^… (^ is xor, ∧ is and).

I'm not sure whether I understand your notes correctly but you already wrote y = {s0, s4}.  First, we do nu y. <>y. y0 = all states, y1=all states except s7 because it as no successor hence, also none to y0, y2=y1. Now, we intersect it with the states satisfying b (s0, s4, s7). As we already kicked out s7, only s0, s4 are left.

To solve the outer mu, we just iteratively add predecessors that satisfy a. The iteration likes likes: s0,s4, then s0, s4, s5, then s0, s4, s5, then s0, s4, s5, s1, then s0, s4, s5, s1, s2, then fixpoint.

Comments

Okay thank you so much. So, for inner bracket (b ∧ nu x. <>x), is it not required to reach the fix point?. And , what should be the order to consider while solving this problem. First, I need to solve for (nu x) and then (nu x . <>x) and then (b ∧ nu x. <>x).

---

The inner fixpoint is nu x. <>x. We do reach it. It is all states except for s2. We then compute b ∧ nu x. <>x by intersecting b and the fixpoints. We got {s0, s4}.

I don't understand the following problem.