Publication details

<< back
 

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 and Jitka STŘÍBRNÁ. Modifications of Expansion Trees for Weak Bisimulation in BPA (Modifications of Expansion Trees for Weak Bisimulation in BPA). In Verification of Infinite-State Systems Infinity'2002. The Netherlands: Elsevier Science Publishers, 2002. p. 1-21. ISBN 0444512918.Export BibTeX
@inproceedings{405612,
author = {Černá, Ivana and Stříbrná, Jitka},
address = {The Netherlands},
booktitle = {Verification of Infinite-State Systems Infinity'2002},
keywords = {process algebra; weak bisimulation; decidability},
language = {eng},
location = {The Netherlands},
isbn = {0444512918},
pages = {1-21},
publisher = {Elsevier Science Publishers},
title = {Modifications of Expansion Trees for Weak Bisimulation in BPA},
year = {2002}
}
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:

 
 
top