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.
