We present a symbolic algorithm for strongly connected component
decomposition. The algorithm performs Theta(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 Xie and Beerel's
quadratic bound. The algorithm can be used to decide emptiness of
Buechi automata with the same complexity bound, improving Emerson
and Lei's quadratic bound. It can also be used to decide emptiness
of Streett automata, with the same bound in terms of nodes.
