12 - Parity games and infinite tree automata

Question 1

How to play a parity game?

Answer 1

Two players A and P moves a token between positions (not necessarily finite). Positions have owner and priority Ω.

A wins if the highest priority that occurs infinitely often is even

A = even = circle
P = odd = square

Question 2

What are attractors? How we compute them

Answer 2

let u ⊆ Pos
the attractor is the positions from which A can force a visit to u, no matter what the opponent does

formally:

attractor u for player A is:
AttrA(u) := (j ∈ N)U AttrjA(u)
where 
AttrjA(u) := u and Attr(j+i)A(u)
where 
Attr(j+i)A(u) :=Attr(j)A(u) + positions that can be reached in 1 step for player A

It is computed expanding 1 step until fixed point

used on McNZSolver to compute winning strategies

Question 3

Closure properties PTA

Answer 3

Complementation

Question 4

tree closed under complement main steps of the proof

Answer 4

1) Construct alphabet Δ over Σ x S
S = winning strategy for P
2) Construct DPTA for
Lp ⊆ (Δ x D) ^ ω
DPA A’ = (Δ x D, Qp, q0p, –>p, Ωp)
3) From A’, we obtain the tree automaton ¬A* changing the transitions
4) Project ¬A* to the first component Σ of Δ = ΣxS and obtain ¬A

Question 5

PTA acceptance?

Answer 5

acceptance of tree can be characterized by tree, even omega reg lang know path derive tree automata of tree language

Understand acceptance of tree t by PTA A as parity game G(A,t)

t ∉ L(A) if P has winning strategy

P for Pathfinder
A for Acceptor

Question 6

PTA emptiness?

Answer 6

Abstract alphabet of original PTA A to single letter and accept single tree more generic tree A-. If this tree is not accepted, then neither is A.

its like buchi, use closure properties of pta