Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

769 questions

886 answers


424 users

0 votes

in * TF "Emb. Sys. and Rob." by (200 points)

1 Answer

+1 vote
The exercise is about a graph game with two players. Player 0 chooses a transition in the oval nodes while player 1 chooses a transition in the rectangle nodes. This creates an infinite path where the winner of the game is determined by checking the nodes that occur infinitely often on the generated path. The Zielonka algorithm can be used to compute a winning strategy for the players if there is one. Have a look at the teaching tool that helps you with the solution.
by (117k points)
Thanks for the response. I have tried to decode the working but I did not get it what the attractor is how the algorithm is working etc. If you can provide a detail answer, it will be great.
Solving parity games with Zielonka's algorithm is described in detail in the final section of the chapter on μ-calculus. There you can read that attrA(φ) is the set of states where player A can enforce reaching a φ-state hence, attrA(φ) :⇔ μx.(φ ∨ ⟨A⟩x) where ⟨A⟩φ means that player A can enforce a transition to a state where φ holds. This is defines as  ⟨A⟩φ := A ∧ ♦φ ∨ B ∧ φ, i.e., a state belongs to ⟨A⟩φ if player A can choose a transition, and there is a transition to φ or if player B can choose and all transitions lead to φ. The attractor set attrA(φ) is therefore the set of states where player A can enforce a path to the states φ no matter what player B will do.
What does A & B here refer to? Does A & B refer to player 0(oval) and player 1(rectangle) respectively? I was able to understand the trace of the algorithm but the only part I am getting confused is calculating the attractors. I understood what this equation meant ⟨A⟩φ := A ∧ ♦φ ∨ B ∧ φ. However I was not able to figure out what A & B stands for? Could you please give an example?
The game has player A and player B which are in parity games also called player 0 (oval nodes) and player 1 (rectangle nodes).
Thank you for the clarification.
Imprint | Privacy Policy