A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking

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

doi:10.1007/978-3-319-25942-0_3

A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

16 Citations (Scopus)

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 language	English
Title of host publication	Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings
Pages	35-51
Number of pages	17
DOIs	https://doi.org/10.1007/978-3-319-25942-0_3
Publication status	Published - 2015
Externally published	Yes

Access to Document

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

https://doi.org/10.1007/978-3-319-25942-0_3

Cite this

Dijk, T. V., Hahn, E. M., Jansen, D. N., Li, Y., Neele, T., Stoelinga, M., Turrini, A., & Zhang, L. (2015). A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. In Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings (pp. 35-51) https://doi.org/10.1007/978-3-319-25942-0_3

@inproceedings{9c8825673a3342d7a64d93ae6e274cef,

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.",

author = "Dijk, {Tom van} and Hahn, {Ernst Moritz} and Jansen, {David N.} and Yong Li and Thomas Neele and Mari{\"e}lle Stoelinga and Andrea Turrini and Lijun Zhang",

year = "2015",

doi = "10.1007/978-3-319-25942-0_3",

language = "English",

pages = "35--51",

booktitle = "Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings",

}

Dijk, TV, Hahn, EM, Jansen, DN, Li, Y, Neele, T, Stoelinga, M, Turrini, A & Zhang, L 2015, A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. in Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings. pp. 35-51. https://doi.org/10.1007/978-3-319-25942-0_3

A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking. / Dijk, Tom van; Hahn, Ernst Moritz; Jansen, David N. et al.
Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings. 2015. p. 35-51.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Dijk, Tom van

AU - Hahn, Ernst Moritz

AU - Jansen, David N.

AU - Li, Yong

AU - Neele, Thomas

AU - Stoelinga, Mariëlle

AU - Turrini, Andrea

AU - Zhang, Lijun

PY - 2015

Y1 - 2015

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.

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

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

M3 - Conference contribution

SP - 35

EP - 51

BT - Dependable Software Engineering: Theories, Tools, and Applications - First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings

ER -

A Comparative Study of BDD Packages for Probabilistic Symbolic Model Checking

Abstract

Access to Document

Fingerprint

Cite this