Strategiesynthese für Paritätsspiele auf endlichen Graphen

Parity games are infinite two person games, here considered on finite graphs. A play is an infinite path in the graph, whose vertices are chosen by the two players in alternation. The winner of the play is determined by the vertices that are visited infinitely often in the play. The problem of solving a parity game (i.e., finding the winner for plays starting in a given vertex and the construction of a winning strategy) belongs to the complexity class NP intersection co-NP. It is one of the core problems in the theory of program verification, because many model checking problems can be reduced to solving parity games by a polynomial time reduction. In this thesis a new algorithm for solving parity games is presented. Contrary to known discrete procedures this one uses the method of strategy improvement as it is already known from stochastic games. Unlike for procedures in the literature, no example is known for the present algorithm which requires polynomial time. The algorithm is based on a new kind of valuation for infinite plays