Higher Dimensional Transition Systems

Gian Luca Cattani BRICS* – Computer Science Dept.,

University of Aarhus, Denmark cattani@brics.dk

Vladimiro Sassone^{⋆} Dipartimento di Informatica Università di Pisa, Italy vs@di.unipi.it

Abstract

We introduce the notion of higher dimensional transition systems as a model of concurrency providing an elementary, set-theoretic formalisation of the idea of higher dimensional transition. We show an embedding of the category of higher dimensional transition systems into that of higher dimensional automata which cuts down to an equivalence when we restrict to non-degenerate automata. Moreover, we prove that the natural notion of bisimulation for such structures is a generalisation of the strong history preserving bisimulation, and provide an abstract categorical account of it via open maps. Finally, we define a notion of unfolding for higher dimensional transition systems and characterise the structures so obtained as a generalisation of event structures.

Introduction

In [11], Pratt argued in favour of generalising transition systems to models able to represent concurrent systems faithfully enough. In particular, he advocates for a transitionbased model in which the concurrent activity of several agents is explicitly represented by ‘higher dimensional transitions’ and formalises his intuition by means of ωcategories, whose n-cells are meant to represent the simultaneous execution of n concurrent actions.

Observing that, after all, n-cells do not accommodate higher dimensional transitions so well, most notably because of a mismatch of the respective notions of source and target, van Glabbeek [2] proposed the notion higher dimensional automata as a simpler, more fitting formalisation of Pratt’s idea. However, in such automata, higher dimensional transitions represent lists rather than sets of activities, so providing a model for ‘located concurrency’ more concrete than the one initially advocated for. Moreover, higher dimensional automata include ‘degenerate’ structures which fail the original computational intuition.

Taking up van Glabbeek’s framework, Goubault and Jensen in [6, 5] proposed to use structures and methods derived from algebraic topology, most notably the chain bicomplexes of [6]. Although the precise relationships between higher dimensional automata and bicomplexes have not been made formal, this approach offers the advantage of building on a classical, widely-known, well-established body of results and techniques. Nevertheless, as for today, such techniques do not seem to have found impressive applications in the semantics of concurrency. In other words, bicomplexes seem to bring in, unselectively, a mathematically highly non-trivial theory of continuity to study relatively simpler discrete phenomena, without really achieving significant breakthroughs.

The purpose of this paper is to show that a precise formalisation of Pratt’s idea of ‘higher dimensional transitions systems’ can be much simpler. Starting from the intuition and experience on transition systems with independence [12, 14], we follow a very simple approach: label transitions with finite multisets of actions, representing the simultaneously performance of their component actions, and impose exactly and only the local conditions on the ‘concurrency hypercubes’ needed to guarantee the existence of n distinct component transitions, which may run in any interleaving order, for each n-dimensional activity.

This yields an elementary set-theoretic framework, actually even simpler than transition systems with independence, in which the geometric intuition about higher dimensional transition is retained. This means that, in principle, ideas, methods, and results from algebraic topology can be translated in our context. Moreover, as shown in Section 2, higher dimensional transition systems embeds (fully and faithfully) in higher dimensional automata, preserving and reflecting the respective notions of homotopy and bisimulation, and such an embedding is actually an equivalence of categories when we restrict to non-degenerate automata.

1 (Analogous results holds for bicomplexes, though we do not present them here.) It is in this precise sense that we claim that nothing is lost by moving from higher dimensional automata to higher dimensional transition systems and that the latter are an adequate formalisation of the idea of transitions of higher dimension.

* Basic Research in Computer Science, Centre of the Danish National Research Foundation.

⋆ Research carried out during the author’s leave at BRICS supported by EU Human Capital and Mobility grant ERBCHBGCT920005.

Our further results are as follows. In Section 1, we consider the notion of bisimulation that arises naturally for higher dimensional transition systems, and, following a current trend in concurrency theory, we provide an abstract account of it as an instance of the bisimulation via open maps paradigm [8, 1].

The notion of unfolding of higher dimensional transition systems, developed in Section 3, provides, as for transition systems with independence in [12], a ‘behavioural’ counterpart of transition systems by ‘unrolling’ them to acyclic structures in which all the paths between the same pair of states are homotopic and, therefore, a sensible notion of ‘event’ can be defined. The unfolding, presented in the form of a coreflection of the category HDTS of higher dimensional transitions systems and its full subcategory oHDTS defined by the properties above, is shown to preserve and reflect bisimulation. As a consequence, oHDTS captures, up to bisimulation, all of HDTS. Moreover, we prove that oHDTS embeds in a presheaf category Set^{Obs^{op}}, for a rather simple category (of observations) Obs, so providing a nice categorical framework for higher dimensional transitions systems which has no counterpart in the previous approaches.

