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 Wang | 1 | 1109 | 61.81 |
Roderick Bloem | 2 | 1708 | 101.26 |
Gary D. Hachtel | 3 | 1069 | 140.38 |
Kavita Ravi | 4 | 422 | 21.67 |
Fabio Somenzi | 5 | 3394 | 302.47 |