The Binary Decision Diagram: Abstraction and Implementation
| Main Author: | |
|---|---|
| Language: | English |
| Published: |
The Ohio State University / OhioLINK
2018
|
| Subjects: | |
| Online Access: | http://rave.ohiolink.edu/etdc/view?acc_num=osu152414624378423 |
| id |
ndltd-OhioLink-oai-etd.ohiolink.edu-osu152414624378423 |
|---|---|
| record_format |
oai_dc |
| spelling |
ndltd-OhioLink-oai-etd.ohiolink.edu-osu1524146243784232021-08-03T07:06:26Z The Binary Decision Diagram: Abstraction and Implementation Asim, Saad F., Asim Computer Science Binary Decision Diagram Computer Science A Boolean formula in predicate logic is an expression on Boolean variables that evaluates to either True or False. This fundamental construct has many important applications in computer science, such as the validation of system models. However, as these models are extended, the number of variables in the expression grows exponentially, creating problems for efficient representation. Traditional data structures used to represent Boolean formulas containing a large number of variables become especially inefficient for operations such as checking whether the expression is satisfiable. Binary Decision Diagrams (BDDs), a relatively new data structure used to represent Boolean formulas, enjoy several advantages over these traditional data structures. First, BDDs are often compact, even for Boolean formulas involving many variables. Furthermore, they are canonical representations for Boolean formulas, meaning equivalence checking can be done effectively. Finally, they can be efficiently combined to represent more complex formulas.The goal of this study is to develop a provably correct software realization of the BDD. This realization can be verified with respect to precise specifications using proofs, not just checked using test cases as is typical with software implementations. Achieving this goal requires solving problems in three phases: designing a behavioral specification based on a mathematical model, developing a layered implementation in Java, and establishing a correspondence between the implementation and model. The full implementation of a provably correct BDD realization provides an efficient method of representing system models that users can be completely confident in using. 2018-08-14 English text The Ohio State University / OhioLINK http://rave.ohiolink.edu/etdc/view?acc_num=osu152414624378423 http://rave.ohiolink.edu/etdc/view?acc_num=osu152414624378423 unrestricted This thesis or dissertation is protected by copyright: all rights reserved. It may not be copied or redistributed beyond the terms of applicable copyright laws. |
| collection |
NDLTD |
| language |
English |
| sources |
NDLTD |
| topic |
Computer Science Binary Decision Diagram Computer Science |
| spellingShingle |
Computer Science Binary Decision Diagram Computer Science Asim, Saad F., Asim The Binary Decision Diagram: Abstraction and Implementation |
| author |
Asim, Saad F., Asim |
| author_facet |
Asim, Saad F., Asim |
| author_sort |
Asim, Saad F., Asim |
| title |
The Binary Decision Diagram: Abstraction and Implementation |
| title_short |
The Binary Decision Diagram: Abstraction and Implementation |
| title_full |
The Binary Decision Diagram: Abstraction and Implementation |
| title_fullStr |
The Binary Decision Diagram: Abstraction and Implementation |
| title_full_unstemmed |
The Binary Decision Diagram: Abstraction and Implementation |
| title_sort |
binary decision diagram: abstraction and implementation |
| publisher |
The Ohio State University / OhioLINK |
| publishDate |
2018 |
| url |
http://rave.ohiolink.edu/etdc/view?acc_num=osu152414624378423 |
| work_keys_str_mv |
AT asimsaadfasim thebinarydecisiondiagramabstractionandimplementation AT asimsaadfasim binarydecisiondiagramabstractionandimplementation |
| _version_ |
1719453737632661504 |