Finally, Section 3 introduces a category HDES of generalised event structures, called higher dimensional event structures, which is proved equivalent to oHDTS. Considering a corresponding generalisation of the strong history preserving bisimulation [8], we prove that, remarkably, it coincides under the equivalence oHDTS ≅ HDES with the bisimulation defined in Section 1 for HDTS. This, together with the fact that the unfolding HDTS → oHDTS preserves and reflects bisimulation, proves the remarkable fact that the natural notion of bisimulation of higher dimensional transitions systems is a generalisation of the strong history preserving bisimulation.

Due to the extended abstract nature of this presentation and the tight space bounds, the proofs must be only sketched, where not completely omitted, and the exposition of the background material kept minimal. Some acquaintance with [6] and [8] and related work would help the reader.

\underline{Acknowledgements} . We thank Rob van Glabbeek for helpful e-mail

1 Bisimulation of Higher Dimensional Transition Systems

Following the idea Pratt advocated in [11], we seek a transition-based, noninterleaving model of concurrency where, similarly to [2, 6, 5], the higher dimensional transitions are represented explicitly. Differently from the previous approaches, ideally we simply decorate a transition with a finite multiset of labels representing actions which perform simultaneously.

\underline{Remark}. In order to ensure the existence of n distinct components for each n-dimensional activity, we need to be able to distinguish the individual occurrences of an action in a multiset. To this aim, we shall label transitions by subsets of L × ω, to be thought of as multisets on L in which the multiple occurrences of a label are distinguished by natural numbers. For σ ⊆ L × ω, we shall use μ(σ) to denote the multiset on L underlying σ.

\underline{Notation}. Besides the standard notations for sets, we shall use ∅, +, and | | to denote respectively the empty multiset, multiset union, and cardinality. Given a partial function α:L_{1} ⇀ L_{2}, α will also stand for the induced map of multisets.

Definition 1.1 (Higher Dimensional Transition Systems) A higher dimensional transition system (hdts) is a structure (S,L,trans,s), where S is a set of states, L is a set of actions, s ∈ S is the initial state, and

trans ⊆ S × (P_{fin}(L × ω) ∖ {∅})× S

is a set of transitions, such that

i) (s,σ,s′),(s,σ′,s′) ∈ trans
and μ(σ) = μ(σ′) implies σ = σ′;
ii) for σ_{1},σ_{2} a partition of σ and (s,σ,s′) ∈ trans,
there exist unique v_{1},v_{2} ∈ S such that
(s,σ_{1},v_{1}) ≠ (s,σ_{2},v_{2}),
(v_{1},σ_{2},s′),(v_{2},σ_{1},s′) ∈ trans;
iii) for σ_{1},σ_{2},σ_{3} a partition of σ and (s,σ,s′) ∈ trans,
if (s,σ_{1},v_{1}), (v_{1},σ_{2}∪ σ_{3},s′),
(v_{1},σ_{2},v_{2}), (v_{2},σ_{3},s′) ∈ trans,
and (s,σ_{1}∪ σ_{2},v′_{2}), (v′_{2},σ_{3},s′),
(s,σ_{1},v′_{1}), (v′_{1},σ_{2},v′_{2}) ∈ trans,
then v_{1} = v′_{1} and v_{2} = v′_{2}.

The first condition in the above definition simply guarantees that there are no two transitions between the same states transitions carrying the same multiset of labels. The second condition guarantees that all the interleaving of a transition s →^{σ} s′are present as paths from s to s′, whilst the third ensures that such paths glue together properly: it corresponds to the cubical laws of higher dimensional automata.

2

discussions and Mogens Nielsen and Glynn Winskel for their comments on a draft of this paper.

The figure below shows the two simplest interesting examples of hdts: the empty, i.e., 1-dimensional, and the filled, i.e., 2-dimensional, squares.

[figure: v; s_{1}; b; s_{2}; a; s; a; b; T_{1}; v; s_{1}; b; s_{2}; a; s; a; b; {a,b}; T_{2}]

Observe that considering subsets of (L × ω) rather than multisets on L plays a crucial role in expressing the conditions of Definition 1.1. From now on, we shall forget the indices attached to the actions and treat transitions as labeled by multisets. In particular, we shall write (s,μ,s′) ∈ trans, for μ multiset on L, to mean that there exists (a necessarily unique) (s,σ,s′) ∈ trans with μ(σ) = μ.

