 |
| | | | | Erläuterung | | Binary Decision Diagrams (BDDs) sind eine Datenstruktur zur kompakten Darstellung von booleschen Funktionen. Eine boolesche Funktion ist eine Funktion, deren Argumente Wahrheitswerte darstellen und deren Ergebnis ebenfalls ein Wahrheitswert ist. Ein zwei-Bit-Vergleicher kann beispielsweise als Funktion mit 4 Variablen – jede steht für ein Bit – dargestellt werden. Eine direkte Datenstruktur zur Darstellung solcher Funktionen ist ein binärer Entscheidungsbaum. Dort sind die Variablen als Knoten des Baumes modelliert, die möglichen Variablenbelegungen als Kanten und die Funktionswerte bei Belegung aller Variablen mit bestimmten Werten jeweils als Blatt des entsprechenden Pfades durch den Baum.
BDDs funktionieren nach dem gleichen Prinzip wie Entscheidungsbäume, nur werden gleiche Teilbäume zusammengefasst. Die Variante der Ordered Binary Decision Diagrams (OBDDs) haben als zusätzliche Bedingung, dass die Variablen auf jedem Pfad von der Wurzel zu einem Blatt in der gleichen Reihenfolge auftreten (bei BDDs kann die Reihenfolge auf verschiedenen Pfaden durchaus variieren).
OBDDs sind eine der im Model Checking am häufigsten verwendeten Datenstrukturen.
| |
| | | | | | | | | | | | Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben. |
|
| | | | | | | | Binary Decision Diagrams | | | | |  | Erläutert Technologien | | | | | | | | | |
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
