Saturation Heuristic for Faster Bisimulation with Petri Nets

Bisimilarity is an extensional notion of equivalence of states of an automata. A bisimulation is a set of such equivalences among the states of automata. The bisimulation problem is the task of deciding bisimilarity for all pairs of states of an automata. The present work applies the Saturation [15] heuristic and interleaved MDD partition representation to the bisimulation problem. Previous work [15] comparing the use of various partition representations in a classical fixed-point algorithm for the bisimulation problem, motivated the present work. By focusing on bisimulation for systems with deterministic transition relations (Petri Nets) we show that bisimulation can be expressed as a state-space exploration problem. This suggests the use of the saturation[3] heuristic, which has been found to be relatively efficient for state-space generation. The present work explores the use of our novel saturation-based bisimulation algorithm in the context of the SmArT verification tool. We compare the execution time and memory consumption of our saturation-based fully-implicit methods (using interleaved MDDs) with the execution time and memory consumption of fully-implicit and partially-implicit methods (using non-interleaved MDDs) considered in the previous work, as applied to the same bisimulation problems. We found that with some models having very many equivalence classes in their bisimulation partitions, our novel algorithm gave better speed performance than any of the other algorithms tested. The memory utilization of the classic algorithm was surprisingly better in those cases where it could be applied. With models having very small numbers of equivalence classes in their bisimulation partitions, our novel algorithm performed only slightly less well than the fastest algorithm, while the classic algorithm continues to show better memory utilization.