Definition 1.2 (Morphisms of HDTS) For T_{1} and T_{2} hdts, a morphism from T_{1} to T_{2} consists of a map f:S_{T_{1}}→ S_{T_{2}}and a partial function α:L_{T_{1}}⇀ L_{T_{2}}that preserve the initial state and such that

(s,μ,s′) ∈ trans_{T_{1}} and α(μ) = ∅ ⇒ f(s) = f(s′); (s,μ,s′) ∈ trans_{T_{1}} and α(μ) ≠ ∅

⇒ (f(s),α(μ),f(s′)) ∈ trans_{T_{2}}.

Let HDTS denote the induced category of hdts. It is worth observing that two hdts which differ only for the indices of the labels are isomorphic in HDTS.

Some well-known subcategories of HDTS

i) The category TS of transition systems is embedded as a coreflective subcategory in HDTS, namely the full subcategory consisting of those hdts whose all transitions s →^{μ} s′have dimension one, i.e., |μ| = 1.

ii) For TSI the category of transition systems with independence, there exists an embedding TSI ↪ HDTS that adds all the higher dimensional transitions induced by the interleaved occurrence of independent actions.

iii) The category Petri of Petri nets [9] embeds in HDTS via the standard case graph construction.

iv) The domain of configurations of prime event structures [13] defines an obvious embedding EvStr ↪ HDTS that has a reflection left adjoint.

v) Analogously, configuration structures [3, 4] embed reflectively in HDTS, provided we equip them with the natural notion of morphism: pairs of partial maps on events and labels that preserve configurations and respect the relabelling.

Moreover, HDTS can be seen as a full subcategory of the category STS of the step transition systems of [10] and bears a seemingly close relationship, not yet fully understood, to local event structures [7].

Definition 1.3 (Paths and Runs) A path in a hdts is a sequence of contiguous transitions (s_{0},μ_{1},s_{1})(s_{1},μ_{2},s_{2})··· (s_{n−1} ,μ_{n},s_{n}). A run is a path that originates from the initial state.

Building on the classical notion of path, we want to formalise the idea that runs actually represent the same computation if they differ only for being different interleaving of the same concurrent actions. The following is the counterpart of the topological notion of continuous transformation of paths into each other.

Definition 1.4 (Adjacency and Homotopy) For T a hdts, adjacency is the least reflexive, symmetric, binary relation ↔_{T} on the paths of T which is closed under path concatenation and such that

(s_{0},μ_{1},s_{1})(s_{1},μ_{2},s_{2}) ↔_{T} (s_{0},μ_{1}+ μ_{2},s_{2}),

i.e., [figure: s_{1}; μ_{2}; s_{0}; μ_{1}+μ_{2}; ↕T; μ_{1}; s_{2}]

The homotopy relation ↔− _{T} on the paths of T is the transitive closure of ↔_{T}.

A computation of T is then naturally defined to be an equivalence class [π]↔− _{T} of runs of T. Clearly, morphisms respect such a definition.

Proposition 1.5 Let ⟨f,α⟩:T_{1} → T_{2} be a morphism of hdts and let π and π′ be homotopic paths in T_{1}. Then, their images via ⟨f,α⟩ are homotopic paths in T_{2}.

In order to define a suitable notion of bisimulation for hdts, it is natural to require that path homotopy is respected. For instance, if two higher dimensional transitions match each other in the ‘bisimulation game’ and they split as sequences of two lower dimensional transitions, the intermediate states should be bisimilar, too. More precisely, as formalised by the following definitions, we ask that bisimilarity of states and bisimulation game extend smoothly to computations.

Definition 1.6 (R -Bisimilar Paths) Let T_{1} and T_{2} be hdts and R ⊆ S_{T_{1}}× S_{T_{2}} be a relation on their states. Paths (s_{0},μ_{1},s_{1})(s_{1},μ_{2},s_{2})··· (s_{n−1} ,μ_{n},s_{n}) and (t_{0},μ_{1},t_{1})(t_{1},μ_{2},t_{2})··· (t_{n−1} ,μ_{n},t_{n}) of T_{1} and T_{2}, respectively, are R -related if s_{i} R t_{i}, for i = 0,...,n. Paths π_{1} and π_{2} are R -bisimilar, in symbols π_{1} ↔− _{R} π_{2}, if they are R -related and

3 ▷ for all π′_{1} ↔− _{T_{1}}π_{1},

there exists π′_{2} ↔− _{T_{2}}π_{2} with π′_{1} and π′_{2} R -related;

▷ for all π′_{2} ↔− _{T_{2}}π_{2}, there exists π′_{1} ↔− _{T_{1}}π_{1} with π′_{1} and π′_{2} R -related.

