Variable ordering and selection of FSM traversal

The authors consider the problem of variable ordering in algorithms for verification of finite state machines (FSMs) for which the traversal is based on BDD (binary decision diagram) representation and image computation via implicit enumeration. They treat two separate BDD ordering problems: (1) minimization of the representation of the next state function and the representation of the set of reachable states, and (2) a selection heuristic to reduce the complexity of the image computation problem by dynamic selection of the implicit enumeration splitting variables. In both problems they present theoretical results based on the algebraic structure of the next state functions, heuristic ordering methods, and favorable experimental results for problems with significant algebraic structure.<>