Linear parallel algorithms to compute strong and branching bisimilarity

• DOI: 10.1007/s10270-022-01060-7
• Publication Date: 2022-12-06T14:06:40Z
• Authors: Jan Martens; Jan Friso Groote; Lars B. van den Haak; Pieter Hijma; Anton Wijs
• Keywords: PRAM; RCPP; Parallel algorithms; 0202 electrical engineering, electronic engineering, information engineering; SDG 7 - Affordable and Clean Energy; 02 engineering and technology; Branching bisimulation; Strong bisimulation

Abstract We present the first parallel algorithms that decide strong and branching bisimilarity in linear time. More precisely, if a transition system has n states, m transitions $$\vert Act \vert $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mo>|</mml:mo> <mml:mi>A</mml:mi> <mml:mi>c</mml:mi> <mml:mi>t</mml:mi> </mml:mrow> </mml:math> action labels, we introduce an algorithm decides $$\mathcal {O}(n+\vert )$$ <mml:mi>O</mml:mi> <mml:mo>(</mml:mo> <mml:mi>n</mml:mi> <mml:mo>+</mml:mo> <mml:mo>)</mml:mo> time on $$\max (n,m)$$ <mml:mo>max</mml:mo> <mml:mo>,</mml:mo> <mml:mi>m</mml:mi> processors using up to (n^2,m,\vert n)$$ <mml:msup> <mml:mn>2</mml:mn> </mml:msup> processors.