Concurrent bisimulation algorithm

TL;DR

This paper introduces an efficient concurrent bisimulation algorithm based on the Paige and Tarjan method, optimized for parallel processing, with performance comparable to the best existing solutions and supported by experimental results.

Contribution

It presents a novel concurrent bisimulation algorithm that generalizes Hopcroft's principle for better parallelization, improving efficiency in formal analysis of concurrent systems.

Findings

Algorithm achieves competitive running time with existing solutions.

Experimental results validate the algorithm's efficiency.

Discussion on lower bounds for optimal algorithm runtime.

Abstract

The coarsest bisimulation-finding problem plays an important role in the formal analysis of concurrent systems. For example, solving this problem allows the behavior of different processes to be compared or specifications to be verified. Hence, in this paper an efficient concurrent bisimulation algorithm is presented. It is based on the sequential Paige and Tarjan algorithm and the concept of the state signatures. The original solution follows Hopcroft's principle "process the smaller half". The presented algorithm uses its generalized version "process all but the largest one" better suited for concurrent and parallel applications. The running time achieved is comparable with the best known sequential and concurrent solutions. At the end of the work, the results of tests carried out are presented. The question of the lower bound for the running time of the optimal algorithm is also discussed.