On Plain and Hereditary History-Preserving Bisimulation

Abstract

We investigate the difference between two well-known notions of
independence bisimilarity, history-preserving bisimulation and hereditary
history-preserving bisimulation. We characterise the difference between
the two bisimulations in trace-theoretical terms, advocating the
view that the first is (just) a bisimulation for causality, while the second
is a bisimulation for concurrency. We explore the frontier zone between
the two notions by defining a hierarchy of bounded backtracking bisimulations.
Our goal is to provide a stepping stone for the solution to
the intriguing open problem of whether hereditary history-preserving
bisimulation is decidable or not. We prove that each of the bounded
bisimulations is decidable. However, we also prove that the hierarchy
is strict. This rules out the possibility that decidability of the general
problem follows directly from the special case. Finally, we give a non-
trivial reduction solving the general problem for a restricted class of
systems and give pointers towards a full answer.