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