Graph operations on parity games and polynomialtime algorithms

Parity games are games that are played on directed graphs whose vertices are labeled by natural numbers, called priorities. The players push a token along the edges of the digraph. The winner is determined by the parity of the greatest priority occurring infinitely often in this infinite play. A motivation for studying parity games comes from the area of formal verification of system