Linear-time safe-alternating DFS and SCCs

An alternating graph is a directed graph whose vertex set is partitioned into two colour classes, existential and universal. This forms the basic arena for well-known models in formal verification, discrete optimal control, and infinite duration two-player games where Player square and Player circle alternate in a turn-based sliding of a pebble along the arcs they control. We study alternating strongly-connectedness on alternating graphs as a generalization of strongly-connectedness in directed graphs, aiming at providing a linear-time decomposition and a sound structural graph characterization. For this a novel notion of alternating reachability is introduced: Player square attempts to reach vertices without leaving a prescribed subset of the vertices while Player circle works against. This is named safe-alternating reach-ability. It is shown that every alternating graph uniquely decomposes into safe-alternating strongly-connected components, where Player square can visit each vertex within a given component infinitely often without having to ever leave out the component itself. Our main result is a linear-time algorithm for computing this alternating graph decomposition. Both the underlying graph structures and the algorithm generalize the classical decomposition of a directed graph into strongly-connected components, building on the algorithms devised by Tarjan in 1972. Our theory has direct applications e.g. solving well-known infinite duration pebble games faster. Dinneen and Khoussainov showed in 1999 that deciding a given Update Game costs O (mn) time, where n is the number of vertices and m is that of arcs. We solve that task in Theta(m + n) linear time. In turn the complexity of Explicit McNaughton-M & uuml;ller Games improves from cubic to quadratic. (c) 2025 Elsevier Inc. All rights are reserved, including those for text and data mining, AI training, and similar technologies.