Hereditary History Preserving Bisimilarity is Undecidable

Abstract

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.