Multi-core Symbolic Bisimulation Minimisation

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

    5 Citations (Scopus)
    21 Downloads (Pure)

    Abstract

    Bisimulation minimisation alleviates the exponential growth of transition systems in model checking by computing the smallest system that has the same behavior as the original system according to some notion of equivalence. One popular strategy to compute a bisimulation minimisation is signature-based partition refinement. This can be performed symbolically using binary decision diagrams to allow models with larger state spaces to be minimised. This paper studies strong and branching symbolic bisimulation for labeled transition systems, continuous-time markov chains, and interactive markov chains. We introduce the notion of partition refinement with partial signatures. We extend the parallel BDD library Sylvan to parallelize the signature refinement algorithm, and develop a new parallel BDD algorithm to refine a partition, which conserves previous block numbers and uses a parallel data structure to store block assignments. We also present a specialized BDD algorithm for the computation of inert transitions. The experimental evaluation, based on benchmarks from the literature, demonstrates a speedup of up to 95x sequentially. In addition, we find parallel speedups of up to 17x due to parallelisation with 48 cores. Finally, we present the implementation of these algorithms as a versatile tool that can be customized for bisimulation minimisation in various contexts.
    Original languageEnglish
    Title of host publicationProceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016)
    EditorsM. Chechik, J.-F. Raskin
    Place of PublicationBerlin
    PublisherSpringer
    Pages332-348
    Number of pages17
    ISBN (Print)978-3-662-49673-2
    DOIs
    Publication statusPublished - Apr 2016

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume9636
    ISSN (Print)0302-9743

    Keywords

    • EWI-27828
    • CR-D.2.4
    • Labeled transition systems
    • Continuous-time Markov chains
    • FMT-BDD: BINARY DECISION DIAGRAMS
    • Multi-Core
    • Interactive Markov chains
    • Parallel
    • Bisimulation minimisation
    • Binary Decision Diagrams
    • FMT-MC: MODEL CHECKING

    Fingerprint Dive into the research topics of 'Multi-core Symbolic Bisimulation Minimisation'. Together they form a unique fingerprint.

  • Cite this

    van Dijk, T., & van de Pol, J. C. (2016). Multi-core Symbolic Bisimulation Minimisation. In M. Chechik, & J-F. Raskin (Eds.), Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016) (pp. 332-348). (Lecture Notes in Computer Science; Vol. 9636). Berlin: Springer. https://doi.org/10.1007/978-3-662-49674-9_19