Hereditary History-Preserving Bisimilarity: Logics and Automata

We study hereditary history-preserving (hhp-) bisimilarity, a canonical behavioural equivalence in the true concurrent spectrum, by means of logics and automata. We first show that hhp-bisimilarity on prime event structures can be characterised in terms of a simple logic whose formulae just observe events in computations and check their executability. The logic suggests a characterisation of hhp-bisimilarity based on history-dependent automata, a formalism for modelling systems with dynamic allocation and deallocation of resources, where the history of resources is traced over time. Prime event structures can be naturally mapped into history-dependent automata in a way that hhp-bisimilarity exactly corresponds to the canonical behavioural equivalence for history-dependent automata.