### Abstract

Original language | English |
---|---|

Title of host publication | Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016) |

Editors | M. Chechik, J.-F. Raskin |

Place of Publication | Berlin |

Publisher | Springer Verlag |

Pages | 332-348 |

Number of pages | 17 |

ISBN (Print) | 978-3-662-49673-2 |

DOIs | |

State | Published - Apr 2016 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Verlag |

Volume | 9636 |

ISSN (Print) | 0302-9743 |

### Fingerprint

### 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

*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

}

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

Research output: Scientific - peer-review › Conference contribution

TY - CHAP

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

ER -