18th Annual IEEE Symposium on Logic in Computer Science (LICS'03)
Strong Bisimilarity on Basic Parallel Processes is PSPACE-complete
Ottawa, Canada
June 22-June 25
ISBN: 0-7695-1884-2
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.