Definition 1.7 (Bisimulation of HDTS) A bisimulation between hdts T_{1} and T_{2} is a relation R on their states such that, whenever s R t and π_{1} ↔− _{R} π_{2}, for π_{1} and π_{2} runs ending respectively in states s and t, then

▷ for all (s,μ,s′) ∈ trans_{T_{1}}, there exists (t,μ,t′) ∈ trans_{T_{2}}with π_{1}(s,μ,s′) ↔− _{R} π_{2}(t,μ,t′);

▷ for all (t,μ,t′) ∈ trans_{T_{2}}there exists (s,μ,s′) ∈ trans_{T_{1}}with π_{1}(s,μ,s′) ↔− _{R} π_{2}(t,μ,t′).

Hdts T_{1} and T_{2} are bisimilar, in symbols T_{1} ∼ T_{2}, if there exists a bisimulation between them which relates their initial states.

The rest of this section is devoted to prove that ∼ can be captured categorically by means of open maps. In Section 3 we shall see that ∼ is also a natural generalisation of the strong history preserving bisimulation.

Observe that in a hdts, surrounding a ‘multiple’ transition (s,μ,s′) we always find all the possible interleavings of the actions of μ. We refer to it as the hypercube of the actions of μ at s. With this in mind, we now identify the full subcategory of HDTS that will work as the ‘path category’ (in the terminology of [8]) upon which openness is defined.

Definition 1.8 (Observations) An observation is an acyclic hdts (P,L,trans,s) of the following form

[figure: s; {a_{1}}; s_{1}; {a_{2}}; ...; {a_{n}}; s_{n}; μ; u,]

where s_{n} →^{μ} u stands for the hypercube of the actions from μ at s_{n} and all the others are transitions of dimension one. Let Obs be the full subcategory of HDTS of observations.

This category generalises the least known subcategory of pomsets (see [8, 1]) that has been used to established open bisimilarity in TSI.

In order to define Obs-openness, we need to endow HDTS with a fibred structure. Let HDTS_{L} denote the subcategory of those hdts labeled over L with maps whose label component is the identity. Hence, in a fibre, an arrow is completely determined by its action on states. Henceforth, when talking about openness, we shall always assume the considered objects to belong to the same fibre.

Definition 1.9 (Obs-openness) An arrow f:T_{1} → T_{2} of hdts is Obs-open if for all P and Q in Obs, and all arrows p, q, and m as in the commutative diagram below, there exists r:Q → T_{1} satisfying the path lifting property that r ∘ m = p and f ∘ r = q.

[figure: P; p; m; T_{1}; f; Q; q; r; T_{2}]

T_{1} and T_{2} are Obs-open bisimilar if they are connected by a span T_{1} ← P → T_{2} of Obs-open maps.

Theorem 1.10 (Bisimilarity vs. Open Bisimilarity)

Two hdts are Obs-open bisimilar if and only if they are bisimilar according to Definition 1.7.

Proof. (Sketch.) If f:T_{1} → T_{2} is Obs-open, then the relation R = {(s,f(s)) | s ∈ S_{T_{1}}} is a bisimulation. Conversely, if R is a bisimulation, one can consider the hdts consisting of pairs of R -bisimilar runs with the obvious transition relation, and show that the projections onto the terminal states of the runs define a span of Obs-open maps that relates T_{1} and T_{2}. ✓

In our framework, the number of actions labelling a transition determines its degree of concurrency. It seems natural then to consider what happens if we restrict Obs to its subcategory of objects that have hypercubes of ‘dimension’ at most n, i.e., if we forget about concurrency of ‘level’ greater than n. As expected, for n = 1 and n = 2 one obtains (concepts equivalent to) the usual concepts of, respectively, transition systems modulo strong bisimulation and transition systems with independence modulo strong history preserving bisimulation.

2 Higher Dimensional Automata and Transition Systems

The aim of this section is to investigate the precise relationships between hdts and higher dimensional automata (hda for short). Being possible to add a set of final states to hdts and lift the present results, without loss of generality we restrict to hda without such a notion. We shall show that hdts correspond precisely to non-degenerate hda. We start by seeing how to embed hdts into hda.

For the purpose of this construction, assume that any set of labels L is equipped with a linear order. Such orders induce linear orders on the elements of any subset of the set L×ω of indexed labels. For T a hdts, let hda(T) be the hda (S,d,σ,τ,s_{T},λ) defined as follows:

▷ S = S_{T}+ trans_{T}, (+ is the disjoint union),

▷ d(s) = 0, d((s,μ,s′)) = |μ|, (d is the dimension map),

4

