Abstract

In symbolic model checking, decision diagrams are used to store all reachable states of a computer program. The size of decision diagrams is highly dependent on the used variable ordering of the underlying structure, a matrix that represents transitions and variables of the system. The model checker LTSmin [16] currently uses a custom implementation to find a good variable ordering, but with this implementation LTSmin fails to produce good orderings for larger matrices. Therefore, this paper explores existing bandwidth, profile and wavefront reduction algorithms and properties, including algorithms used in the field of Structural Analysis in Civil Engineering. We will present the solution to apply existing algorithms to our rectangular matrices in symbolic model checking.

References

1. New Metrics for Static Variable Ordering in Decision Diagrams (Digital version available here)
2. Parallelization of reordering algorithms for bandwidth and wavefront reduction (Digital version available here)
3. reducing the total bandwidth of a sparse unsymmetric matrix (Digital version available here)

Additional Resources

1. The paper
2. good.txt
3. bad.txt