On the influence of the state encoding on OBDD-representations of finite state machines
Ordered binary decision diagrams are an important data structure for the representation of Boolean functions. Typically, the underlying variable ordering is used as an optimization parameter. When finite state machines are represented by OBDDs the state encoding can be used as an additional optimization parameter. In this paper, we analyze the influence of the state encoding on the OBDD-representations of counter-type finite state machines. In particular, we prove lower bounds, derive exact...
Page 1