Jan Martens: A parallel algorithm for bisimulation partition refinement

Event Details

The notion of strong bisimilarity on LTSs is an equivalence that expresses whether states have the same behavior. In their pioneering work Kanellakis and Smolka proposed a partition refinement algorithm that finds the coarsest partition of bisimilar states. We propose a parallel version of this algorithm that performs this partition refinement on an LTS with n states and m labels in O(n) steps on max(n,m) CRCW PRAM processors. Additionally, it does not perform more work than the sequential counterpart.