AbstractWe describe a randomized algorithm for Parity Games (equivalent to the Mu-Calculus Model Checking), which runs in expected time 2O(k1/(1+2epsilon)) when k is Omega(n1/2+epsilon), n is the number of vertices, and 0 < epsilon <= 1/2. That is, our algorithm is subexponential in the number of colors k of the game graph provided that k is not too small. 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.
Categories and Subject Descriptors: F.2 [Analysis of Algorithms and Problem Complexity]
Additional Key Words and Phrases: parity games, mu-calculus model checking, decision complexity, subexponential decision algorithm
Selected references
- Anne Condon. The complexity of stochastic games. Information and Computation, 96(2):203-224, February 1992.
- Marcin Jurdzi\'nski. Deciding the winner in parity games is in UP \cap co-UP. Information Processing Letters, 68(3):119-124, 15 November 1998.
- Gil Kalai. A subexponential randomized simplex algorithm (extended abstract). In Proceedings of the Twenty-Fourth Annual ACM Symposium on the Theory of Computing, pages 475-482, Victoria, British Columbia, Canada, 4-6 May 1992.
- Walter Ludwig. A subexponential randomized algorithm for the simple stochastic game problem. Information and Computation, 117(1):151-155, 15 February 1995.
- Uri Zwick and Mike Paterson. The complexity of mean payoff games on graphs. Theoretical Computer Science, 158(1-2):343-359, 20 May 1996. Mathematical Games.