Problem in Zielonka Algorithm exam solution 22.09.06 problem 5

In the below Zielonka solution,

Doubt 1: At Game number 0, Should'nt it be B={S2,S3,S4,S5,S6,S7} instead of {S0,S3,S4,S5,S6,S7}?

Because, when i=1, atrr_(1-i)={s3,s4,s5,s6,s7} and the predecessors of s7 are s2 and s6. But in the exam solution, the predecessor of s3 which is s0 is also considered. But we will have to consider the universal predecessor of s3 instead of the existential predecessor and hence since s0 is the predecessor of s8 as well it cannot be included. Is our understanding correct?

Doubt 2:
Let's consider the solution is correct for B= {s0,s3,s4,s5,s6,s7} and the (win_1)g\b ={s1,s2,s8}. In this, why are we considering s8? Is it because s8 has no other choice apart from going to s1 and then being stuck in an infinite loop s1<->s6?

edited

The full solution is computed below, but let's directly address your question: B := attractor(0,winA0) := attractor(0,{s3,s4,s5,s6,s7}) := {s0,s3,s4,s5,s6,s7} as given in the example solution is correct. State s2 is controlled by player 1 which can can choose the transition s2->s1 so that we do not have to go to {s3,s4,s5,s6,s7}. However, s0 belongs to the attractor since s0 is controlled by player 0 who can choose the transition s0->s3 which enters the desired set. The states s1,s2,s8 are controlled by player 1, and player 1 can choose to stay there: s8->s1<->s2.

Let's see whether we agree with the solution, the outgoing colored edges show the choices of the players in the states. We therefore have the following plays:

• s0 -> s3 <-> s4 where player 0 wins with rank 8
• s1 <-> s2 where player 1 wins with rank 7
• s2 <-> s1 where player 1 wins with rank 7
• s3 <-> s4 where player 0 wins with rank 8
• s4 <-> s3 where player 0 wins with rank 8
• s5 -> s6 -> ... where player 0 wins with rank 8 as explained below
• in s6, player 1 has choices, but will lose the game with any choice:
• s6 <-> s5 where player 0 wins with rank 4
• s6 <-> s7 where player 0 wins with rank 6
• s6 -> s4 <-> s8 where player 0 wins with rank 8
• s6 -> s8 <-> s4 where player 0 wins with rank 8
• s8 -> s1 <-> s2 where player 1 wins with rank 7

So, the computation of the winning strategies is correct.

I do not understand your doubt 2, but maybe the above games answer that?

Here is the full computation of the winning strategies:

```    player0 0,3,5,7;
player1 1,2,4,6,8;
ranks   0:9; 1:6; 2:7; 3:8; 4:5; 5:3; 6:4; 7:6; 8:1;
transitions
0->3; 0->8; 1->0; 1->2; 2->1; 2->7; 3->2; 3->4;
4->3; 5->6; 6->3; 6->4; 6->5; 6->7; 7->6; 8->0; 8->1;
```

For the game graph, we find the highest rank h:=9 on states Qh:={s0}. As 9 is an odd number, player 1 may win if infinitely often visiting state s0 can be enforced by player 1, so we have i:=1. So, we compute the attractor set of player 1 and state s0 which are the states A := attractor(1,{s0}) := {s0,s1,s2,s8}. We remove these states from the game 0, and obtain game1 below which has the solution winA0={s3,s4,s5,s6,s7}; winA1={} as explained below.

Since winA0 is not empty, we have to solve another game that is obtained by removing the states B := attractor(0,winA0) := attractor(0,{s3,s4,s5,s6,s7}) := {s0,s3,s4,s5,s6,s7} from the game 0 which yields game 4 below which has the solution winB0={}; winB1={s1,s2,s8}. The solution of game 0 above is therefore win0={s0,s3,s4,s5,s6,s7}; win1={s1,s2,s8}.

Now, we remove the states {s0,s1,s2,s8} from the game graph, and solve the remaining game 1 shown above. In that game, the highest rank is h:=8 on states Qh:={s3}. As 8 is an even number, player 0 may win if infinitely often visiting state s3 can be enforced by player 0, so we have i:=0. So, we compute the attractor set of player 0 and state s3 which are the states A := attractor(0,{s3}) := {s3,s4}. We remove these states from the game 1, and obtain game2 below which has the solution win0={s5,s6,s7}; win1={} as explained below. Since win1={} holds, it follows that we do not need the second recursive call, and the solution of game 1 is win0={s3,s4,s5,s6,s7}; win1={}, i.e., player 0 has a winning strategy in all states of this game.

Now, we remove the states {s3,s4} from game 1 and solve the remaining game 2 shown above. Clearly, player 0 has a winning strategy in every state, since if player 1 will only finitely often visit state s7, it must visit state s5 from some time on always, but that implies that also state s6 is visited always from some time onwards. Therefore the highest rank that appears infinitely often would be 4, and player 0 wins. Otherwise, player 1 must visit s7 with rank 6 infinitely often, so that player 0 will win with rank 6. Hence, the solution of game2 is easily seen as win0={s5,s6,s7}; win1={}.

The above game 4 has clearly the solution win0={}; win1={s1,s2,s8} since there is only one infinite path where player 1 will win with rank 7.

