Some Remarks on Weak Bisimilarity of BPA-Processes

ČERNÁ, Ivana and Jitka STŘÍBRNÁ. Some Remarks on Weak Bisimilarity of BPA-Processes. Brno: FI MU Brno, 2000, 26 pp. FIMU-RS-2000-09.

Basic information

• Original name: Some Remarks on Weak Bisimilarity of BPA-Processes
• Authors: ČERNÁ, Ivana and Jitka STŘÍBRNÁ.
• Edition: Brno, 26 pp. FIMU-RS-2000-09, 2000.
• Publisher: FI MU Brno

Other information

• Original language: English
• Type of outcome: Book on a specialized topic
• Field of Study: 10000 1. Natural Sciences
• Country of publisher: Czech Republic
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• RIV identification code: RIV/00216224:14330/00:00002688
• Organization unit: Faculty of Informatics

Abstract

The purpose of this work is to examine the decidability problem of weak bisimilarity for BPA-processes. It has been known that strong bisimilarity, which may be considered a special case of weak bisimilarity, where the internal (silent) action tau is treated equally to observable actions, is decidable for BPA-processes. For strong bisimilarity, these processes are finitely branching and so for two non-bisimilar processes there exists a level n that distinguishes the two processes. Additionally, from the decidability of whether two processes are equivalent at a given level n, semidecidability of strong non-bisimilarity directly follows. We examine the following two closely related approaches to semidecidability of strong equivalence: 1.construction of a (finite) bisimulation or expansion tree, 2.construction of a finite Caucal base. We have attempted to find out if any of the above mentioned approaches could be generalized to (semi)decide weak bisimilarity. Our findings indicate that a direct generalization is not sufficient and an efficient (semi)decision procedure cannot be obtained in this way.

Links

• GA201/00/0400, research and development project: Name: Nekonečně stavové souběžné systémy - modely a verifikace

Investor: Czech Science Foundation, Infinite state concurrent systems - models and verification

• GA201/99/D026, research and development project: Name: Rozhodnutelnost a složitost observačních ekvivalencí na nekonečně stavových procesech

Investor: Czech Science Foundation, Decidability and complexity of observational equivalences on infinite - state processes

• 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