On the Influence of the State Encoding on OBDD-Representations of Finite State Machines

¹ FB IV – Informatik, Universität Trier, 54286 Trier, Germany; meinel@uni-trier.de.
² Zentrum Mathematik, TU München, 80290 München, Germany; theobald@mathematik.tu-muenchen.de.

Received: June 1997
Accepted: July 1998

Abstract

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 sizes for important encodings and construct a worst-case encoding which leads to exponential-size OBDDs.

Résumé

Les diagrammes de décision binaire (Ordered Binary Decision Diagrams, OBDD) sont une structure de données importante pour la représentation de fonctions booléennes. Habituellement l'ordre des variables est le paramètre à optimiser. Quand des automates finis sont représentés par des OBDD, le codage des états peut lui aussi être optimisé. Nous analysons l'influence du codage des états sur la représentation des machines à compteurs par des OBDD. En particulier, nous prouvons des bornes inférieures, nous calculons la taille exacte de codages importants et nous construisons un codage qui mène à des OBDD de taille exponentielle.