The games-for-verification crowd seems to be a different community from those of us who do algorithmic game theory (coming from economics). The topic is not covered in the textbook (fair enough I suppose, the book is big enough already). I dropped in on them to give a tutorial Nash equilibria and computational complexity, at the meeting GAMES 2010, the annual Workshop of the ESF Networking Programme on Games for Design and Verification. I got the impression that France and Poland are well-represented in that community, although that may just be an artifact of the composition of the network.
They have the main open problem of: what is the complexity of solving parity games? (Google: did you mean party games?) Parity games are known to be in both NP and co-NP, also known to be mildly subexponential (Zwick and Paterson), so believed to be in P. Currently there are no proposed algorithms that are conjectured to do the job; apparently there used to be one, but it was recently shown to be exponential in the worst case, for an artificial class of examples. The parity games problem is derived from the problem of checking whether a formula in modal mu-calculus is satisfied by a given Buchi automaton, and I gather that is a poly-time reduction. There is also an exponential-time reduction if instead the formula is in monadic second-order logic. However, the work on parity games seems to take on a life of its own, without the need to refer to model-checking. So for example, I am not sure that the question of finding a mixed equilibrium for a parity game relates to solving a model-checking problem, but it's an interesting topic.