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 proceedingConference contributionAcademicpeer-review

    8 Citations (Scopus)
    156 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 - 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

    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

    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