Fröschle, Sibylle B.Sibylle B.FröschleLasota, SławomirSławomirLasota2021-12-162021-12-162009-06-18Electronic Notes in Theoretical Computer Science 239 (C): 17-42 (2009-07-01)http://hdl.handle.net/11420/11285We 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. As part of our framework we present a generic unique decomposition result, which we obtain by building on a characterization by Luttik and van Oostrom. 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 a PSPACE upper bound for weak and branching bisimilarity on totally normed BPP.en1571-06612009C1742Elsevier Sciencehttps://creativecommons.org/licenses/by-nc-nd/3.0/Basic Parallel ProcessesBisimulation equivalencebranching bisimulationdistributed bisimulationunique decompositionweak bisimulationInformatikJournal Article10.15480/882.403410.1016/j.entcs.2009.05.02810.15480/882.4034Other