Distributed State Space Minimization
Stefan Blom, Simona Orzan · Electronic Notes in Theoretical Computer Science · 2003
In [5], we have given a straightforward distributed implementation of the Kanellakis-Smolka 'naive' algorithm for reducing labeled transition systems modulo strong bisimulation. The algorithm proceeds by partition refinement, that is by computing increasingly fine-grained partitions of the set of states. In this paper we present an optimized distributed implementation, in which the refinements are no longer entirely recomputed in every iteration, but they are computed incrementally. A second significant improvement is the overlap between communication and computation, that results in a better use of both memory and processing power. We discuss these optimizations and show experimental results.