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

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

    8 Citations (Scopus)
    130 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 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
    Publication statusPublished - Nov 2015
    Event1st International Symposium on Dependable Software Engineering: Theories, Tools, and Applications, SETTA 2015 - Nanjing, China
    Duration: 4 Nov 20156 Nov 2015
    Conference number: 1

    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. https://doi.org/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. 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, 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{\"e}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",
    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",

    }

    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/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, 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: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-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, 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

    A2 - Li, Xuandong

    A2 - Liu, Zhiming

    A2 - Yi, Wang

    PB - Springer

    CY - Cham, Switzerland

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