An algorithm for strongly connected component analysis in n log n symbolic steps

Abstract

We present a symbolic algorithm for strongly connected component decomposition. The algorithm performs Θ(n log n) image and preimage computations in the worst case, where n is the number of nodes in the graph. This is an improvement over the previously known quadratic bound. The algorithm can be used to decide emptiness of Büchi automata with the same complexity bound, improving Emerson and Lei's quadratic bound, and emptiness of Streett automata, with a similar bound in terms of nodes. It also leads to an improved procedure for the generation of nonemptiness witnesses.