Zielonka’s Algorithm for Parity Games: Example

Question

I have multiple questions/doubts here:

1: How are attractors computed? This is the formula, right?

attrA(φ) :⇔ μx.(φ ∨ ⟨A⟩x) and attrB(φ) :⇔ μx.(φ ∨ ⟨B⟩x)

But I cannot really understand how attr0(win′0) = {s0, s1, s2, s3, s4, s5, s6}

2. How is win₁′ = {s0, s1, s2, s3} in that path, the highest rank is 16, doesn't that mean player 0 wins?

3. Also confused about how actually to compute attractors in general.

I must be missing some parts of my understanding and need help!

Answer 1

Attractors are computed as explained on slide 150, and some or their properties are also mentioned there. Hence, your formulas for the attractors are correct. For this reason, computing attractors is done by µ-calculus model checking.

About your second question, win1'={s0, s1, s2, s3} is not a path, but the set of states where player 1 has a winning strategy. We thereby consider the game on page 161 and yes, the highest rank of the four states is the rank of state s1 which is 16 and that number is even. However, state s1 cannot be visited infinitely often. There are just two paths, the one where we always loop in s0 such that the highest rank would be 3, and the other path is s3 s1 (s2 s4)^omega where the states visited infinitely often are s2 and s3 and thus the highest rank visited infinitely often is 5 which is also odd, so that player 1 also wins that play.

For the game on page 160 that you consider, we have to compute attr1({s4}) and later then also attr0(win0') for the second recursive call. These are computed in the game that is considered as a Kripke structure with the above fixpoints. Hence, in detail, the computation is as follows:

 µx.(p ∨ a∧<>φ ∨ b∧[]φ):

〖p〗= {s4}

〖q〗= {s5;s6}

〖a〗= {s0;s1;s2;s3;s4;s5}

〖b〗= {s6}

step 0 : x = {}
    〖x〗= {}
    〖<> x〗 = {}
    〖[] x〗 = {}
    〖a & [] x〗 = {}
    〖b & <> x〗 = {}
    〖p | a & [] x | b & <> x〗 = {s4}
step 1 : x = {s4}
    〖x〗= {s4}
    〖<> x〗 = {s3}
    〖[] x〗 = {}
    〖a & [] x〗 = {}
    〖b & <> x〗 = {}
    〖p | a & [] x | b & <> x〗 = {s4}
fixpoint reached!

and the second attractor:

computing states of mu x:bool. (q | a & <> x | b & [] x)

step 0 : x = {}
    〖x〗= {}
    〖<> x〗 = {}
    〖a & <> x〗 = {}
    〖[] x〗 = {}
    〖b & [] x〗 = {}
    〖q | a & <> x | b & [] x〗 = {s5;s6}
step 1 : x = {s5;s6}
    〖x〗= {s5;s6}
    〖<> x〗 = {s4;s5;s6}
    〖a & <> x〗 = {s4;s5}
    〖[] x〗 = {s4;s6}
    〖b & [] x〗 = {s6}
    〖q | a & <> x | b & [] x〗 = {s4;s5;s6}
step 2 : x = {s4;s5;s6}
    〖x〗= {s4;s5;s6}
    〖<> x〗 = {s3;s4;s5;s6}
    〖a & <> x〗 = {s3;s4;s5}
    〖[] x〗 = {s4;s6}
    〖b & [] x〗 = {s6}
    〖q | a & <> x | b & [] x〗 = {s3;s4;s5;s6}
step 3 : x = {s3;s4;s5;s6}
    〖x〗= {s3;s4;s5;s6}
    〖<> x〗 = {s2;s3;s4;s5;s6}
    〖a & <> x〗 = {s2;s3;s4;s5}
    〖[] x〗 = {s2;s4;s6}
    〖b & [] x〗 = {s6}
    〖q | a & <> x | b & [] x〗 = {s2;s3;s4;s5;s6}
step 4 : x = {s2;s3;s4;s5;s6}
    〖x〗= {s2;s3;s4;s5;s6}
    〖<> x〗 = {s1;s2;s3;s4;s5;s6}
    〖a & <> x〗 = {s1;s2;s3;s4;s5}
    〖[] x〗 = {s1;s2;s3;s4;s6}
    〖b & [] x〗 = {s6}
    〖q | a & <> x | b & [] x〗 = {s1;s2;s3;s4;s5;s6}
step 5 : x = {s1;s2;s3;s4;s5;s6}
    〖x〗= {s1;s2;s3;s4;s5;s6}
    〖<> x〗 = {s0;s1;s2;s3;s4;s5;s6}
    〖a & <> x〗 = {s0;s1;s2;s3;s4;s5}
    〖[] x〗 = {s1;s2;s3;s4;s5;s6}
    〖b & [] x〗 = {s6}
    〖q | a & <> x | b & [] x〗 = {s0;s1;s2;s3;s4;s5;s6}
step 6 : x = {s0;s1;s2;s3;s4;s5;s6}
    〖x〗= {s0;s1;s2;s3;s4;s5;s6}
    〖<> x〗 = {s0;s1;s2;s3;s4;s5;s6}
    〖a & <> x〗 = {s0;s1;s2;s3;s4;s5}
    〖[] x〗 = {s0;s1;s2;s3;s4;s5;s6}
    〖b & [] x〗 = {s6}
    〖q | a & <> x | b & [] x〗 = {s0;s1;s2;s3;s4;s5;s6}
fixpoint reached!