  Solving parity games, which are equivalent to modal $\mu$-calculus model
checking, is a central algorithmic problem in formal methods. Besides the
standard computation model with the explicit representation of games, another
important theoretical model of computation is that of set-based symbolic
algorithms. Set-based symbolic algorithms use basic set operations and one-step
predecessor operations on the implicit description of games, rather than the
explicit representation. The significance of symbolic algorithms is that they
provide scalable algorithms for large finite-state systems, as well as for
infinite-state systems with finite quotient. Consider parity games on graphs
with $n$ vertices and parity conditions with $d$ priorities. While there is a
rich literature of explicit algorithms for parity games, the main results for
set-based symbolic algorithms are as follows: (a) an algorithm that requires
$O(n^d)$ symbolic operations and $O(d)$ symbolic space; and (b) an improved
algorithm that requires $O(n^{d/3+1})$ symbolic operations and $O(n)$ symbolic
space. Our contributions are as follows: (1) We present a black-box set-based
symbolic algorithm based on the explicit progress measure algorithm. Two
important consequences of our algorithm are as follows: (a) a set-based
symbolic algorithm for parity games that requires quasi-polynomially many
symbolic operations and $O(n)$ symbolic space; and (b) any future improvement
in progress measure based explicit algorithms imply an efficiency improvement
in our set-based symbolic algorithm for parity games. (2) We present a
set-based symbolic algorithm that requires quasi-polynomially many symbolic
operations and $O(d \cdot \log n)$ symbolic space. Moreover, for the important
special case of $d \leq \log n$, our algorithm requires only polynomially many
symbolic operations and poly-logarithmic symbolic space.
