There is a fundamental relation between the modal mu-calculus and infinite-duration two-player games, highlighted perhaps best by the well-known equivalence of mu-calculus formula evaluation and the solution of so-called parity games. Furthermore, parity games also feature prominently in tableau-based reasoning methods for the mu-calculus. Recent work has also shown that the close relation between extremal fixpoints in the mu-calculus and parity conditions can be generalized, lifting the connection to the level of fixpoint equation systems over arbitrary complete lattices.

In this talk, I will detail the above-mentioned connections, summing up recent research that shows how results from game theory can be used to improve and generalize existing algorithmic methods for the analysis of mu-calculus formulas. While this approach leads to improved worst-case runtime guarantees on one hand, it also enables the treatment of generalized mu-calculi that involve, e.g., quantitative or probabilistic modalities.