A uniform framework for weighted decision diagrams and its implementation

From International Center for Computational Logic

Toggle side column

A uniform framework for weighted decision diagrams and its implementation

Jörn OssowskiJörn Ossowski,  Christel BaierChristel Baier
Jörn Ossowski, Christel Baier
A uniform framework for weighted decision diagrams and its implementation
International Journal on Software Tools for Technology Transfer, 10(5):425--441, 2008
  • KurzfassungAbstract
    This paper 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 to 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 multi-valued 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, with or without edge-attributes, and their zero-suppressed variants.
  • Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science
@article{OB2008,
  author  = {J{\"{o}}rn Ossowski and Christel Baier},
  title   = {A uniform framework for weighted decision diagrams and its
             implementation},
  journal = {International Journal on Software Tools for Technology Transfer},
  volume  = {10},
  number  = {5},
  year    = {2008},
  pages   = {425--441},
  doi     = {10.1007/S10009-008-0069-Y}
}