Strong Bisimilarity and Regularity of Basic Process Algebra is PSPACE-Hard

• Authors: SRBA Jiří
• Year of publication: 2002
• Type: Article in Proceedings
• Conference: Proceedings of 29th International Colloquium on Automata, Languages and Programming (ICALP'02)
• MU Faculty or unit: Faculty of Informatics
• Field: Information theory
• Keywords: bisimilarity checking; complexity; infinite systems
• Description: Strong bisimilarity and regularity checking problems of Basic Process Algebra (BPA) are decidable, with the complexity upper bounds 2-EXPTIME. On the other hand, no lower bounds were known. In this paper we demonstrate PSPACE-hardness of these problems.

Related projects

• Infinite state concurrent systems - models and verification
• Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing