Open AccessHereditary History Preserving Bisimilarity is Undecidable
Author(s) -
Marcin Jurdziński,
Mogens Nielsen
Publication year - 1999
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v6i19.20076
Subject(s) - undecidable problem , halting problem , domino , petri net , asynchronous communication , transition system , concurrency , reduction (mathematics) , decidability , mathematics , discrete mathematics , theory of computation , computer science , algorithm , programming language , biology , turing machine , computer network , biochemistry , geometry , computation , catalysis
We show undecidability of hereditary history preserving bisimilarity for 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.