An O(n^2) Time Algorithm for Alternating B\"uchi Games

TL;DR

This paper introduces an $O(n^2)$ time algorithm for solving B{"u}chi games on graphs, significantly improving previous bounds and enabling efficient dynamic updates in game graphs.

Contribution

The authors present the first $O(n^2)$ time algorithm for B{"u}chi games on graphs, surpassing the longstanding $ ilde{O}(n imes m)$ bound, and develop a dynamic algorithm for maintaining winning sets.

Findings

Achieved $O(n^2)$ time complexity for B{"u}chi game solving.

Extended the technique to compute maximal end-component decomposition in $O(n^2)$.

Developed a dynamic algorithm with $O(n)$ amortized update time for winning set maintenance.

Abstract

Computing the winning set for B{\"u}chi objectives in alternating games on graphs is a central problem in computer aided verification with a large number of applications. The long standing best known upper bound for solving the problem is $\tilde{O}(n \cdot m)$, where $n$ is the number of vertices and $m$ is the number of edges in the graph. We are the first to break the $\tilde{O}(n\cdot m)$ bound by presenting a new technique that reduces the running time to $O(n^2)$. This bound also leads to an $O(n^2)$ algorithm time for computing the set of almost-sure winning vertices in alternating games with probabilistic transitions (improving an earlier bound of $\tilde{O}(n\cdot m)$) and in concurrent graph games with constant actions (improving an earlier bound of $O(n^3)$). We also show that the same technique can be used to compute the maximal end-component decomposition of a graph in time $O(n^2)$. Finally, we show how to maintain the winning set for B{\"u}chi objectives in alternating games under a sequence of edge insertions or a sequence of edge deletions in O(n) amortized time per operation. This is the first dynamic algorithm for this problem.