An efficient heuristic for state encoding minimizing the BDD representations of the transition relations of finite state machines

An efficient representation of the (smoothed) transition relation of a synchronous finite state machine (FSM) speeds up the traversal based symbolic verification and the functional simulation of the FSM. When using reduced ordered binary decision diagrams (BDDs), dynamic reordering algorithms are applied in order to keep the sizes of the BDDs tractable. However when FSMs are represented by BDDs, the state encoding can be used as an additional optimization criterion. In this paper, we present a new algorithm for state encoding of FSMs that minimizes the BDD representations of the corresponding (smoothed) transition relations. Experimental results show the approach to be very efficient.