Title
Divide and Compose: SCC Refinement for Language Emptiness
Abstract
We propose a refinement approach to symbolic SCC analysis, which performs large parts of the computation on abstracted systems, and on small subsets of the state space. For language-emptiness checking, it quickly discards uninteresting parts of the state space; for the remaining states, it adapts the model checking computation to the strength of the SCCs at hand. We present a general framework for SCC refinement, which uses a compositional approach to generate and refine overapproximations. We show that our algorithm significantly outperforms the one of Emerson and Lei.
Year
DOI
Venue
2001
10.1007/3-540-44685-0_31
CONCUR
Keywords
Field
DocType
model checking computation,abstracted system,compositional approach,general framework,symbolic scc analysis,scc refinement,state space,remaining state,language emptiness,refinement approach,language-emptiness checking,model checking
Model checking,Computer science,Decomposition tree,Theoretical computer science,Emptiness,State space,Computation
Conference
ISBN
Citations 
PageRank 
3-540-42497-0
6
0.57
References 
Authors
14
5
Name
Order
Citations
PageRank
Chao Wang1110961.81
Roderick Bloem21708101.26
Gary D. Hachtel31069140.38
Kavita Ravi442221.67
Fabio Somenzi53394302.47