Multi-core symbolic bisimulation minimisation

Tom van Dijk, Jaco van de Pol

Abstract

We introduce parallel symbolic algorithms for bisimulation minimisation, to combat the combinatorial state space explosion along three different paths. Bisimulation minimisation reduces a transition system to the smallest system with equivalent behaviour. We consider strong and branching bisimilarity for interactive Markov chains, which combine labelled transition systems and continuous-time Markov chains. Large state spaces can be represented concisely by symbolic techniques, based on binary decision diagrams. We present specialised BDD operations to compute the maximal bisimulation using signature-based partition refinement. We also study the symbolic representation of the quotient system and suggest an encoding based on representative states, rather than block numbers. Our implementation extends the parallel, shared memory, BDD library Sylvan, to obtain a significant speedup on multi-core machines. We propose the usage of partial signatures and of disjunctively partitioned transition relations, to increase the parallelisation opportunities. Also our new parallel data structure for block assignments increases scalability. We provide SigrefMC, a versatile tool that can be customised for bisimulation minimisation in various contexts. In particular, it supports models generated by the high-performance model checker LTSmin, providing access to specifications in multiple formalisms, including process algebra. The extensive experimental evaluation is based on various benchmarks from the literature. We demonstrate a speedup up to 95x for computing the maximal bisimulation on one processor. In addition, we find parallel speedups on a 48-core machine of another 17x for partition refinement and 24x for quotient computation. Our new encoding of the reduced state space leads to smaller BDD representations, with up to a 5162-fold reduction.
Original languageEnglish
Number of pages21
JournalInternational journal on software tools for technology transfer
DOIs
StateAccepted/In press - 2 Aug 2017

Fingerprint

Markov processes
Binary decision diagrams
Algebra
Explosions
Data structures
Scalability
Specifications

Keywords

  • Bisimulation minimisation
  • Interactive Markov chains
  • Binary decision diagrams
  • Parallel algorithms

Cite this

Dijk, Tom van; Pol, Jaco van de / Multi-core symbolic bisimulation minimisation.

02.08.2017.

Research output: Scientific - peer-reviewArticle

@article{01996af8f71f4f71baeba7b43eb1cb65,
title = "Multi-core symbolic bisimulation minimisation",
abstract = "We introduce parallel symbolic algorithms for bisimulation minimisation, to combat the combinatorial state space explosion along three different paths. Bisimulation minimisation reduces a transition system to the smallest system with equivalent behaviour. We consider strong and branching bisimilarity for interactive Markov chains, which combine labelled transition systems and continuous-time Markov chains. Large state spaces can be represented concisely by symbolic techniques, based on binary decision diagrams. We present specialised BDD operations to compute the maximal bisimulation using signature-based partition refinement. We also study the symbolic representation of the quotient system and suggest an encoding based on representative states, rather than block numbers. Our implementation extends the parallel, shared memory, BDD library Sylvan, to obtain a significant speedup on multi-core machines. We propose the usage of partial signatures and of disjunctively partitioned transition relations, to increase the parallelisation opportunities. Also our new parallel data structure for block assignments increases scalability. We provide SigrefMC, a versatile tool that can be customised for bisimulation minimisation in various contexts. In particular, it supports models generated by the high-performance model checker LTSmin, providing access to specifications in multiple formalisms, including process algebra. The extensive experimental evaluation is based on various benchmarks from the literature. We demonstrate a speedup up to 95x for computing the maximal bisimulation on one processor. In addition, we find parallel speedups on a 48-core machine of another 17x for partition refinement and 24x for quotient computation. Our new encoding of the reduced state space leads to smaller BDD representations, with up to a 5162-fold reduction.",
keywords = "Bisimulation minimisation, Interactive Markov chains, Binary decision diagrams, Parallel algorithms",
author = "Dijk, {Tom van} and Pol, {Jaco van de}",
note = "published online",
year = "2017",
month = "8",
doi = "10.1007/s10009-017-0468-z",

}

Multi-core symbolic bisimulation minimisation. / Dijk, Tom van; Pol, Jaco van de.

02.08.2017.

Research output: Scientific - peer-reviewArticle

TY - JOUR

T1 - Multi-core symbolic bisimulation minimisation

AU - Dijk,Tom van

AU - Pol,Jaco van de

N1 - published online

PY - 2017/8/2

Y1 - 2017/8/2

N2 - We introduce parallel symbolic algorithms for bisimulation minimisation, to combat the combinatorial state space explosion along three different paths. Bisimulation minimisation reduces a transition system to the smallest system with equivalent behaviour. We consider strong and branching bisimilarity for interactive Markov chains, which combine labelled transition systems and continuous-time Markov chains. Large state spaces can be represented concisely by symbolic techniques, based on binary decision diagrams. We present specialised BDD operations to compute the maximal bisimulation using signature-based partition refinement. We also study the symbolic representation of the quotient system and suggest an encoding based on representative states, rather than block numbers. Our implementation extends the parallel, shared memory, BDD library Sylvan, to obtain a significant speedup on multi-core machines. We propose the usage of partial signatures and of disjunctively partitioned transition relations, to increase the parallelisation opportunities. Also our new parallel data structure for block assignments increases scalability. We provide SigrefMC, a versatile tool that can be customised for bisimulation minimisation in various contexts. In particular, it supports models generated by the high-performance model checker LTSmin, providing access to specifications in multiple formalisms, including process algebra. The extensive experimental evaluation is based on various benchmarks from the literature. We demonstrate a speedup up to 95x for computing the maximal bisimulation on one processor. In addition, we find parallel speedups on a 48-core machine of another 17x for partition refinement and 24x for quotient computation. Our new encoding of the reduced state space leads to smaller BDD representations, with up to a 5162-fold reduction.

AB - We introduce parallel symbolic algorithms for bisimulation minimisation, to combat the combinatorial state space explosion along three different paths. Bisimulation minimisation reduces a transition system to the smallest system with equivalent behaviour. We consider strong and branching bisimilarity for interactive Markov chains, which combine labelled transition systems and continuous-time Markov chains. Large state spaces can be represented concisely by symbolic techniques, based on binary decision diagrams. We present specialised BDD operations to compute the maximal bisimulation using signature-based partition refinement. We also study the symbolic representation of the quotient system and suggest an encoding based on representative states, rather than block numbers. Our implementation extends the parallel, shared memory, BDD library Sylvan, to obtain a significant speedup on multi-core machines. We propose the usage of partial signatures and of disjunctively partitioned transition relations, to increase the parallelisation opportunities. Also our new parallel data structure for block assignments increases scalability. We provide SigrefMC, a versatile tool that can be customised for bisimulation minimisation in various contexts. In particular, it supports models generated by the high-performance model checker LTSmin, providing access to specifications in multiple formalisms, including process algebra. The extensive experimental evaluation is based on various benchmarks from the literature. We demonstrate a speedup up to 95x for computing the maximal bisimulation on one processor. In addition, we find parallel speedups on a 48-core machine of another 17x for partition refinement and 24x for quotient computation. Our new encoding of the reduced state space leads to smaller BDD representations, with up to a 5162-fold reduction.

KW - Bisimulation minimisation

KW - Interactive Markov chains

KW - Binary decision diagrams

KW - Parallel algorithms

U2 - 10.1007/s10009-017-0468-z

DO - 10.1007/s10009-017-0468-z

M3 - Article

ER -