2013/11/25 by Konrad Kułakowski, Kułakowski, Konrad
Computer Science · #Distributed #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Parallel #Petri Nets in System Modeling #and Cluster Computing (cs.DC) #cs.DC #cs.LO
paper · pdf · doi:10.48550/arxiv.1311.7635
22 pages, 7 figures
openalex publication_date 2013/11/25 · arxiv created 2014/01/10 · arxiv updated 2014/01/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.