Go to page
 

Bibliographic Metadata

Title
Multi-core symbolic bisimulation minimisation
Authorvan Dijk, Tom ; von de Pol, Jaco
Published in
International Journal on Software Tools for Technology Transfer, 2018, Vol. 20, Issue 2, page 157-177
PublishedSpringer Berlin Heidelberg, 2018
LanguageEnglish
Document typeJournal Article
Keywords (EN)Bisimulation minimisation / Interactive Markov chains / Binary decision diagrams / Parallel algorithms
ISSN1433-2787
URNurn:nbn:at:at-ubl:3-1803 Persistent Identifier (URN)
DOI10.1007/s10009-017-0468-z 
Restriction-Information
 The work is publicly available
Files
Multi-core symbolic bisimulation minimisation [0.65 mb]
Links
Reference
Classification
Abstract (English)

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 95 for computing the maximal bisimulation on one processor. In addition, we find parallel speedups on a 48-core machine of another 17 for partition refinement and 24 for quotient computation. Our new encoding of the reduced state space leads to smaller BDD representations, with up to a 5162-fold reduction.

Stats
The PDF-Document has been downloaded 2 times.
License
CC-BY-License (4.0)Creative Commons Attribution 4.0 International License