Modifications of Expansion Trees for Weak Bisimulation in BPA

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ČERNÁ Ivana STŘÍBRNÁ Jitka

Year of publication 2002
Type Article in Proceedings
Conference Verification of Infinite-State Systems Infinity'2002
MU Faculty or unit

Faculty of Informatics

Citation
Field Computer hardware and software
Keywords process algebra; weak bisimulation; decidability
Description 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:

You are running an old browser version. We recommend updating your browser to its latest version.