Solving Parity Games in Big Steps

Sven Schewe

This paper proposes a new algorithm that improves the complexity bound for solving parity games. Our approach combines McNaughton’s iterated fixed point algorithm with a preprocessing step, which is called prior to every recursive call. The preprocessing uses ranking functions similar to Jurdzinski’s, but with a restricted codomain, to determine all winning regions smaller than a predefined parameter. The combination of the preprocessing step with the recursive call guarantees that McNaughton’s algorithm proceeds in big steps, whose size is bounded from below by the chosen parameter. Higher parameters result in smaller call trees, but to the cost of an expensive preprocessing step. An optimal parameter balances the cost of the recursive call and the preprocessing step, resulting in an improvement of the known upper bound for solving parity games from approximately O(m n^(c/2)) to O(m n^(c/3)).

27th International Conference on Foundations of Software Technology and Theoretical Computer Science (FST TCS 2007) (FSTTCS 2007).

(pdf) (bib)