by (170k points)
I still do not understand the "State s2 is controlled by player 1 which can choose the transition s2->s1 so that we do not have to go to {s3,s4,s5,s6,s7}. However, s0 belongs to the attractor since s0 is controlled by player 0 who can choose the transition s0->s3 which enters the desired set. "  So you have not considered the s2 because s7 belongs to player 0 and s2 belongs to player 1 which is not the universal predecessor of s7. You have included s0 because s0 is the predecessor of s3 and both belong to the same player 0?
But our understanding was:
i. since i = h mod 2: 9 mod2 = 1
ii. (win_0,win_1 )\A = (s3,s4,s5,s6,s7)  look for the predecessors of these states.
s3(player:0)= predecessors of s3 = (S0, S4, S6)  But since we have i=1(player 1) we can include existential predecessor of S3 if they belong to player 1 [since i=1] and if the predecessors belong to different player (here player 0) then include it only if it is universal predecessor.  With this understanding and also since we are at player 1[i=1],  S3(player 0)'s predecessor S0(player 0) is not the universal predecessor of S3. So we did not include S0.
S7(player 0) predecessors are S6,S7;    S7 belongs to player 1 and we are at i=1[player 1], so S7 need not be universal predecessor of S7 and hence S7 can be inlcuded which results in B={s0,s3,s4,s5,s6,s7}.
Is our understanding correct?
Well, we need to compute B := attractor(0,{s3,s4,s5,s6,s7}) which clearly contains already the given states {s3,s4,s5,s6,s7}. Apart from these, we have to add the states where player 0 can enforce that the game play reaches one of the states in {s3,s4,s5,s6,s7}.

This is not just the universal predecessor set, it is rather defined as attrA(φ) :⇔ μx.(φ ∨ ⟨A⟩x) for player A where ⟨A⟩φ := (A ⇒ <>φ|[]φ), i.e., a state belongs to ⟨A⟩φ if it is controlled by player A and has a successor where φ, and if it is controlled by the other player, then all successors must belong to φ. So, it depends whether a state is controlled by which one of the players.

To compute the attractor, we inspect the states which are predecessors of {s3,s4,s5,s6,s7}. These are the states s0 and s2. State s0 is controlled by player 0, so it is sufficient if one transition leads to {s3,s4,s5,s6,s7} which is the case, so s0 must be added. State s2 is however controlled by player 1, so that it will only be added to the attractor if all its successors reach {s3,s4,s5,s6,s7}. This is not the case, player 1 can also choose the transition s2->s1, so that {s3,s4,s5,s6,s7} is not reached.

Having added s0, we also have to check which states can enforce to visit s0. Its predecessors are s1 and s8, but both are controlled by player 1 which can choose transition which do not led to s0. So, apart from s0 no further states are added to {s3,s4,s5,s6,s7}.
Thank you very much for explaining in detail again. Unfortunately, I am confused again.

1.    “ To compute the attractor, we inspect the states which are predecessors of {s3,s4,s5,s6,s7}. These are the states s0 and s2. State s0 is controlled by player 0, so it is sufficient if one transition leads to {s3,s4,s5,s6,s7} which is the case, so s0 must be added. State s2 is however controlled by player 1, so that it will only be added to the attractor if all its successors reach {s3,s4,s5,s6,s7}. This is not the case, player 1 can also choose the transition s2->s1, so that {s3,s4,s5,s6,s7} is not reached.

This is not just the universal predecessor set, it is rather defined as attrA(φ):⇔ μx.(φ ∨ ⟨A⟩x) for player A where ⟨A⟩φ:= (A ⇒ <>φ|[]φ), i.e., a state belongs to ⟨A⟩φ if it is controlled by player A and has a successor where φ, and if it is controlled by the other player, then all successors must belong to φ. So, it depends whether a state is controlled by which one of the players.”

Doubt: My understanding after reading the explanation is: For computing the attractor, Say for example, according to “we inspect the states which are predecessors of {s3,s4,s5,s6,s7}. These are the states s0 and s2. State s0 is controlled by player 0, so it is sufficient if one transition leads to {s3,s4,s5,s6,s7} which is the case, so s0 must be added.”  ;

S0(player 0) is added because its transition leads to S3(player 0) and both S0 and S3 belong to the same player (i.e. player 0), it is sufficient if one transition leads to S3? Is this understanding correct?

If it is correct, then in the solution :

In Game number 0: {S0,S1,S2,S3,S4,S5,S6,S7,S8}
h=9
i=1
Q_h=S0
A={S0,S1,S2,S8}

Here while computing A,  we inspect the states which are predecessors of {S0 }. These are the states S1, S8.  But since S0 belongs to player 0 and S1 belongs to player 1,  also S1 has transition to S2 as well S1->S2, S1 should not be added to A?   Then why is S1 added to A?
Similarly, S8 (player 1) is predecessor of S0(player 0) and S8(player 1) can choose the transition(S1->S8) which do not belong to Q_h( S0) ?Then why is S8 added to A?
State s0 is not added because the state s3 reached from s0 belongs to the same player. It is added because s0 belongs to player 0, and player 0 can therefore choose to switch from s0 to s3. State s2 is not added because s2 belongs to player 1, and player 1 may choose to switch to s1 so that the desired state set will not be reached. It matters which player has the control over the state. According to this, we compute existential or universal predecessors.
Thank you, Prof. for explaining.