In: 18th Annual IEEE Symposium on Logic in Computer Science, Ottawa, Canada, June 22 - 25, 2003, pages 218-227. June 2003.
Abstract: The paper shows an algorithmwhich, given a Basic Parallel Processes (BPP) system, constructs a set of linear mappings which characterize the (strong) bisimulation equivalence on the system. Though the number of the constructed mappings can be exponential, they can be generated in polynomial space; this shows that the problem of deciding bisimulation equivalence on BPP is in PSPACE. Combining with the PSPACE-hardness result by Srba, PSPACE-completeness is thus established.