▷ σ((s,μ,s′),i) is the (unique) transition (s,μ′,s′′) such that (s,μ,s′) ↔− _{T} (s,μ′,s′′)(s′′,{a},s′), for a the ith element of (the set underlied by) μ, (σ is the source map),

▷ τ((s,μ,s′),i) is the (unique) transition (s′′,μ′,s′) such (s,μ,s′) ↔− _{T} (s,{a},s′′)(s′′,μ′,s′), for a the ith element of (the set underlied by) μ, (τ is the target map),

▷ λ((s,{a},s′)) = a, (λ is the labelling map).

It is tedious, though not hard, to prove that all the cubical laws [2, 6] hold. The proof of the following result is also not difficult.

Proposition 2.1 There is a translation from paths of T to paths of hda(T) which preserves and reflects the homotopy relations. Moreover, T_{1} and T_{2} are bisimilar if and only if hda(T_{1}) and hda(T_{2}) are such.

As anticipated before, hdts correspond to hda that are non-degenerate in the following sense.

Definition 2.2 (Non-Degenerate HDA) An higher dimensional automata H is non-degenerate if

▷ for any state s,

|{s′∈ S | s′= σ(s,i)}| = d(s) = |{s′∈ S | s′= τ(s,i)}|,

▷ let σ̄:S → S denote the function that maps a state s to

\overbrace{σ(··· (σ}^{d(s)}(s,1),1)··· ,1) and analogously for τ̄:S → S; then the map ⟨σ̄,τ̄,λ^{∗}⟩:S → S × S × L^{∗} is injective.

Thus, the above definition formalises that any n-dimen-sional state must have n different sources and n different targets and that equal actions cannot have the same starting and ending states. Observe that this is clearly in tune with the computational intuition.

Theorem 2.3 (HDTS vs. ndHDA) There is an equivalence of categories HDTS ≅ ndHDA, where ndHDA is the category of non degenerate hda with the weak structure preserving notion of arrow, i.e., arrows that preserve source and target maps only up to a permutation of their indices, outlined in [2].

3 Unfolding Higher Dimensional Transition Systems

In order to reveal the events occurring in the runs of a hdts and their interactions, we develop here, in complete analogy with the corresponding results for TSI [12], the notion of unfolding of hdts to suitable structures.

Definition 3.1 (Occurrence HDTS)

An occurrence hdts is a hdts that is reachable, acyclic and such that for any pair of transitions (s′,μ,s) and (s′′,μ′,s), there exist two homotopic paths ending with (s′,μ,s) and (s′′,μ′,s), respectively.

Let oHDTS denote the full subcategory of HDTS consisting of occurrence hdts.

It is worth remarking that the conditions which define occurrence hdts guarantee that all the paths between two given states are homotopic and, therefore, that they represent the same computation.

For T a hdts, let the unfolding U(T) be (S,L_{T},trans,s), where

▷ S = {[π]↔− _{T} | π a run of T },

▷ ([π_{1}]↔− _{T},μ,[π_{2}]↔− _{T}) ∈ trans whenever there exists a run in [π_{2}]↔− _{T} that extends a run in [π_{1}]↔− _{T} by a single (s,μ,s′) ∈ trans_{T},

▷ s is the homotopy class of the empty run.

The picture below shows the unfoldings of the hdts T_{1} and T_{2} of Section 1. Since the two paths of length two in T_{2} are homotopic, U(T_{2}) is isomorphic to T_{2}, whilst, since (s,{a},s_{1})(s_{1},{b},v) ↮− _{T_{1}} (s,{b},s_{2})(s_{2},{a},v), the top state of T_{1} is split in U(T_{1}).

[figure: [π′_{1}]↔− _{T_{1}}; [π′_{2}]↔− _{T_{1}}; [π_{1}]↔− _{T_{1}}; b; [π_{2}]↔− _{T_{1}}; a; [∅]↔− _{T_{1}}; a; b; U(T_{1}); [π′]↔− _{T_{2}}; [π_{1}]↔− _{T_{2}}; b; [π_{2}]↔− _{T_{2}}; a; [∅]↔− _{T_{2}}; a; b; {a,b}; U(T_{2})]

Since an arrow between hdts naturally lifts to an arrow between their transitions, and hence between their runs, U immediately extends to a functor HDTS → oHDTS.

Theorem 3.2

U is right adjoint to the inclusion oHDTS ↪ HDTS, and thus oHDTS is a coreflective subcategory of HDTS. Therefore, U preserves and reflects the bisimulation relation, i.e., T_{1} and T_{2} are bisimilar if and only if U(T_{1}) and U(T_{2}) are such.

