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