Buchi automata in formal software verification
The fastest theoretical algorithm to solve Büchi Games in game graphs is presented in  [1]  and runs in $O(n^2)$: The algorithm uses a hierarchical decomposition approach. An easier folklore algorithm with $O(mn)$ running time using just the attractor concept is mentioned.

Büchi Games on graphs should be in linear time after computing the strongly connected components of the graph.

[1] Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition. J. ACM, (2014)