Name
Abstract | ||
|---|---|---|
CTL model checking of complex systems often suffers from the state-explosion problem. We propose using Symbolic Guided Search to avoid difficult-to-represent sections of the state space and prevent state explosion from occurring.Symbolic Guided Search applies hints to guide the exploration of the state space. In this way, the size of the BDDs involved in the computation is controlled, and the truth of a property may be decided before all states have been explored. In this work, we show how hints can be used in the computation of nested fixpoints. We show how to use hints to obtain overapproximations useful for greatest fixpoints, and we present the first results for backward search. Our experiments demonstrate the effectiveness of our approach. |
Year | DOI | Venue |
|---|---|---|
2000 | 10.1145/337292.337306 | DAC |
Keywords | Field | DocType |
ctl model checking,complex system,difficult-to-represent section,state space,greatest fixpoints,state explosion,nested fixpoints,symbolic guided search,state-explosion problem,boolean functions,model checking,computer bugs,data structures,debugging | Boolean function,Data structure,Permission,Model checking,Computer science,Software bug,Algorithm,Real-time computing,Theoretical computer science,State space,Debugging,Computation | Conference |
ISSN | ISBN | Citations |
0738-100X | 1-58113-187-9 | 38 |
PageRank | References | Authors |
1.84 | 22 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Roderick Bloem | 1 | 1708 | 101.26 |
| Kavita Ravi | 2 | 422 | 21.67 |
| Fabio Somenzi | 3 | 3394 | 302.47 |