Proof. (Sketch.) Let O be an occurrence hdts and T a hdts. Since each state o of O determines a class of runs [π_{o}]↔− _{O}, each arrow f:O → T determines an arrow f̄:O → U(T) that maps o to the class [f(π_{o})]↔− _{T}. Vice versa, each f̄:O → U(T) originates an f:O → T by taking f(o) to be the ending state of any of the paths in f̄(o). The constructions are easily shown to be in natural bijection to each other.

5

The second part of the theorem follows from general property of adjunctions with respect to the path lifting property that defines Obs-open bisimulation. ✓

The following technical result is the key to establish an embedding of oHDTS into a category of presheaves.

Theorem 3.3 Obs is a dense full subcategory of oHDTS.

Proof. (Sketch.) For OT an occurrence hdts, consider the category Obs ↓ OT, i.e., the category whose objects are arrows o:O → OT in oHDTS, for O an observation, and whose arrows m:o_{1} → o_{2} are arrows in Obs between the observations O_{1} and O_{2}, domains respectively of o_{1} and o_{2}, such that o_{1} = o_{2} ∘ m. Since Obs is a full subcategory of oHDTS, there is a ‘projection functor’ π:Obs ↓ OT → oHDTS such that π(o_{1}) = O_{1} and π(m) = m. Now, it is not difficult to see that OT ≅ lim_{−→} π, i.e., every occurrence hdts is a colimit of observations in a canonical way. ✓

It follows from this theorem, for general arguments (see [8]), that oHDTS embeds in Set^{Obs^{op}}, the topos of presheaves over Obs. The characterisation of bisimulation by means of open maps given in Theorem 1.10 provides us also with the key to define a corresponding notion of bisimulation in the presheaf category. In fact, the same definition of open morphism applies mutatis mutandis, once we replace ‘representables’ for ‘observations’. The notion of bisimulation so derived agrees with the original one on the image of oHDTS in Set^{Obs^{op}}, which, therefore, proposes itself as a valuable categorical framework into which HDTS, up to bisimulation, can be studied.

Our next aim is to find an alternative description of oHDTS centered on notions of events and configurations. In other words, we now look for a generalisation of event structures to a model able to handle properly the sophisticated interactions occurring in the computations of hdts. Such considerations led us to the following definition.

Definition 3.4 (Higher Dimensional Event Structure) A higher dimensional event structure (hdes) is a structure (E,⊢,ℓ,L), where E is a set of events, L is a set of actions, ℓ:E → L is a labelling function, and ⊢ ⊆ P_{fin}(E) × P_{fin}(E), the entailment relation, is such that

x ⊢ y implies x ⊂ y and

for all x ⊂ y′⊂ y, x ⊢ y′ and y′⊢ y.

For E and F hdes, a morphism from E to F is a pair of partial maps f:E ⇀ F and α:L_{E} ⇀ L_{F} such that

i) ℓ_{F} ∘ f = α ∘ ℓ_{E};

ii) x ⊢ x′ implies f(x) ⊢ f(x′).

Thus, a hdes consists of a set of events together with a set of ‘transition rules’ between sets of events. Such rules define directly the proper notion of computation for hdes.

Definition 3.5 (Paths and Runs) A path in a higher dimensional event structure is a sequence x = x_{0}x_{1}··· x_{n} of subsets of E such that

x_{i} ⊢ x_{i+1} , for 0 ≤ i < n.

A run is a path x with x_{0} = ∅.

The concepts of adjacency and homotopy of paths we defined for hdts have corresponding notions for hdes.

Definition 3.6 (Adjacency and Homotopy) For E a hdes, adjacency is the least reflexive, symmetric, binary relation ↔_{E} on the paths of E such that x ↔_{E} y if, for some i ∈ ω,

