Options
Decidability of plain and hereditary history-preserving bisimilarity for BPP
Citation Link: https://doi.org/10.15480/882.4048
Publikationstyp
Conference Paper
Date Issued
1999-12-01
Sprache
English
Author(s)
TORE-DOI
Volume
27
Start Page
85
End Page
106
Citation
Electronic Notes in Theoretical Computer Science 27: 85-106 (1999-12-01)
Contribution to Conference
Publisher DOI
Scopus ID
Publisher
Elsevier Science
In this paper we investigate the decidability of history-preserving bisimilarity (HPB) and hereditary history-preserving bisimilarity (HHPB) for basic parallel processes (BPP). We find that both notions are decidable for this class of infinite systems, and present tableau-based decision procedures. The first result is not new but has already been established via the decidability of causal bisimilarity, a notion that is equivalent to HPB. We shall see that our decision procedure is similar to Christensen's proof of the decidability of distributed bisimilarity, which leads us to the coincidence between HPB and distributed bisimilarity for B-The decidability of HHPB is a new result. This result is especially interesting, since the decidability of HHPB for finite-state systems has been a long-standing open problem which has recently been shown to be undecidable. I would like to thank the many people with whom I have discussed the notions of plain and hereditary HPB, in particular I thank Colin Stirling for his advice on my BPP work, Astrid Kiehn for providing me with her notes on distributed bisimilarity, and Ilaria Castellani and Rob van Glabbeek for their helpful comments at EXPRESS. I also thank two of the anonymous referees for valuable comments which drew my attention to the coincidence of distributed and history-preserving bisimilarity.
DDC Class
004: Informatik
Publication version
publishedVersion
Loading...
Name
1-s2.0-S157106610580297X-main.pdf
Size
625.18 KB
Format
Adobe PDF