Global model checking

Question

Hello

Please may clarify why in following exam "Problem 4.d" the red highlighted part being all states, should not be s0,s1,s2,s3,s4,s5,s6?

https://es.cs.uni-kl.de/teaching/vrs/exams/2021.02.17.vrs/2021.02.17.vrs.solutions.pdf

Thanks.

Answer 1

That seems to be a little mistake. Actually, there is no variable d and the formula does not ask for an implication inf->d. It seems that when producing a comprehensive solution, we have abbreviated the states satisfying EF c by d. Assuming this, we have

    [|inf|] = {s0;...;s6}
    [|!inf|] = {s7}
    [|d|] = [|EF c|] = {s0;s1;s2;s3;s4;s5;s6} = [|inf|]
    [|inf -> EF c|] = [|!inf | EF c|] = {s7} ∪ {s0;...;s6} = {s0;...;s7}