Paper Details

A Distributed Algorithm for Strong Bisimulation Reduction of State Spaces
Stefan Blom and Simona Orzan

It is a known problem that state spaces can grow very big, which makes operating with them (including reducing them) difficult, because of memory shortage. In the attempt of extending the size of the state spaces that can be dealt with, we designed and implemented a bisimulation reduction algorithm for distributed memory settings using message-passing communication, such as clusters of workstations. The algorithm performs reduction of large labeled transition systems modulo strong bisimulation. We justify its correctness and termination. We provide an evaluation of the worst-case time and message complexity and some performance data from a prototype implementation. Both theory and practice show that the algorithm scales up with the number of workers.