Thesis Details
Knihovna pro binární rozhodovací diagramy
Efficient manipulation of Boolean functions is an important component of many computer-aided design task. As a data structure for representing and manipulating Boolean functions, Binary Decision Diagrams are commonly used. These diagrams are commonly used in many fields such as model checking, system verification, circuit design, etc. In this thesis we describe these diagrams and there are present their modifications. Furthermore, this paper present and describes techniques for effective handling and representation of binary decision diagrams. This thesis describes the design and implementation of library that will work with these diagrams. It is further discussed how the developed library can be used within the library VATA for manipulating tree automata. Finally, the library was compared with well known and heavily optimized library CUDD, which is public and with library CacBDD. The experimental results showed that the performance of the proposed library is quite close to that of CUDD a CacBDD (has comparable and mostly even slightly better performance).
Boolean functions, symbolic manipulation, binary decision diagrams.
Kreslíková Jitka, doc. RNDr., CSc. (DIFS FIT BUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT), člen
Růžička Richard, doc. Ing., Ph.D., MBA (DCSY FIT BUT), člen
Šlapal Josef, prof. RNDr., CSc. (DADM FME BUT), člen
Zbořil František, doc. Ing., Ph.D. (DITS FIT BUT), člen
@mastersthesis{FITMT18227,
author = "Petr Jank\r{u}",
type = "Master's thesis",
title = "Knihovna pro bin\'{a}rn\'{i} rozhodovac\'{i} diagramy",
school = "Brno University of Technology, Faculty of Information Technology",
year = 2015,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/18227/"
}