Skip to Main Content
 

Global Search Box

 
 
 
 

ETD Abstract Container

Abstract Header

The Binary Decision Diagram: Abstraction and Implementation

Asim, Saad F, Asim

Abstract Details

2018, Master of Science, Ohio State University, Computer Science and Engineering.
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.
Paul Sivilotti (Advisor)
Neelam Soundarajan (Committee Member)
174 p.

Recommended Citations

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)