Hereditary History Preserving Bisimilarity Coincides with History Preserving Bisimilarity for a Class of Live Free Choice Systems

History preserving (hp) and hereditary hp (hhp) bisimilarity are two equivalences for concurrent systems that reflect causal dependencies between events. hp bisimilarity is well-known to be decidable for finite-state systems, whereas the decidability of hhp bisimilarity had been a renowned open problem for several years until it was finally proved undecidable. Recently, the following positive result has been obtained: hhp bisimilarity coincides with hp bisimilarity for a class of live free choice systems. To our knowledge, this is the only positive result for a class with a reasonable amount of interplay between concurrency and conflict, as well as nondeterminism. In this paper we provide an extended abstract of the proof that stands behind this result. The aim is to provide an overview of the modules involved and how they interact in the key results. We will not directly be concerned with hp and hhp bisimilarity in this paper, but with an auxiliary bisimilarity and its hereditary version