Deciding bisimilarity is P -complete
José L. Balcázar, Joaquim Gabarró, Miklós Sántha · Formal Aspects of Computing · 1992
Abstract In finite labelled transition systems the problems of deciding strong bisimilarity, observation equivalence and observation congruence are P -complete under many—one NC -reducibility. As a consequence, algorithms for automated analysis of finite state systems based on bisimulation seem to be inherently sequential in the following sense: the design of an NC algorithm to solve any of these problems will require an algorithmic breakthrough, which is exceedingly hard to achieve.