Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds

Abstract

In this paper we study bisimilarity problems for simple process algebras. In particular, we show PSPACE-hardness of the following problems:

1. strong bisimilarity of Basic Parallel Processes (BPP),
2. strong bisimilarity of Basic Process Algebra (BPA),
3. strong regularity of BPP, and
4. strong regularity of BPA.

We also demonstrate NL-hardness of strong regularity problems for the normed subclasses of BPP and BPA.

Bisimilarity problems for simple process algebras are introduced in a general framework of process rewrite systems, and a uniform description of the new techniques used for the hardness proofs is provided.