Distributed Branching Bisimulation Minimization by Inductive Signatures

Date Added: Dec 2009
Format: PDF

The idea of distributed model checking of very large systems, is to store the state space in the collective memory of a cluster of workstations, and employ parallel algorithms to analyze the graph. One approach is to generate the graph in a distributed way, and on-the-fly (i.e. during generation) run a distributed model checking algorithm. This is what is done in the DiVinE toolset. This is useful if the system is expected to contain bugs, because the generation can stop after finding the first bug. Another approach is to generate the full state space in a distributed way, and subsequently run a distributed bisimulation reduction algorithm.