Hereditary History Preserving Simulation is Undecidable

Abstract

We show undecidability of hereditary history preserving simulation
for finite asynchronous transition systems by a reduction from the halting
problem of deterministic Turing machines. To make the proof more
transparent we introduce an intermediate problem of deciding the winner
in domino snake games. First we reduce the halting problem of deterministic
Turing machines to domino snake games. Then we show how to
model a domino snake game by a hereditary history simulation game on
a pair of finite asynchronous transition systems.