Title :
Strong bisimilarity on basic parallel processes in PSPACE-complete
Author_Institution :
Dept. of Comput. Sci., Tech. Univ. of Ostrava, Czech Republic
Abstract :
The paper shows an algorithm which, 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 PSAPCE. Combining with the PSPACE-hardness result by Srba, PSPACE-completeness is thus established.
Keywords :
bisimulation equivalence; computational complexity; polynomials; theorem proving; BPP system; LTS; PSPACE-completeness; PSPACE-hardness; basic parallel process; bisimulation equivalence; labelled transition system; linear mapping; polynomial space algorithm; strong bisimilarity; Arithmetic; Automata; Computer science; Concurrent computing; Logic; Natural languages; Polynomials; Terminology; Upper bound;
Conference_Titel :
Logic in Computer Science, 2003. Proceedings. 18th Annual IEEE Symposium on
Print_ISBN :
0-7695-1884-2
DOI :
10.1109/LICS.2003.1210061