Technical Report 2000-014

Better Decision Algorithms for Parity Games and the Mu-Calculus Model Checking

Sergei Vorobyov

June 2000

We suggest an algorithm with the asymptotically best behavior among currently known algorithms for the problems enumerated in the title, when the number of alternations k is Omega (n1/2+varepsilon), where n is the number of states and 0<varepsilonleq 1/2. The best previously known algorithm [BrowneClarkeJhaLongMarrero97] runs in time O(k2· n· sqrt(n)k) and uses approximately the same space. For comparison, our algorithm for k=n (the most difficult case) runs in time O(n3· (1.61803)k) and uses a small polynomial space. We also show, for the first time, that there is a subexponential randomized algorithms for the problem when k=Omega (n1/2+varepsilon). It was an open problem as to whether such algorithms exist at all.

Available as compressed Postscript (94 kB, no cover)

Download BibTeX entry.