摘要：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.
