Hereditary History Preserving Bisimilarity is Undecidable

We show undecidability of hereditary history preserving bisimilarityfor finite asynchronous transition systems by a reduction from the haltingproblem of deterministic 2-counter machines. To make the proof moretransparent we introduce an intermediate problem of checking dominobisimilarity for origin constrained tiling systems. First we reduce thehalting problem of deterministic 2-counter machines to origin constraineddomino bisimilarity. Then we show how to model domino bisimulations ashereditary history preserving bisimulations for finite asynchronous transitionssystems. We also argue that the undecidability result holds forfinite 1-safe Petri nets, which can be seen as a proper subclass of finiteasynchronous transition systems