x_{i} = y_{i}∪ y_{i+1} , and x_{j} = \{ \begin{matrix}y_{j} & for j < i, \\ y_{j+1} & for j > i. \end{matrix}

The homotopy relation ↔− _{E} on the paths of E is the transitive closure of ↔_{E}. A computation in E is an equivalence class of the homotopy relation.

It is not difficult to observe that, in order for occurrence hdts and hdes to match perfectly, we still miss two important ingredients. In fact, differently from occurrence hdts, not every two paths of hdes E leading from x to y are homotopic.

Example 3.7 Consider an hdes ({e_{1},e_{2}},⊢,ℓ,L), where the entailment relation consists of the pairs

∅ ⊢ {e_{1}}, ∅ ⊢ {e_{2}}, {e_{1}} ⊢ {e_{1},e_{2}}, and {e_{2}} ⊢ {e_{1},e_{2}}.

Then, the paths ∅ ⊢ {e_{1}} ⊢ {e_{1},e_{2}} and ∅ ⊢ {e_{2}} ⊢ {e_{1},e_{2}} are clearly not homotopic, since ∅ ⊬ {e_{1},e_{2}}.

Secondly, we must observe that not every event in E will necessarily appear in some computation. Although a more elementary description of such requirements could be desirable, for the time being we take the following definition.

Definition 3.8 (Proper Event Structures) A hdes E is said to be proper if it is reachable, i.e., every e ∈ E belongs to some computation, and whenever x ⊢ y and x′⊢ y for some x,x′,y ∈ P_{fin}(E), there exist z ∈ P_{fin}(E) such that

z ⊢ x_{1} ⊢ ... ⊢ x ⊢ y and z ⊢ x′_{1} ⊢ ... ⊢ x′⊢ y,

and the two paths are homotopic. It is immediate to see that proper hdes and their morphism form a category which we shall refer as HDES.

6

Equipped with these definitions, we can now prove the following result.

Proposition 3.9 There is an equivalence of categories HDES ≅ oHDTS which preserves (and reflects) the relations of adjacency and homotopy defined independently in the two categories.

Proof. (Hints.) We only hint at the definitions of the objectcomponents of the involved functors. For both the directions of this equivalence, consider as states in one case and as events in the opposite direction, (suitable) homotopy classes of runs. Correspondingly, transitions and, on the other direction, the enabling are naturally defined exploiting the extensions (prefix ordering) of paths. ✓

Since hdes are a generalisation of event structures, it seems natural to provide them with a notion of bisimulation derived from the ideas which led to strong history preserving bisimulation. As already hinted in Section 1, this can indeed be done. Remarkably, building on the equivalence presented in Proposition 3.9, we shall prove that this yields yet another characterisation of ∼.

\underline{Observation}. Observe that for a path x = x_{0}x_{1}...x_{n} in an hdes E, the restriction of the labelling and of the entailment of E to x_{n} yields a sub-hdes. Moreover, since any two homotopic paths will share the same set of occurred events, we shall use x to denote also the set of events in [x]↔− _{E}.

\underline{Notation}. In the following, we write [x]↔− _{E} ≤ [y]↔− _{E} to mean that each run in [x]↔− _{E} can be extended to a run in [y]↔− _{E}. If such extensions can be achieved by the concurrent occurrence of events carrying the labels μ, we write [x]↔− _{E} →^{μ} [x′]↔− _{E}. In the next definition, we omit the index ↔− _{E} from the equivalence classes.

Definition 3.10 (Strong History Preserving Bisimulation) A strong history preserving bisimulation between the hdes E and F is a set H of triples ([x],f,[y]), for [x] and [y] computations in, respectively, E and F, and f:x → y an isomorphism of (sub-)hdes. Moreover

i) ([∅],∅,[∅]) ∈ H,

ii) ([x],f,[y]) ∈ H and [x] →^{μ} [x′] implies that there exists [y′] such that [y] →^{μ} [y′] and ([x′],f′,[y′]) ∈ H for f′ an extension of f,

iii) ([x],f,[y]) ∈ H and [y] →^{μ} [y′] implies that there exists [x′] such that [x] →^{μ} [x′] and ([x′],f′,[y′]) ∈ H for f′ an extension of f,

iv) ([x],f,[y]) ∈ H and [x′] ≤ [x] implies that there exists [y′] ≤ [y] such that ([x′],f′,[y′]) ∈ H for f′ the restriction of f to [x′], v) ([x],f,[y]) ∈ H and [y′] ≤ [y] implies that there ex-

ists [x′] ≤ [x] such that ([x′],f′,[y′]) ∈ H for f′ the restriction of f to [x′],

Hdes E and F are strong history preserving bisimilar if and only if there exists a bisimulation between them.

Finally, we have the announced result linking the bisimulation on hdts with the strong history preserving bisimulation on hdes.

Theorem 3.11 (Bisimulation vs. SHP Bisimulation) Two hdts are bisimilar if and only if their unfolding as hdes are strong history preserving bisimilar.

Proof. (Hints.) Using the equivalence of Proposition 3.9, it is possible to show that Obs-open bisimulation on HDES corresponds precisely to the strong history preserving bisimulation of Definition 3.10. Since from Theorems 1.10 and 3.2 we know that bisimulation for hdts corresponds to Obs-open bisimulation for occurrence hdts, the thesis follows. ✓

This last result can be also read as saying that strong history preserving bisimulation, rather than a mere strengthening of history preserving bisimulation, is a natural notion of bisimulation for higher dimensional structures of independent interest.

