Uppsala University Department of Information Technology

Technical Report 2000-014

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

Sergei Vorobyov

June 2000

Abstract:
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.



Uppsala Universitet