The Glory of the Past and Geometrical Concurrency

Geometrical concurrency was introduced by V. Pratt and R. van Glabbeek as the model of Higher Dimensional Automata (HDA) [Pra03, Pra00, vG06]. ◮ HDA is more general than most other true concurrency models (like event structures or Petri nets), and accommodates nicely action refinement [vGG01]. ◮ HDAs are not constrained to only before-after modelling and expose explicitly the choices in the system, therefore combining well causality, concurrency, and choice. Modal logic over HDAs was introduced as HDML [Pri10]. ◮ HDML contrasts with standard modal logics in the fact that it can reason about what holds “during ” some concurrent events are executing. ◮ HDML captures only split bisimulation, which is rather low in the spectrum of van Glabbeek and Vaandrager [vGV97]. The hHDML logic that we present here solves the question of what is a simple and natural extension of HDML that captures hereditary history preserving bisimulation. Compared to related works: ◮ hHDML does not refer to events, but talks only about labels; i.e., ⊲ hHDML does not use event identifiers as in [PU11] ⊲ or more complicated event-based modalities as in [BC10]. ◮ hHDML uses backward looking modalities as in [PU11]. ◮ hHDML uses single step modalities, thus not looking at entire parts of the HDA model, as the modalities of [PU11, BC10] do (or Until). The geometrical aspect of HDAs makes it possible to use, for capturing the hh-bisimulation, a standard modal logic that does not employ event variables, but uses standard past modalities. For more understanding we introduce ST-configuration structures, extending the configuration structures of van Glabbeek and Plotkin [vGP09] starting from the notion of ST-configuration as defined in [vGV97, vG06]. ◮ ST-configuration structures are a natural generalization of configuration structures to the setting of HDA. ◮ ST-structures correspond to Chu spaces over 3. ◮ Stable ST-structures correspond to stable configuration structures of [vGG01], hence to stable event structures. ◮ Acyclic cubical HDAs correspond to rooted, connected, and adjacent-closed ST-structures. ◮ hh-bisimulation caries over from acyclic HDAs to adjacent-close