Algorithms for Buchi Games

The classical algorithm for solving Buchi games requires time O(n.m) for game graphs with n states and $m$ edges. For game graphs with constant outdegree, the best known algorithm has running time O(n2log n). We present two new algorithms for Buchi games. First, we give an algorithm that performs at most O(m) more work than the classical algorithm, but runs in time O(n) on infinitely many graphs of constant outdegree on which the classical algorithm requires time O(n2). Second, we give an algorithm with running time O(n.m.log(delta(n))/log(n)), where 1< delta(n) < n is the outdegree of the game graph. Note that this algorithm performs asymptotically better than the classical algorithm if delta(n)=O(log(n)).


PDF