A uniform framework for weighted decision diagrams and its implementation

1 This papers introduces a generic framework for OBDD variants with weighted edges. It covers many boolean and multi-valued OBDD-variants that have been studied in the literature and applied for the symbolic representation and manipulation of discrete functions. Our framework supports reasoning about reducedness and canonicity of new OBDD-variants and provides a platform for the implementation and comparison of OBDD-variants. Furthermore, we introduce a new multivalued OBDD-variant, called normalized algebraic decision diagram, which supports min/max-operations and turns out to be very useful for, e.g., integer linear programming and model checking probabilistic systems. Finally, we explain the main features of an implementation of a newly developed BDD-package, called JINC, which relies on our generic notion of weighted decision diagrams, and realizes various synthesis algorithms, reordering techniques and transformation algorithms for boolean and multi-terminal OBDDs, without or with...

• Type: Journal
• Year: 2008
• Where: STTT
• Authors: Jörn Ossowski, Christel Baier
• Keywords: Generic Framework, Multi-valued Obdd-variants, OBDD Variants, STTT 2008