Doubt regarding calculating winning strategies in Zielonka Algorithm

Hello!

I have two queries regarding calculating winning strategies of both players (win0' & win1') in the above mentioned game.

*) I have calculated win0' = {s0, s3} but as per solution provided by tool it is only {s0}. Why s3 is not included? s3 has a loop so player 0 can also win there as rank is even.

*) I have calculated win1' = {s2, s7} but as per solution provided by tool it is {s2, s4, s6, s7}. I didn't get why we are considering s4 & s6, they are not in loop.

Please correct me if I have understood something wrong.

You are confused because player 0 has a winning strategy in state s3 which is true as you can see with the result that the tool finally computes. However, for the first recursive call, we remove the attractor A := attractor(0,Qh) := {s1,s3,s5} so that these states do no longer belong to the game1 that is solved in the recursive call. Hence, these states will neither occur in win0' nor in win1'. For the first recursive call, we consider the following game:

For your second question, look at the above game graph. Player 1 has a winning strategy in states s4 and s6, since in s4 player 1 can choose the transition to s2 (but even the other one will also do), and in s6, player 0 has no other choice than also moving to s2. In s2, player 0 has no other choice than moving to s7 where player 1 moves back to s2 which generates an infinite play where s2 and s7 occur infinitely often. Hence, the highest rank that appears infinitely often is 5 which is odd, so that player 1 win in the states s4 and s6 for sure.

Right?

by (166k points)
selected by
Yeah got it :) Thank you so much professor!