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 › Academic › peer-review

8 Citations (Scopus)

151 Downloads (Pure)

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
Subtitle of host publication	First International Symposium, SETTA 2015, Nanjing, China, November 4-6, 2015, Proceedings
Editors	Xuandong Li, Zhiming Liu, Wang Yi
Place of Publication	Cham, Switzerland
Publisher	Springer
Pages	35-51
Number of pages	17
ISBN (Electronic)	978-3-319-25942-0
ISBN (Print)	978-3-319-25941-3
DOIs	https://doi.org/10.1007/978-3-319-25942-0_3
Publication status	Published - 2015
Event	1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2015 - Nanjing, China Duration: 4 Nov 2015 → 6 Nov 2015 Conference number: 1

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	9409
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2015
Abbreviated title	SETTA
Country	China
City	Nanjing
Period	4/11/15 → 6/11/15

Keywords

EC Grant Agreement nr.: FP7/2007-2013
EC Grant Agreement nr.: FP7/318490
Model check
Markov decision process (MDP)
Garbage collection
Binary decision diagrams
Symbolic model check

Access to Document

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

Dijk2015compartive
open
Accepted author version, 252 KB

Fingerprint 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

van Dijk, T., 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 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). Springer. https://doi.org/10.1007/978-3-319-25942-0_3

van Dijk, Tom ; Hahn, Ernst Moritz ; Jansen, David N. ; Li, Yong ; Neele, Thomas ; Stoelinga, Mariëlle ; 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. editor / Xuandong Li ; Zhiming Liu ; Wang Yi. Cham, Switzerland : Springer, 2015. pp. 35-51 (Lecture Notes in Computer Science).

@inproceedings{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, Model check, Markov decision process (MDP), Garbage collection, Binary decision diagrams, Symbolic model check",

author = "{van Dijk}, Tom 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",

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

note = "1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2015, SETTA ; Conference date: 04-11-2015 Through 06-11-2015",

}

van Dijk, T, 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 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/11/15. https://doi.org/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, David N.; Li, Yong; Neele, Thomas; Stoelinga, Mariëlle; 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: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - van Dijk, Tom

AU - Hahn, Ernst Moritz

AU - Jansen, David N.

AU - Li, Yong

AU - Neele, Thomas

AU - Stoelinga, Mariëlle

AU - Turrini, Andrea

AU - Zhang, Lijun

N1 - Conference code: 1

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.

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

KW - EC Grant Agreement nr.: FP7/318490

KW - Model check

KW - Markov decision process (MDP)

KW - Garbage collection

KW - Binary decision diagrams

KW - Symbolic model check

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

A2 - Li, Xuandong

A2 - Liu, Zhiming

A2 - Yi, Wang

PB - Springer

CY - Cham, Switzerland

T2 - 1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2015

Y2 - 4 November 2015 through 6 November 2015

ER -

van Dijk T, Hahn EM, Jansen DN, Li Y, Neele T, Stoelinga M 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). https://doi.org/10.1007/978-3-319-25942-0_3