Publication details
Modifications of Expansion Trees for Weak Bisimulation in BPA
| Basic information | |
|---|---|
| Original title: | Modifications of Expansion Trees for Weak Bisimulation in BPA |
| Authors: | Ivana Černá, Jitka Stříbrná |
| Further information | |
|---|---|
| Citation: | ČERNÁ, Ivana  - STŘÍBRNÁ, Jitka. Modifications of Expansion Trees for Weak Bisimulation in BPA. In Verification of Infinite-State Systems Infinity'2002. The Netherlands : Elsevier Science Publishers, 2002. ISBN 0444512918, pp. 1-21. 2002, 24.8.2002, Brno, Czech Republic. |
| Original language: | English |
| Field: | Computer hardware and software |
| Type: | Article in Proceedings |
| Keywords: | process algebra; weak bisimulation; decidability |
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 (\cite{BBK,BCS,CHS}). 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. There are two closely related approaches to semidecidability of strong equivalence: construction of a (finite) bisimulation or expansion tree and 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.
Related projects:
- Infinite state concurrent systems - models and verification
- Decidability and complexity of observational equivalences on infinite - state processes
- Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing
