An n log n Symbolic Algorithm for Strongly Connected Component Analysis

Roderick Bloem, Harold N. Gabow and Fabio Somenzi

To appear at Formal Methods in Computer Aided Design (FMCAD00), Austin, Texas, November 1-3, 2000


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.

Server START Conference Manager
Update Time 26 Jun 2000 at 16:35:38
Start Conference Manager
Conference Systems