Solving Parity Games in Practice

This lecture covers the practical aspects of solving parity games, where players move tokens along edges in a directed total graph. Winning strategies are discussed, along with the determinacy of games and the relationship between parity games and model checking. Various algorithms, such as the Recursive Algorithm and the Small Progress Measures Algorithm, are presented, each with its analysis and examples. The lecture also explores the complexity of solving parity games, the need for determinism, and heuristic approaches. Universal optimizations, reductions of the graph structure, solving of special cases, and problem-specific parameter reductions are highlighted as key strategies for efficient solving. The lecture concludes by discussing the discrepancy between theoretical and practical results in solving parity games.