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 re presentation of Boolean functions. Typically, the underlying Variable order ing is used as an optimization parameter. When finite state machines are re presented by OBDDs the state encoding can be used as an additional optimiza tion parameter. In this paper, we analyze the influence of the state encodi ng on the OBDD-representations of counter-type finite state machines. In pa rticular, we prove lower bounds, derive exact sizes for important encodings and construct a worst-case encoding which leads to exponential-size OBDDs.