BDD-based parity game solving: a comparison of Zielonka's recursive algorithm, priority promotion and fixpoint iteration
Lisette Sanchez, J.W. Wesselink, Tim A. C. Willemse · TU/e Research Portal · 2018
Parity games are two player games with omega-winning conditions, played on finite graphs.Several algorithms for solving parity games have been proposed in the literature, and while the problem was recently shown to be solvable in quasi-polynomial time, so far, the question whether such games can be solved in polynomial time remains elusive.In practice, parity games play an important role in verification, satisfiability and synthesis.It is therefore important to identify algorithms that can efficiently deal with large and complex games that arise from such applications.In this paper, we describe our experiments with BDDbased implementations of Zielonka's recursive algorithm, the more recent Priority Promotion algorithm and the Fixpoint-Iteration algorithm.We conclude that overall, Zielonka's BDD-based algorithm beats the BDDbased Priority Promotion algorithm by a small margin for games that are characteristic of practical verification problems.For games with a large number of distinct priorities, Priority Promotion scales better.The Fixpoint-Iteration algorithm performs similar to Zielonka's algorithm for games with at most 5 different priorities.