Linear parallel algorithms to compute strong and branching bisimilarity
Jan Martens, Jan Friso Groote, Lars B. van den Haak, Pieter Hijma, Anton Wijs · Software & Systems Modeling · 2022
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 and $$\vert Act \vert $$ | A c t | action labels, we introduce an algorithm that decides strong bisimilarity in $$\mathcal {O}(n+\vert Act \vert )$$ O ( n + | A c t | ) time on $$\max (n,m)$$ max ( n , m ) processors and an algorithm that decides branching bisimilarity in $$\mathcal {O}(n+\vert Act \vert )$$ O ( n + | A c t | ) time using up to $$\max (n^2,m,\vert Act \vert n)$$ max ( n 2 , m , | A c t | n ) processors.