Title:Linear Time Algorithm for Update Games via Strongly-Trap-Connected Components

Abstract:An arena is a finite directed graph whose vertices are divided into two classes, i.e $V=V_{\square}\cup V_{\bigcirc}$; this forms the basic playground for a plethora of 2-player infinite pebble-games. We introduce and study a refined notion of reachability for arenas, named \emph{trap-reachability}, where Player~$\square$ attempts to reach vertices without leaving a prescribed subset $V'\subseteq V$, while Player~$\bigcirc$ works against. It is shown that every arena decomposes into \emph{strongly-trap-connected components (STCCs)}. Our main result is a linear time algorithm for computing this unique decomposition. Both the graph structures and the algorithm generalize the classical decomposition of a directed graph into its strongly-connected components (SCCs). The algorithm builds on a generalization of the depth-first search (DFS), taking inspiration from Tarjan's SCC{s} classical algorithm. The structures of palm-trees and jungles described in Tarjan's original paper need to be revisited and generalized (i.e tr-palm-trees and tr-jungles) in order to handle the 2-player infinite pebble-game's setting. This theory has direct applications in solving Update Games (UGs) faster. Dinneen and Khoussainov showed in 1999 that deciding who's the winner in a given UG costs $O(mn)$ time, where $n$ is the number of vertices and $m$ is that of arcs. We solve that problem in $\Theta(m+n)$ linear time. The result is obtained by observing that the UG is a win for Player~$\square$ if and only if the arena comprises one single STCC. It is also observed that the tr-palm-tree returned by the algorithm encodes routing information that an $\Theta(n)$-space agent can consult to win the UG in $O(1)$ time per move. Finally, the polynomial-time complexity for deciding Explicit McNaughton-Muller Games is also improved, from cubic to quadratic.