Hereditary history preserving Bisimilarity is Undecidable

Abstract

History preserving bisimilarity (hp-bisimilarity) and hereditary history preserving bisimilarity (hhp-bisimilarity) are behavioural equivalences taking into account causal relationships between events of concurrent systems. Their prominent feature is being preserved under action refinement, an operation important for the top-down design of concurrent systems. We show that-unlike hp-bisimilarity-checking hhpbisimilarity for finite labelled asynchronous transition systems is not decidable, by a reduction from the halting problem of 2-counter machines. To make the proof more transparent we introduce an intermediate problem of checking domino bisimilarity for origin constrained tiling systems, whose undecidability is interesting in its own right. We also argue that the undecidability of hhp-bisimilarity holds for finite labelled 1-safe Petri nets.