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 languageEnglish
Title of host publicationDependable Software Engineering: Theories, Tools, and Applications
Subtitle of host publicationFirst International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings
EditorsXuandong Li, Zhiming Liu, Wang Yi
Place of PublicationCham, Switzerland
PublisherSpringer
Pages35-51
Number of pages17
ISBN (Electronic)978-3-319-25942-0
ISBN (Print)978-3-319-25941-3
DOIs
StatePublished - Nov 2015
Event1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2015 - Nanjing, China

Publication series

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

Conference

Conference1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2015
Abbreviated titleSETTA
CountryChina
CityNanjing
Period4/11/156/11/15

Fingerprint

Binary decision diagrams
Model checking
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 X. Li, Z. Liu, & W. Yi (Eds.), Dependable Software Engineering: Theories, Tools, and Applications: First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings (pp. 35-51). (Lecture Notes in Computer Science; Vol. 9409). Cham, Switzerland: Springer. 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.

Dependable Software Engineering: Theories, Tools, and Applications: First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings. ed. / Xuandong Li; Zhiming Liu; Wang Yi. Cham, Switzerland : Springer, 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",
pages = "35--51",
editor = "Xuandong Li and Zhiming Liu and Wang Yi",
booktitle = "Dependable Software Engineering: Theories, Tools, and Applications",

}

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 X Li, Z Liu & W Yi (eds), Dependable Software Engineering: Theories, Tools, and Applications: First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings. Lecture Notes in Computer Science, vol. 9409, Springer, Cham, Switzerland, pp. 35-51, 1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2015, Nanjing, China, 4-6 November. 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.

Dependable Software Engineering: Theories, Tools, and Applications: First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings. ed. / Xuandong Li; Zhiming Liu; Wang Yi. Cham, Switzerland : Springer, 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 - Dependable Software Engineering: Theories, Tools, and Applications

PB - Springer

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 Li X, Liu Z, Yi W, editors, Dependable Software Engineering: Theories, Tools, and Applications: First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings. Cham, Switzerland: Springer. 2015. p. 35-51. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-25942-0_3