We describe a randomized algorithm for Parity Games (equivalent to the Mu-Calculus Model Checking), which runs in expected time 2O(k1/(1+2varepsilon))subexponential in the number of colors k of the game graph when k is Omega (n1/2+varepsilon), n is the number of vertices, and 0<varepsilonleq 1/2.
All previously known algorithms were exponential in the number of colors, with the best one taking time and space O(k2· n· sqrt(n)k).
Our algorithm does not rely on Linear Programming subroutines and uses a low-degree polynomial space.
Available as Postscript (318 kB, no cover)
Download BibTeX entry.