Abstract
Game graphs are used in model checking to verify the existence of desirable properties of a system. We will give an introduction to the graph algorithmic problems that arise on game graphs and present the state of the art in upper and (conditional) lower bounds on the running time for solving these problems. This is joint work with Krishnendu Chatterjee, Wolfgang Dvorak and Veronika Loitzenbauer.