Name
Abstract | ||
|---|---|---|
In this work we investigate a symbolic heuristic search algorithm in a model checker. The symbolic search algorithm is built on a system that manipulates binary decision diagrams (BDDs). We study the performance of the search algorithm in terms of the number of BDD operations, size of the BDDs, number of nodes they contain and run-time. We study the heuristic distribution of the state space, we measure effort by computing the mean heuristic value, and we compare single and multiple heuristics. In the case of multiple heuristics, we consider admissible and non-admissible merge strategies. We experiment on problems from a variety of domains. We find that multiple heuristics can perform significantly worse than single heuristics in symbolic search in at least one domain. In general, the effect of the heuristics on the symbolic search in the different domains varies markedly, and we conjecture that the different behaviour is caused by intrinsic differences in the characteristics of the state space. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1007/11527862_22 | SARA |
Keywords | Field | DocType |
multiple abstraction heuristics,multiple heuristics,symbolic search algorithm,search algorithm,symbolic heuristic search algorithm,state space,symbolic verification,mean heuristic value,different behaviour,single heuristics,heuristic distribution,symbolic search,heuristic search,binary decision diagram | The Symbolic,Heuristic,Search algorithm,Model checking,Abstraction,Computer science,Algorithm,Binary decision diagram,Heuristics,State space | Conference |
Volume | ISSN | ISBN |
3607 | 0302-9743 | 3-540-27872-9 |
Citations | PageRank | References |
3 | 0.40 | 21 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kairong Qian | 1 | 63 | 3.38 |
| Albert Nymeyer | 2 | 106 | 9.98 |
| Steven Susanto | 3 | 10 | 0.85 |