We report on the experimental study of the Gurvich-Karzanov-Khachiyan (GKK) algorithm for cyclic games adapted for parity games (equivalent to the µ-calculus model checking), one of the major open problems in complexity and automata theories, computer-aided verification. The algorithms demonstrates excellent polynomial (actually, a sublinear number of iterations) behavior in a substantial (millions) number of experiments with games of sizes up to 20.000 and 6 - 7 colors. It also allows for a natural randomization. We conducted extensive experiments of the randomized GKK algorithm on the `hard' Lebedev-Gurvich's game instances, which force the deterministic version of the algorithm to make exponentially many iterations. With high probability the algorithm converges after just a few hundred iterations (compared with 250 - 260 for deterministic version). This allows for giving up computations that converge slowly and restart with a fresh initial potential transformation. While it remains to be theoretically justified and proved, we present convincing experimental data on dependency of the average and maximal number of iterations on game sizes, outdegrees, colors, initial randomizations.
Available as PDF (448 kB) and compressed Postscript (251 kB)
Download BibTeX entry.