We suggest and experimentally test a new approach to solving the Parity Games problem, equivalent to the propositional modal µ-calculus, a fundamental problem in automata, games, complexity theories, as well as in practical computer-aided verification, whose precise computational complexity is a long-standing open question.
Based on the algorithm due to Gurvich, Karzanov, and Khachiyan for solving the more general Mean Payoff Games, we make an adaptation and optimization for parity games, implement it in Knuth's system CWEB of "literate programming" using C++.
The algorithm is less known in the model-checking community and is based on different ideas, as compared to the well-investigated ideas including fixpoint iteration, strategy improvement, dynamic programming.
Run on a considerable number (several millions) of randomly generated test game instances with up to 20.000 vertices and 6 - 7 colors, the algorithm demonstrates a rapid convergence with sublinear number of iterations. Moreover, unlike other known algorithms, for which examples of exponential behaviors are known, our algorithm admits internal randomization, which gives improvements in our tests and may help the algorithm to avoid bad cases.
Our experiments strongly suggest that the algorithm is polynomial on the average under reasonable distributions, which remains to be explained in further studies.
This report contains results of the summer project done by the first author under the supervision and with participation of the second author. It represents an ongoing project, the new updates will be available from http://www.csd.uu.se/~vorobyov/eb-gkk
Available as compressed Postscript (311 kB)
Download BibTeX entry.