Conclusion

The paper introduced higher dimensional transition systems as an attempt to formalise in the simplest possible way Pratt’s idea of transitions of higher dimension. Our treatment here, somehow inspired by recent work on independence models for concurrency such as transition systems with independence and event structures, supports the claim that nothing is lost by moving from higher dimensional automata to higher dimensional transition systems. In particular, we proved that the two approaches coincide in a strong categorical sense when we restrict attention to nondegenerate automata.

The paper focused especially on the notion of bisimulation of higher dimensional transition systems, proving that the natural choice leads to a generalisation of the strong history preserving bisimulation. Remarkably, this yields a characterisation of such an equivalence in terms of preservation of homotopy, viz., bisimulation lifts from states to computations, i.e., homotopy classes of runs.

It is worth remarking here that bisimilarity of finite higher dimensional transition systems is decidable. This non-trivial result follows by proving, e.g., that the length of the pairs of R -bisimilar paths considered in Definition 1.7 can be bound uniformly in the sizes of the transition systems under analysis. It follows then from Theorem 3.11 —

7 together with the fact that the unfolding U:HDTS → HDES cuts down to the unfolding of transition systems with independence to event structures developed in [12] — that strong history preserving bisimulation is decidable for finite transition systems with independence, which was a relatively long-standing open problem. The details of this proof and the analysis of its consequences will be given elsewhere.

As a matter of future work, we would certainly like to find a more elementary and satisfactory condition for proper higher dimensional event structures in Definition 3.8.

References

[1] A. Cheng and M. Nielsen. Open Maps (at) Work, BRICS Report Series RS-95-23 (1995), Computer Science Dept., University of Aarhus. Some of the results appear also in ‘Observing Behaviour Categorically’, in Proceedings of FST&TCS’95, P.S. Thiagarajan (Ed.), LNCS 1026 (1995), 263–278.

[2] R. van Glabbeek. Bisimulation for higher dimensional automata, email message sent to the Concurrency mailing list on July 7, 1991. Available at http://theory.

stanford.edu/people/rvg/hda.

[3] R. van Glabbeek and U. Goltz. Refinement of actions in Causality based Models. In Proceedings of REX Workshop on Stepwise Refinement of Distributed Systems, J.W. de Bakker et al. (Eds.), LNCS 430 (1989), 267–300.

[4] R. van Glabbeek and G. Plotkin. Configuration Structures. In Proceedings of LICS’95, IEEE Computer Society Press (1995), 99–109.

[5] E. Goubault. Domains of Higher Dimensional Automata. In Proceedings of CONCUR’93, E. Best (Ed.), LNCS 715 (1993), 293–307.

[6] E. Goubault and T. Jensen. Homology of Higher Dimensional Automata. In Proceedings of CONCUR’92, W.R. Cleaveland (Ed.), LNCS 630 (1992), 254–268.

[7] P.W. Hoogers, H.C.M. Kleijn, and P.S. Thiagarajan. Local Event Structures and Petri Nets. In Proceedings of CONCUR’93, E. Best (Ed.), LNCS 715 (1993), 462–476.

[8] A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from Open Maps. BRICS Report Series RS-94-7 (1994), Computer Science Dept., University of Aarhus. Extended abstract appears as ‘Bisimulation and Open Maps’, in Proceedings of LICS’93, IEEE Computer Society Press (1993), 418–427.

[9] J. Meseguer, and U. Montanari. Petri Nets are Monoids. Information and Computation, n. 88 (1990), 105–154.

[10] M. Mukund. Petri Nets and Step Transition Systems. International Journal of Foundations of Computer Science, vol. 3(4) (1992), 443–478.

[11] V. Pratt. Modeling Concurrency with Geometry. In Proceedings of 18th ACM Symposium on Principles of Programming Languages, ACM Press (1991), 311–322.

[12] V. Sassone, M. Nielsen, and G. Winskel. Models for Concurrency: Towards a Classification. Theoretical Computer Science (1996), to appear. Extended abstract appears as ‘A Classification of Models for Concurrency’, in Proceedings of CONCUR’93, E. Best (Ed.), LNCS 715 (1993), 82–96.

[13] G. Winskel. Event Structures. In Advances in Petri Nets, 1986, part II, W. Brauer et al. (Eds.), LNCS 255 (1986), 325–392.

[14] G. Winskel and M. Nielsen. Models for Concurrency In Handbook of Logic and the Foundations of Computer Science, vol. IV, S. Abramsky et al. (Eds.), Oxford University Press (1995), 1–148.

8