A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking

Tom van Dijk, Ernst Moritz Hahn, D.N. Jansen, Yong Li, Thomas Neele, Mariëlle Ida Antoinette Stoelinga, Andrea Turrini, Lijun Zhang

  • 3 Citations

Abstract

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 languageUndefined
Title of host publicationProceedings of the First International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015)
Place of PublicationSwitzerland
PublisherSpringer International Publishing
Pages35-51
Number of pages17
ISBN (Print)978-3-319-25941-3
DOIs
StatePublished - Nov 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume9409
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Binary decision diagrams
Data structures
Experiments

Keywords

  • EC Grant Agreement nr.: FP7/2007-2013
  • EC Grant Agreement nr.: FP7/318490
  • METIS-315022
  • IR-98405
  • EWI-26446

Cite this

van Dijk, T., Hahn, E. M., Jansen, D. N., Li, Y., Neele, T., Stoelinga, M. I. A., ... Zhang, L. (2015). A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. In Proceedings of the First International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015) (pp. 35-51). (Lecture Notes in Computer Science; Vol. 9409). Switzerland: Springer International Publishing. DOI: 10.1007/978-3-319-25942-0_3

van Dijk, Tom; Hahn, Ernst Moritz; Jansen, D.N.; Li, Yong; Neele, Thomas; Stoelinga, Mariëlle Ida Antoinette; Turrini, Andrea; Zhang, Lijun / A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking.

Proceedings of the First International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015). Switzerland : Springer International Publishing, 2015. p. 35-51 (Lecture Notes in Computer Science; Vol. 9409).

Research output: Scientific - peer-reviewConference contribution

@inbook{9758121f81244ea9bbc7f83e89288ff0,
title = "A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking",
abstract = "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.",
keywords = "EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/318490, METIS-315022, IR-98405, EWI-26446",
author = "{van Dijk}, Tom and Hahn, {Ernst Moritz} and D.N. Jansen and Yong Li and Thomas Neele and Stoelinga, {Mariëlle Ida Antoinette} and Andrea Turrini and Lijun Zhang",
note = "eemcs-eprint-26446 ; http://eprints.ewi.utwente.nl/26446",
year = "2015",
month = "11",
doi = "10.1007/978-3-319-25942-0_3",
isbn = "978-3-319-25941-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer International Publishing",
pages = "35--51",
booktitle = "Proceedings of the First International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015)",

}

van Dijk, T, Hahn, EM, Jansen, DN, Li, Y, Neele, T, Stoelinga, MIA, Turrini, A & Zhang, L 2015, A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. in Proceedings of the First International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015). Lecture Notes in Computer Science, vol. 9409, Springer International Publishing, Switzerland, pp. 35-51. DOI: 10.1007/978-3-319-25942-0_3

A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. / van Dijk, Tom; Hahn, Ernst Moritz; Jansen, D.N.; Li, Yong; Neele, Thomas; Stoelinga, Mariëlle Ida Antoinette; Turrini, Andrea; Zhang, Lijun.

Proceedings of the First International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015). Switzerland : Springer International Publishing, 2015. p. 35-51 (Lecture Notes in Computer Science; Vol. 9409).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking

AU - van Dijk,Tom

AU - Hahn,Ernst Moritz

AU - Jansen,D.N.

AU - Li,Yong

AU - Neele,Thomas

AU - Stoelinga,Mariëlle Ida Antoinette

AU - Turrini,Andrea

AU - Zhang,Lijun

N1 - eemcs-eprint-26446 ; http://eprints.ewi.utwente.nl/26446

PY - 2015/11

Y1 - 2015/11

N2 - 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.

AB - 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.

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EC Grant Agreement nr.: FP7/318490

KW - METIS-315022

KW - IR-98405

KW - EWI-26446

U2 - 10.1007/978-3-319-25942-0_3

DO - 10.1007/978-3-319-25942-0_3

M3 - Conference contribution

SN - 978-3-319-25941-3

T3 - Lecture Notes in Computer Science

SP - 35

EP - 51

BT - Proceedings of the First International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015)

PB - Springer International Publishing

ER -

van Dijk T, Hahn EM, Jansen DN, Li Y, Neele T, Stoelinga MIA et al. A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. In Proceedings of the First International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2015). Switzerland: Springer International Publishing. 2015. p. 35-51. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-25942-0_3