Marcin Jurdzi{\'n}ski and Mogens Nielsen and Ji\v{r}\'{\i} Srba
``Undecidability of Domino Games and Hhp-Bisimilarity''

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 that they are preserved under action
  refinement, an operation important for the top-down design of
  concurrent systems. 
  It is shown that, in contrast to hp-bisimilarity, checking
  hhp-bisimilarity  for finite labelled asynchronous transition
  systems is undecidable, by a reduction from the halting problem of
  2-counter machines. 
  To make the proof more transparent a novel intermediate 
  problem of checking domino bisimilarity for origin constrained 
  tiling systems is introduced and shown undecidable.
  It is also shown that the unlabelled domino bisimilarity problem is
  undecidable, which implies undecidability of hhp-bisimilarity for
  unlabelled finite asynchronous systems. 
  Moreover, it is argued that the undecidability of hhp-bisimilarity
  holds for finite elementary net systems and 1-safe Petri nets.