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

被引：35
作者：
Bloem, R [1 ]
Gabow, H
Somenzi, F
机构：
[1] Graz Univ Technol, A-8010 Graz, Austria
[2] Univ Colorado, Boulder, CO USA
来源：
FORMAL METHODS IN SYSTEM DESIGN | 2006年 / 28卷 / 01期
基金：
美国国家科学基金会;
关键词：
symbolic algorithms; strongly connected components; binary decision diagrams; language emptiness; Buchi automata; Streett automata; model checking; depth-first search; breadth-first search;
D O I：
10.1007/s10703-006-4341-z
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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 the previously known quadratic bound. The algorithm can be used to decide emptiness of Buchi 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.
引用
收藏
页码：37 / 56
页数：20
相关论文
共 28 条
[1]  
Aiguo Xie, 1999, 1999 IEEE/ACM International Conference on Computer-Aided Design. Digest of Technical Papers (Cat. No.99CH37051), P37, DOI 10.1109/ICCAD.1999.810617
[2]  
Allen Emerson E., 1986, LICS, P267
[3]  
Bloem R., 1999, Computer Aided Verification. 11th International Conference, CAV'99. Proceedings (Lecture Notes in Computer Science Vol.1633), P222
[4]  
Brayton RK, 1996, LECT NOTES COMPUT SC, V1166, P248, DOI 10.1007/BFb0031812
[5]  
BRYANT RE, 1986, IEEE T COMPUT, V35, P677, DOI 10.1109/TC.1986.1676819
[6]   AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS USING TEMPORAL LOGIC SPECIFICATIONS [J].
CLARKE, EM ;
EMERSON, EA ;
SISTLA, AP .
ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02) :244-263
[7]  
Clarke EM, 1999, MODEL CHECKING, P1
[8]  
CLARKE EM, 1995, DES AUT CON, P427
[9]   MODALITIES FOR MODEL CHECKING - BRANCHING TIME LOGIC STRIKES BACK [J].
EMERSON, EA ;
LEI, CL .
SCIENCE OF COMPUTER PROGRAMMING, 1987, 8 (03) :275-306
[10]  
EVEN S, 1981, J ACM, V28, P1, DOI 10.1145/322234.322235
123