High-density reachability analysis
Kavita Ravi, Fabio Somenzi · 1995
We address the problem of reachability analysis for large nite state systems. Symbolic techniques have revolutionized reacha-bility analysis but still have limitations in traversing large sys-tems. We present techniques to improve the symbolic breadth-rst traversal and compute a lower bound on the reachable states. We identify the problem as one of density during traversal and our techniques seek to improve the same. Our results show a marked improvement on the existing breadth-rst traversal meth-ods. 1