Distributed Branching Bisimulation Minimization by Inductive Signatures
Open Access
- 15 December 2009
- journal article
- research article
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 14 (14), 32-46
- https://doi.org/10.4204/eptcs.14.3
Abstract
We present a new distributed algorithm for state space minimization modulo branching bisimulation. Like its predecessor it uses signatures for refinement, but the refinement process and the signatures have been optimized to exploit the fact that the input graph contains no iota-loops. The optimization in the refinement process is meant to reduce both the number of iterations needed and the memory requirements. In the former case we cannot prove that there is an improvement, but our experiments show that in many cases the number of iterations is smaller. In the latter case, we can prove that the worst case memory use of the new algorithm is linear in the size of the state space, whereas the old algorithm has a quadratic upper bound. The paper includes a proof of correctness of the new algorithm and the results of a number of experiments that compare the performance of the old and the new algorithms.This publication has 15 references indexed in Scilit:
- Leader Election in Anonymous Rings: Franklin Goes ProbabilisticPublished by Springer Science and Business Media LLC ,2008
- CADP 2006: A Toolbox for the Construction and Analysis of Distributed ProcessesLecture Notes in Computer Science, 2007
- DiVinE – A Tool for Distributed VerificationLecture Notes in Computer Science, 2006
- Verification of a sliding window protocol in μ CRL and PVSFormal Aspects of Computing, 2005
- Distributed state space minimizationInternational Journal on Software Tools for Technology Transfer, 2005
- A distributed algorithm for strong bisimulation reduction of state spacesInternational Journal on Software Tools for Technology Transfer, 2005
- Distributed Applications and Interoperable SystemsPublished by Springer Science and Business Media LLC ,2003
- µCRL: A Toolset for Analysing Algebraic SpecificationsLecture Notes in Computer Science, 2001
- Branching bisimilarity is an equivalence indeed!Information Processing Letters, 1996
- On an improved algorithm for decentralized extrema finding in circular configurations of processorsCommunications of the ACM, 1982