Hereditary History Preserving Bisimilarity is Undecidable
DOI:
https://doi.org/10.7146/brics.v6i19.20076Abstract
We show undecidability of hereditary history preserving bisimilarityfor finite asynchronous transition systems by a reduction from the halting
problem of deterministic 2-counter machines. To make the proof more
transparent we introduce an intermediate problem of checking domino
bisimilarity for origin constrained tiling systems. First we reduce the
halting problem of deterministic 2-counter machines to origin constrained
domino bisimilarity. Then we show how to model domino bisimulations as
hereditary history preserving bisimulations for finite asynchronous transitions
systems. We also argue that the undecidability result holds for
finite 1-safe Petri nets, which can be seen as a proper subclass of finite
asynchronous transition systems.
Downloads
Published
1999-01-19
How to Cite
Jurdzinski, M., & Nielsen, M. (1999). Hereditary History Preserving Bisimilarity is Undecidable. BRICS Report Series, 6(19). https://doi.org/10.7146/brics.v6i19.20076
Issue
Section
Articles
License
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.