Multi-core Symbolic Bisimulation Minimisation

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 4 Citations

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.
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 Verlag
Pages332-348
Number of pages17
ISBN (Print)978-3-662-49673-2
DOIs
StatePublished - Apr 2016

Publication series

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

Fingerprint

Markov processes
Binary decision diagrams
Continuous time systems
Model checking
Parallel algorithms
Data structures

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

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 Verlag. DOI: 10.1007/978-3-662-49674-9_19
van Dijk, Tom ; van de Pol, Jan Cornelis. / Multi-core Symbolic Bisimulation Minimisation. Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016). editor / M. Chechik ; J.-F. Raskin. Berlin : Springer Verlag, 2016. pp. 332-348 (Lecture Notes in Computer Science).
@inproceedings{8148e19515bb47b3aabe1d07f92a5578,
title = "Multi-core Symbolic Bisimulation Minimisation",
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.",
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",
author = "{van Dijk}, Tom and {van de Pol}, {Jan Cornelis}",
year = "2016",
month = "4",
doi = "10.1007/978-3-662-49674-9_19",
language = "English",
isbn = "978-3-662-49673-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "332--348",
editor = "M. Chechik and J.-F. Raskin",
booktitle = "Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016)",
address = "Germany",

}

van Dijk, T & van de Pol, JC 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). Lecture Notes in Computer Science, vol. 9636, Springer Verlag, Berlin, pp. 332-348. DOI: 10.1007/978-3-662-49674-9_19

Multi-core Symbolic Bisimulation Minimisation. / van Dijk, Tom; van de Pol, Jan Cornelis.

Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016). ed. / M. Chechik; J.-F. Raskin. Berlin : Springer Verlag, 2016. p. 332-348 (Lecture Notes in Computer Science; Vol. 9636).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Multi-core Symbolic Bisimulation Minimisation

AU - van Dijk,Tom

AU - van de Pol,Jan Cornelis

PY - 2016/4

Y1 - 2016/4

N2 - 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.

AB - 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.

KW - EWI-27828

KW - CR-D.2.4

KW - Labeled transition systems

KW - Continuous-time Markov chains

KW - FMT-BDD: BINARY DECISION DIAGRAMS

KW - Multi-Core

KW - Interactive Markov chains

KW - Parallel

KW - Bisimulation minimisation

KW - Binary Decision Diagrams

KW - FMT-MC: MODEL CHECKING

U2 - 10.1007/978-3-662-49674-9_19

DO - 10.1007/978-3-662-49674-9_19

M3 - Conference contribution

SN - 978-3-662-49673-2

T3 - Lecture Notes in Computer Science

SP - 332

EP - 348

BT - Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016)

PB - Springer Verlag

CY - Berlin

ER -

van Dijk T, van de Pol JC. Multi-core Symbolic Bisimulation Minimisation. In Chechik M, Raskin J-F, editors, Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016). Berlin: Springer Verlag. 2016. p. 332-348. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-662-49674-9_19