The classical algorithm for solving Bu ̈chi 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(n2/logn). We present two new algorithms for Bu ̈chi 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 δ(n)/ log n), where 1 ≤ δ(n) ≤ n is the outdegree of the game graph. Note that this algorithm performs asymptotically better than the classical algorithm if δ(n) = O(log n).
This research was supported in part by the AFOSR MURI grant F49620-00-1-0327 and the NSF ITR grant CCR-0225610 and the SNSF under the Indo-Swiss Joint Research Programme.
GDV: Games in Design and Verification
Chatterjee K, Henzinger TA, Piterman N. Algorithms for Büchi Games. In: ACM; 2006.
Chatterjee, K., Henzinger, T. A., & Piterman, N. (2006). Algorithms for Büchi Games. Presented at the GDV: Games in Design and Verification, ACM.
Chatterjee, Krishnendu, Thomas A Henzinger, and Nir Piterman. “Algorithms for Büchi Games.” ACM, 2006.
K. Chatterjee, T. A. Henzinger, and N. Piterman, “Algorithms for Büchi Games,” presented at the GDV: Games in Design and Verification, 2006.
Chatterjee K, Henzinger TA, Piterman N. 2006. Algorithms for Büchi Games. GDV: Games in Design and Verification.
Chatterjee, Krishnendu, et al. Algorithms for Büchi Games. ACM, 2006.
Link(s) to Main File(s)