A deterministic subexponential algorithm for solving parity games

ABSTRACT

The existence of polynomial time algorithms for the solution of parity games is a major open problem. The fastest known algorithms for the problem are randomized algorithms that run in subexponential time. These algorithms are all ultimately based on the randomized subexponential simplex algorithms of Kalai and of Matoušek, Sharir and Welzl. Randomness seems to play an essential role in these algorithms. We use a completely different, and elementary, approach to obtain a deterministic subexponential algorithm for the solution of parity games. Our deterministic algorithm is almost as fast as the randomized algorithms mentioned above.

REFERENCES

• 1: Henrik Björklund , Sven Sandberg , Sergei G. Vorobyov, A Discrete Subexponential Algorithm for Parity Games, Proceedings of the 20th Annual Symposium on Theoretical Aspects of Computer Science, p.663-674, February 27-March 01, 2003
• 2: {BSV04} H. Bjorklund, S. Sandberg, and S. Vorobyov. Randomized subexponential algorithms for infinite games. Technical Report 2004--09, DIMACS, 2004.
• 3: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 4: Krishnendu Chatterjee , Marcin Jurdziński , Thomas A. Henzinger, Quantitative stochastic parity games, Proceedings of the fifteenth annual ACM-SIAM symposium on Discrete algorithms, January 11-14, 2004, New Orleans, Louisiana
• 5: Anne Condon, The complexity of stochastic games, Information and Computation, v.96 n.2, p.203-224, Feb. 1992 [doi>10.1016/0890-5401(92)90048-K]
• 6: Luca de Alfaro , Rupak Majumdar, Quantitative solution of omega-regular games, Journal of Computer and System Sciences, v.68 n.2, p.374-397, March 2004 [doi>10.1016/j.jcss.2003.07.009]
• 7: E. A. Emerson , C. S. Jutla, Tree automata, Mu-Calculus and determinacy, Proceedings of the 32nd annual symposium on Foundations of computer science, p.368-377, September 1991, San Juan, Puerto Rico [doi>10.1109/SFCS.1991.185392]
• 8: E. Allen Emerson , Charanjit S. Jutla , A. Prasad Sistla, On Model-Checking for Fragments of µ-Calculus, Proceedings of the 5th International Conference on Computer Aided Verification, p.385-396, June 28-July 01, 1993
• 9: {Eme96} E. A. Emerson. Model checking and mu-calculus. In N. Immerman and Ph. C. Kolaitis, editors, Descriptive Complexity and Finite Models, volume 31 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 185--214. American Mathematical Society, 1996.
• 10: {GTW02} E. Grädel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Infinite Games. A Guide to Current Research, volume 2500 of LNCS. Springer, 2002.
• 11: {Hal04} N. Halman. Discrete and Lexicographic Helly The-orems and Their Relations to LP-type Problems. PhD thesis, Tel-Aviv University, 2004.
• 12: Marcin Jurdziński, Deciding the winner in parity games is in UP ∩ co-UP, Information Processing Letters, v.68 n.3, p.119-124, Nov. 15, 1998 [doi>10.1016/S0020-0190(98)00150-1]
• 13: Marcin Jurdzinski, Small Progress Measures for Solving Parity Games, Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, p.290-301, February 01, 2000
• 14: Gil Kalai, A subexponential randomized simplex algorithm (extended abstract), Proceedings of the twenty-fourth annual ACM symposium on Theory of computing, p.475-482, May 04-06, 1992, Victoria, British Columbia, Canada [doi>10.1145/129712.129759]
• 15: Valerie King , Orna Kupferman , Moshe Y. Vardi, On the Complexity of Parity Word Automata, Proceedings of the 4th International Conference on Foundations of Software Science and Computation Structures, p.276-286, April 02-06, 2001
• 16: Walter Ludwig, A subexponential randomized algorithm for the simple stochastic game problem, Information and Computation, v.117 n.1, p.151-155, Feb. 15, 1995 [doi>10.1006/inco.1995.1035]
• 17: {McN93} R. McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65(2):149--184, 1993.
• 18: {MSW96} J. Matoušek, M. Sharir, and E. Welzl. A subexponential bound for linear programming. Algorithmica, 16(4/5):498--516, 1996.
• 19: {Obd03} J. Obdržálek. Fast mu-calculus model checking when tree-width is bounded. In International Conference on Computer-Aided Verification, CAV 2003, volume 2725 of LNCS, pages 80--92. Springer, 2003.
• 20: Jens Vöge , Marcin Jurdzinski, A Discrete Strategy Improvement Algorithm for Solving Parity Games, Proceedings of the 12th International Conference on Computer Aided Verification, p.202-215, July 15-19, 2000
• 21: Wiesław Zielonka, Infinite games on finitely coloured graphs with applications to automata on infinite trees, Theoretical Computer Science, v.200 n.1-2, p.135-183, June 28, 1998 [doi>10.1016/S0304-3975(98)00009-7]
• 22: Uri Zwick , Mike Paterson, The complexity of mean payoff games on graphs, Theoretical Computer Science, v.158 n.1-2, p.343-359, May 20, 1996 [doi>10.1016/0304-3975(95)00188-3]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems

Additional Classification:
  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.1 Numerical Algorithms and Problems

General Terms:
Algorithms, Theory