September 21, 2017, Thursday

From BIMIB

Jump to: navigation, search

Seminar September 19, 2008, 11.30

Parity Games

Romeo Rizzi

Friday September 19, 2008, DISCo U14, T024, 11:30

A parity game is played on a graph (V, E) by two players, Even and Odd, who move a token from vertex to vertex along the edges of the graph so that an infinite path is formed. A partition (V0, V1) is given of the set V of vertices; player Even moves if the token is at a vertex of V0 and player Odd moves if the token is at a vertex of V1. Finally, a priority function p from V to { 1, 2, . . . , d } is given. The players compete for the parity of the highest priority occurring infinitely often: player Even wins if the limit, for i tending to infinity, of p(vi) is even while player Odd wins if it is odd, where v0 , v1 , v2 , . . . is the infinite path formed by the players. The algorithmic problem of solving parity games is, given a parity game G =(V0 , V1 , E, p) and an initial vertex v0 belonging to V, to determine whether player Even has a winning strategy in the game if the token is initially placed on vertex v0. An important motivation to study the problem of solving parity games is its intriguing complexity theoretic status: the problem is known to be in the intersection of NP and co-NP and even in the intersection of UP and co-UP but, despite considerable efforts no polynomial time algorithm has been found so far. The original motivation for the study of parity games comes from the area of formal verification of systems by temporal logic model checking. The problem of solving parity games is polynomial time equivalent to the non-emptiness problem of some class of automata on infinite trees with Rabin-chain acceptance conditions and to the the model checking problem of modal fixpoint logic which is a specification formalism of choice in formal specification.