Skip to Main Content
Frequently Asked Questions
Submit an ETD
Global Search Box
Need Help?
Keyword Search
Participating Institutions
Advanced Search
School Logo
Files
File List
2018_MS_SaadAsim.pdf (979.08 KB)
ETD Abstract Container
Abstract Header
The Binary Decision Diagram: Abstraction and Implementation
Author Info
Asim, Saad F, Asim
Permalink:
http://rave.ohiolink.edu/etdc/view?acc_num=osu152414624378423
Abstract Details
Year and Degree
2018, Master of Science, Ohio State University, Computer Science and Engineering.
Abstract
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.
Committee
Paul Sivilotti (Advisor)
Neelam Soundarajan (Committee Member)
Pages
174 p.
Subject Headings
Computer Science
Keywords
Binary Decision Diagram
;
Computer Science
Recommended Citations
Refworks
EndNote
RIS
Mendeley
Citations
Asim, Asim, S. F. (2018).
The Binary Decision Diagram: Abstraction and Implementation
[Master's thesis, Ohio State University]. OhioLINK Electronic Theses and Dissertations Center. http://rave.ohiolink.edu/etdc/view?acc_num=osu152414624378423
APA Style (7th edition)
Asim, Asim, Saad.
The Binary Decision Diagram: Abstraction and Implementation.
2018. Ohio State University, Master's thesis.
OhioLINK Electronic Theses and Dissertations Center
, http://rave.ohiolink.edu/etdc/view?acc_num=osu152414624378423.
MLA Style (8th edition)
Asim, Asim, Saad. "The Binary Decision Diagram: Abstraction and Implementation." Master's thesis, Ohio State University, 2018. http://rave.ohiolink.edu/etdc/view?acc_num=osu152414624378423
Chicago Manual of Style (17th edition)
Abstract Footer
Document number:
osu152414624378423
Download Count:
854
Copyright Info
© 2018, all rights reserved.
This open access ETD is published by The Ohio State University and OhioLINK.