Normed Processes, Unique Decomposition, and Complexity of Bisimulation Equivalences?

Abstract. We propose a decision procedure for a general class of normed commutative process rewrite systems and their induced bisimulation equivalences. Our technique is inspired by the polynomial-time algorithm for strong bisimilarity on normed Basic Parallel Processes (BPP), developed by Hirshfeld, Jerrum and Moller. We apply our general technique to derive polynomial-time algorithms for strong bisimilarity on normed BPP with communication and for distributed bisimilarity on all BPP with communication. Moreover, our technique yields the first elementary upper bound for weak and branching bisimilarity on totally normed BPP