A randomized subexponential algorithm for parity games

Abstract

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.