Oct 14, 2014: Maryam Hajighasemi: Symbolic model checking using Zero Suppressed Decision Diagram

October 14, 2014Symbolic model checking using Zero Suppressed Decision Diagram
Room: HalB 2FMaryam Hajighasemi

Symbolic model checking, represents the set of states and transition relations as Boolean functions, using Binary Decision Diagrams (BDDs). One alternative to common BDDs are Zero-Suppressed Decision Diagrams (ZDD), which are BDDs based on a new reduction rule. The efficiency of the 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 a fixed set of variables, i.e., the same domain for all possible diagrams. This may result in an increase of size for each diagram. The main goal of this project is to develop an implementation of ZDDs with the 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 different application areas such as reachability algorithm.