Implementation Aspects of a BDD Package Supporting General Decision Diagrams / Dr. Robert Meolic
Sprache des Titels:
Englisch
Original Kurzfassung:
A binary decision diagram (BDD) is a directed, acyclic, binary graph with one root. Originally, BDDs were introduced in the field of digital circuit design as a data structure for efficient representation of Boolean functions. Efficient implementations started to appear in the beginning of '90s. Nowadays, BDDs are also applied to model checking and other verification methods, reachability and reliability analysis, automated reasoning, various combinatorial problems, and many other fields.
A BDD package is a computer library which allows other software to create and manipulate BDDs. All created BDDs are represented simultaneously, and they share as many nodes as possible. Internally, BDD packages use common mechanisms for efficiency: a hash table to store nodes, multiple caches to store already computed results, and heuristic strategies for memory management. Furthermore, a BDD package may offer a manager which allows calculations as if there were multiple copies of the system, i.e. BDDs in different groups do not share nodes and also all internal structures are duplicated. Well-known non-proprietary BDD packages are CUDD and BuDDy.
In the talk, the BDD package Biddy which is developed at the University of Maribor (Slovenia) is introduced. Biddy provides a comprehensible API and an original implementation of memory management. The talk will introduce the functionalities and implementation details of the current version of Biddy. Interesting parts will be explained by live demonstrations. General decision diagrams will be discussed on a theoretical level.
Forschungs-