Zielonka - Practice Questions

Question

Can you please give us some practice questions for the Zielonka algorithm to understand it conceptually better?

We can use the help of teaching tool to cross-check our answers.

Answer 1

Well, it is not that easy to come up with a couple of meaningful examples. If we try to generate them randomly, they are often not good in the sense that they produce bad computations. However, with every example that is there, you get typically many recursive calls and these are further examples that you can study. Anyway, we try to generate more examples and will make them available in the future. 

Little side remark: In the lecture, it was told the µ-calculus model checking is equivalent to a parity game (pages 122-133). Hence, from every µ-calculus model-checking problem, you can get a parity game that you can use. If you use the local model checking tool (on https://es.cs.uni-kl.de/tools/teaching/ModelChecking.html), you find an option to convert the model-checking problem to a parity game. That is nothing else but the local model checking that applies all rules even if these are not needed for the proof. 

Comments

I found in the internet some parity games that I have modified a bit, so here is a list of some examples:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 0,2,5,6;
player1 1,3,4;
ranks   0:1; 1:3; 2:3; 3:4; 4:2; 5:0; 6:3;
transitions
    0->1; 0->4; 1->2; 1->4; 2->2; 2->3; 3->6;
    4->1; 4->5; 4->6; 5->2; 5->3; 6->6;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 1,3,4;
player1 0,2,5,6;
ranks   0:1; 1:3; 2:3; 3:4; 4:2; 5:0; 6:3;
transitions
    0->1; 0->4; 1->2; 1->4; 2->2; 2->3; 3->6;
    4->1; 4->5; 4->6; 5->2; 5->3; 6->6;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 0,3,4,5;
player1 1,2,6;
ranks   0:3; 1:3; 2:5; 3:2; 4:2; 5:5; 6:2;
transitions
    0->2; 1->5; 1->1; 1->2; 1->3; 1->5; 2->3;
    2->4; 2->6; 3->3; 3->5; 3->6; 4->6; 5->2;
    6->4; 6->6;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 1,2,6;
player1 0,3,4,5;
ranks   0:3; 1:3; 2:5; 3:2; 4:2; 5:5; 6:2;
transitions
    0->2; 1->5; 1->1; 1->2; 1->3; 1->5; 2->3;
    2->4; 2->6; 3->3; 3->5; 3->6; 4->6; 5->2;
    6->4; 6->6;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 0,1,2,3,4;
player1 5,6,7;
ranks   0:2; 1:3; 2:2; 3:1; 4:3; 5:2; 6:4; 7:6;
transitions
    0->1; 1->2; 2->0; 2->4; 3->4; 3->6;
    4->6; 4->7; 5->0; 5->1; 5->2; 5->3; 6->7; 7->5;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 5,6,7;
player1 0,1,2,3,4;
ranks   0:2; 1:3; 2:2; 3:1; 4:3; 5:2; 6:4; 7:6;
transitions
    0->1; 1->2; 2->0; 2->4; 3->4; 3->6;
    4->6; 4->7; 5->0; 5->1; 5->2; 5->3; 6->7; 7->5;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 0,1,2,3;
player1 4,5,6,7;
ranks   0:0; 1:2; 2:1; 3:3; 4:0; 5:4; 6:3; 7:1;
transitions
    0->1; 0->4; 1->2; 2->2; 2->3; 3->0;
    4->0; 4->5; 5->7; 6->4; 7->6; 7->7;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 4,5,6,7;
player1 0,1,2,3;
ranks   0:0; 1:2; 2:1; 3:3; 4:0; 5:4; 6:3; 7:1;
transitions
    0->1; 0->4; 1->2; 2->2; 2->3; 3->0;
    4->0; 4->5; 5->7; 6->4; 7->6; 7->7;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 1,3,4;
player1 0,2;
ranks   0:0; 1:0; 2:1; 3:0; 4:0;
transitions 0->1; 0->2; 1->0; 1->2; 2->2; 3->2; 4->3;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 0,2;
player1 1,3,4;
ranks   0:0; 1:0; 2:1; 3:0; 4:0;
transitions 0->1; 0->2; 1->0; 1->2; 2->2; 3->2; 4->3;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 0,1,6,7;
player1 2,3,4,5;
ranks   0:2; 1:4; 2:5; 3:1; 4:2; 5:3; 6:2; 7:1;
transitions
    0->1; 0->4; 1->2; 1->5; 2->1; 2->6;
    3->2; 3->3; 3->7; 4->0; 4->7; 5->1;
    5->4; 6->2; 6->7; 7->3; 7->4;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 2,3,4,5;
player1 0,1,6,7;
ranks   0:2; 1:4; 2:5; 3:1; 4:2; 5:3; 6:2; 7:1;
transitions
    0->1; 0->4; 1->2; 1->5; 2->1; 2->6;
    3->2; 3->3; 3->7; 4->0; 4->7; 5->1;
    5->4; 6->2; 6->7; 7->3; 7->4;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 1,4;
player1 0,2,3;
ranks   0:3; 1:3; 2:2; 3:1; 4:2;
transitions 0->1; 0->4; 1->0; 1->2; 2->1; 3->2; 3->4; 4->3;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
player0 0,2,3;
player1 1,4;
ranks   0:3; 1:3; 2:2; 3:1; 4:2;
transitions 0->1; 0->4; 1->0; 1->2; 2->1; 3->2; 3->4; 4->3;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%