A comparative study of BDD packages for probabilistic symbolic model checking

Tom van Dijk, Ernst Moritz Hahn, David Jansen, Yong Li, Thomas Neele, Mariëlle Stoelinga, Andrea Turrini, Lijun Zhang

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

15 Citations (Scopus)


Symbolic data structures using Binary Decision Diagrams (BDDs) have been successfully used in the last decades to analyse large systems. While various BDD and MTBDD packages have been developed in the community, the CUDD package remains the default choice of most of the symbolic (probabilistic) model checkers. In this paper, we provide the first comparative study of the performance of various BDD/MTBDD packages for this purpose. We provide experimental results for several well-known probabilistic benchmarks and study the effect of several optimisations. Our experiments show that no BDD package dominates on a single core, but that parallelisation yields significant speedups.
Original languageEnglish
Title of host publicationDependable Software Engineering: Theories, Tools, and Applications
EditorsX. Li, Z. Liu, W. Yi
Place of PublicationCham
Number of pages17
ISBN (Electronic)978-3-319-25942-0
ISBN (Print)978-3-319-25941-3
Publication statusPublished - 17 Oct 2015
Externally publishedYes
EventSETTA 2015 First International Symposium - Nanjing, China
Duration: 4 Nov 20155 Nov 2015

Publication series

NameLecture Notes in Computer Science


ConferenceSETTA 2015 First International Symposium


Dive into the research topics of 'A comparative study of BDD packages for probabilistic symbolic model checking'. Together they form a unique fingerprint.

Cite this