The Glory of the Past and Geometrical Concurrency ⋆

Abstract. This paper contributes to the general understanding of the geometrical model of concurrency that was named higher dimensional automata (HDAs) by Pratt and van Glabbeek. In particular we provide some understanding of the modal logics for such models and their expressive power in terms of the bisimulation that can be captured. The geometric model of concurrency is interesting from twomain reasons: its generality and expressiveness, and the natural way in which autoconcurrency and action refinement are captured. Logics for this model, though, are not well investigated, where a simple, yet adequate, modal logic over HDAs was only recently introduced. As this modal logic, with two existential modali-ties, during and after, captures only split bisimulation, which is rather low in the spectrum of van Glabbeek and Vaandrager, the immediate question was what small extension of this logic could capture the more fine-grained hereditary history preserving bisimulation (hh)? In response, the work in this paper provides several insights. One is the fact that the ge-ometrical aspect of HDAs makes it possible to use for capturing the hh-bisimulation, a stan-dard modal logic that does not employ event variables, opposed to the two logics (over less expressive models) that we compare with. The logic that we investigate here uses standar