In graph games, a player will lose the game if that player cannot choose a transition, hence all players must avoid that their deadend states are reached. Conversely, of course, they try to reach a deadend state controlled by the other player.
In parity games, the winner of an infinite game play is determined in that we determine the highest rank that occurs infinitely often on the game play, and check whether this rank is even or odd. If the game play is finite, the player controlling the final deadend state loses.
When computing an attractor, we compute the fixpoint attrA(φ) :⇔ μx.(φ ∨ ⟨A⟩x) with ⟨A⟩φ := A ∧ <>φ ∨ B ∧ []φ. Since it is a least fixpoint, we start the fixpoint computation with false, and obtain next φ ∨ ⟨A⟩false = φ ∨ ⟨A⟩false = φ ∨ A ∧ <>false ∨ B ∧ []false = φ ∨ B ∧ deadend, i.e., the φ-states plus the deadend states of the other player.
Somehow, the deadend states may considered to be wrong in this set since from there, it is not possible to enforce a visit of Qh. However, their membership in the attractor is justified in that reaching them also makes player A win as well as reaching the states with the highest rank (infinitely often).
