Zielonka attractors

Question

How the attractor state has s1? Attractors are something which enforce the player to stay in that state. Here s1 does not have any transitions and it's for player 0. If a state is a deadend can be add it ?

Answer 1

s1 is a deadend state, and the attractors are defined with modal operators ⟨A⟩ and ⟨B⟩ as follows:

•     attrA(φ) := μx.(φ ∨ ⟨A⟩x) 
•     attrB(φ) := μx.(φ ∨ ⟨B⟩x)
•     ⟨A⟩φ := A ∧ <>φ ∨ B ∧ []φ = (A=><>φ|[]φ)
•     ⟨B⟩φ := A ∧ []φ ∨ B ∧ <>φ = (A=>[]φ|<>φ)

Since we compute least fixpoints, we start with the empty set of states. Now, if φ=false, then we have

•     ⟨A⟩false := A ∧ <>false ∨ B ∧ []false = B ∧ dead
•     ⟨B⟩false := A ∧ []false ∨ B ∧ <>false = A ∧ dead

Hence, the attractors also collect deadend states controlled by the other player (see also page 145 of VRS-05-MuCalculus). This is correct, since if a player cannot choose a transition (since there is none), then the player will lose the game.

Comments

So, its applicable in
B := attr1−i(win′1−i); logic as well. Is it correct? So whenever there is a deadend , we can add as an attractor?

---

if it is a deadend state controlled by the other player, yes

---

And if the the same player has deadend we can't add to the attractors right?
 Example, if s0 is the Qh, and it's controlled by player 0,
we have deadend s1 controlled by player 1 and another deadend s2 controlled by player 0. So in the attractors, we have {s0,s1} , we can't add s2 to the attractors. Is it correct ?

    Also, here it should be,    ⟨B⟩φ := A ∧ []φ ∨ B ∧ <>φ = (B=>[]φ|<>φ) , is that right?
It's written as ⟨B⟩φ := A ∧ []φ ∨ B ∧ <>φ = (A=>[]φ|<>φ) , SNF for A. But should be SNF of B right ?

---

No, then the deadend state is not added. Just note that we have to compute for the attractor of player A the states closed under ⟨A⟩ which will add the deadend states controlled by player B, but not those of player A (unless these should already be in the formula phi).

---

Yeah..I understood. Thanks for the clarification.