Complexity of Weak Bisimilarity and Regularity for BPA and BPP

SRBA, Jiří. Complexity of Weak Bisimilarity and Regularity for BPA and BPP. Mathematical Structures in Computer Science. Great Britain: Cambridge University Press, vol. 12, No 1, p. 567587-567607. ISSN 0960-1295. 2003.

Basic information

• Original name: Complexity of Weak Bisimilarity and Regularity for BPA and BPP
• Authors: SRBA, Jiří (203 Czech Republic, guarantor).
• Edition: Mathematical Structures in Computer Science, Great Britain, Cambridge University Press, 2003, 0960-1295.

Other information

• Original language: English
• Type of outcome: Article in a journal
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: United Kingdom of Great Britain and Northern Ireland
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• RIV identification code: RIV/00216224:14330/03:00008472
• Organization unit: Faculty of Informatics
• Keywords in English: weak bisimilarity; complexity; process algebra
• Tags: complexity, process algebra, weak bisimilarity

Abstract

It is an open problem whether weak bisimilarity is decidable for Basic Process Algebra (BPA) and Basic Parallel Processes (BPP). A PSPACE lower bound for BPA and NP lower bound for BPP were demonstrated by Stribrna. Mayr recently achieved a result, saying that weak bisimilarity for BPP is a hard problem for the second level of polynomial hierarchy. We improve this lower bound to PSPACE, moreover for the restricted class of normed BPP. Weak regularity (finiteness) of BPA and BPP is not known to be decidable either. In the case of BPP there is a hardness result for the second level of arithmetical hierarchy by Mayr, which we improve to PSPACE. No lower bound has previously been established for BPA. We demonstrate DP-hardness, which in particular implies both NP and coNP-hardness. In each of the bisimulation/regularity problems we consider also the classes of normed processes. Finally we show how the technique for proving co-NP lower bound for weak bisimilarity of BPA can be applied to strong bisimilarity of BPP.

Links

• GA201/03/1161, research and development project: Name: Verifikace nekonečně stavových systémů

Investor: Czech Science Foundation, Verification of infinite-state systems

• MSM 143300001, plan (intention): Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů

Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing