University of Twente Student Theses

Login

Symbolic model checking using Zero-suppressed Decision Diagrams

Haji Ghasemi, Maryam (2014) Symbolic model checking using Zero-suppressed Decision Diagrams.

[img]
Preview
PDF
1MB
Abstract:Symbolic model checking represents the set of states and transition relation as Boolean functions, using Binary Decision Diagrams (BDDs). One alternative to common BDDs are Zerosuppressed Decision Diagrams (ZDDs), which are BDDs based on a new reduction rule. The efficiency of ZDD representation, in comparison with the original BDD, is noticeable especially for sparse state spaces, in which the actual number of existing states is much smaller than the total number of possible states. To the best of our knowledge, the current implementation for ZDDs is using fixed set of variables, i.e., domain for all possible diagrams. This may result in increase of size for each diagram. The main goal of this project is to develop an implementation of ZDDs with possibility of having different domains for specific diagrams. The secondary goal is to investigate the efficiency of ZDDs in comparison with BDDs, e.g. memory usage and running time, for reachability algorithm.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:http://purl.utwente.nl/essays/66388
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page