A distributed algorithm for strong bisimulation reduction of state spaces

Stefan Blom and Simona Orzan

From the issue entitled "Special section on parallel and distributed model checking"

View Related Documents

Abstract

It is a known problem that state spaces can grow very large, which makes operating on them (including reducing them) difficult because of operational memory shortage. In an attempt to extend 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. By using message passing, the same implementation can be used on both clusters of workstations and large shared memory machines. The algorithm performs reduction of large labeled transition systems modulo strong bisimulation. We justify its correctness and termination and 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 workstations.

Keywords  Strong bisimulation - Distributed tools - State space reduction - Model checking - Multirelational coarsest partition problem

Fulltext Preview

Image of the first page of the fulltext document