Erik Kemp - Bandwith reduction to find an optimal variable ordering

author:Erik Kemp
title:Bandwith reduction to find an optimal variable ordering
keywords:bandwidth reduction binary decision diagrams
topics:Case studies and Applications, Graphs, Algorithms and Data Structures
committee:prof.dr. J.C. van de Pol (1st supervisor)
J.J.G. Meijer MSc
graduation date:21 June 2015

Computer Science final project

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