On the Expressiveness of

Higher Dimensional Automata

R.J. van Glabbeek^{1,2}

National ICT Australia and School of Computer Science and Engineering The University of New South Wales Locked Bag 6016, Sydney, NSW 1466, Australia

Abstract

In this paper I compare the expressive power of several models of concurrency based on their ability to represent causal dependence. To this end, I translate these models, in behaviour preserving ways, into the model of higher dimensional automata, which is the most expressive model under investigation. In particular, I propose four different translations of Petri nets, corresponding to the four different computational interpretations of nets found in the literature.

I also extend various equivalence relations for concurrent systems to higher dimensional automata. These include the history preserving bisimulation, which is the coarsest equivalence that fully respects branching time, causality and their interplay, as well as the ST-bisimulation, a branching time respecting equivalence that takes causality into account to the extent that it is expressible by actions overlapping in time. Through their embeddings in higher dimensional automata, it is now well-defined whether members of different models of concurrency are equivalent.

Keywords: Concurrency, expressiveness, causality, higher dimensional automata, Petri nets, event structures, history preserving bisimulation, ST-bisimulation.

1 A hierarchy of concurrency models

Figure 1 lists the main models of concurrency proposed in the literature, ordered by expressive power. Of all models, the labelled variant is understood. Here I only treat models of processes that perform actions a, b, c, … whose internal structure is not further examined, and real-time and stochastic aspects

1 This work was supported by EPSRC under grant number GR/S22097

2 Email: rvg@cs.stanford.edu

An extended abstract of this paper appeared in Electronic Notes in Theoretical Computer Science 128(2), April 2005: Proceedings of the 11th International Workshop on Expressiveness in Concurrency, EXPRESS 2004, pp. 5–34.

[figure: synchronisation trees [20]; prime event structures [30,31]; ^{\begin{cases}bundle e.s. [18] \\ flow e.s. [5] \\ stable e.s. [30,31] \\ safe Petri nets \end{cases}}; Winskel’s event structures [30,31]; pure Petri nets; rooted finitary configuration structures [11,12]; automata [10]; Petri nets; higher dimensional automata [9]]

Fig. 1. A hierarchy of concurrency models, ordered by expressive power up to history preserving bisimulation

of processes are completely ignored. Furthermore, I only study the representation of processes, not the representation of operators on processes. I restrict myself to models that take branching time fully into account, and hence skip models that represent processes by the sets of their executions. Thus, the expressive power of the models differs only to the extent that certain forms of causal dependence are expressible. I limit myself to models that take a fully asynchronous view on parallelism: whenever a number of actions can happen simultaneously, this must be because they are causally independent, and hence they can also happen in any order. Because of this, I do not include Petri nets with inhibitor arcs, or Chu spaces [25].

There is an arrow from model A to model B in Figure 1 iff there exists a translation from processes representable in model A to processes representable in model B that fully respects branching time, causality, and their interplay. Thus a process and its translation ought to be history preserving bisimulation equivalent [26,11].

Part of the contribution of this paper is a definition of what this means. Forms of history preserving bisimulation were defined on behaviour structures in [26], on stable event structures in [11], and on Petri nets under the individual token interpretation in [4]; however, it has never been formally defined what it means for an event structure, for instance, to be history preserving bisimulation equivalent to a Petri net.

In Section 2 I introduce the model of higher dimensional automata. Then, in Sections 4, 5 and 6, I define behaviour preserving translations from the other models of Figure 1 into this model; for the model of Petri nets I do this in four different ways, corresponding to the four different computational interpretations of nets found in the literature. In Section 8 I define history preserving bisimulation equivalence on higher dimensional automata. The embeddings of the other models of concurrency into higher dimensional automata make this definition apply to processes representable in any of these models: two processes are equivalent iff their representations as higher dimensional automata are. Naturally, I have to ensure that the new definition agrees with the existing ones on the models where it has already been defined.

With this tool in hand, the hierarchy of Figure 1 is justified in Section 9. In particular, counterexamples will be presented to illustrate the strictness of the expressiveness ordering.

Besides history preserving bisimulation equivalence, I also define interleaving bisimulation equivalence [20,11] on higher dimensional automata, and thus on the other models, as well as ST-bisimulation equivalence [14], a branching time respecting semantic equivalence that takes causality into account to the extent that it can be expressed by the possibility of durational actions to overlap in time. If I compare the models merely up to interleaving bisimulation equivalence they turn out to be all equally expressive. If I compare them up to ST-bisimulation equivalence, I conjecture that just two equivalence classes of models remain: the models that do not take causality into account—in Figure 1 just the model of synchronisation trees—and the models that do—in Figure 1 all other models. It follows that the more interesting hierarchy of Figure 1 is due to causal subtleties that evaporate when considering processes up to ST-bisimulation equivalence.

2 Higher dimensional automata

One of the most commonly used models of concurrency is that of automata, also known as process graphs, state transition diagrams or labelled transition systems. In ordinary automata, the parallel composition P of two actions a and b is displayed in the same way as a system M that executes a and b in either order, ending in the same state each way, such that a and b are mutually exclusive (see Figure 2). Nevertheless, it is often important to tell these systems apart. This happens for instance when a and b take time: the total running time of M is at least the sum of the running times of a and b, whereas P may be as quick as the maximum of the running times of a and b. Another occasion where it is essential to distinguish between P and M is when designing systems using action refinement, as described in [11]. In many other models of concurrency P and M are represented distinctly. For the model of Petri nets, this is illustrated in Figure 2.

Throughout the years, people have wondered whether the elegance of automata could be combined with the expressiveness of models like Petri nets or event structures, that are able to capture causal relationships between action occurrences. These relationships include the causal independence of a and b in P, the dependence of b on a in the left branch of the automaton representing M,

P: • a •b  M: • a • •b

[figure: a; b; b; a]

Fig. 2. The automaton in the middle represents both parallelism, as does the Petri net P, and mutual exclusion, as does the Petri net M.

and the dependence of a on b in the right branch. As a result, several models of concurrency have been proposed that are essentially automata, upgraded with some extra structure to express causal independence [28,2,26,29,32].

In [7] it was pointed out that ordinary automata, without such extra structure, are already sufficiently expressive to capture these causal relationships. All that is needed is a reading of automata that assumes squares to represent concurrency, and nonconfluent branching to represent a choice or conflict. Under this concurrent interpretation the automaton of Figure 2 represents parallelism only, whereas mutual exclusion is represented by the automaton of Figure 3. The square of Figure 2 is now seen as the product of the transi-

[figure: a; b; b; a]

Fig. 3. Representation of mutual exclusion in ordinary automata under the concurrent interpretation

b a  a b

Fig. 4. Travelling through the inside of a square

tions a and b that form its sides. As each of these two transitions has 3 cells, a start node, an end node, and the edge between them, their product has 9 cells, namely the 4 nodes and 4 edges displayed in Figure 2, and the inside of the square. The latter represents the concurrent execution of a and b.

Modelling concurrency by means of squares (or cubes, hypercubes etc. in case of three or more concurrent actions) is particularly useful when actions are thought to have a duration or structure. A concurrent execution of a and b in the process a∥b can then be thought of as a continuous path through the surface of the square, starting at the top and terminating at the bottom node, while being nondecreasing when projected on any edge. The execution displayed in Figure 4 for instance passes through a point in which 50% of a and about 17% of b has happened. As long as we want to identify all such paths (when abstracting from timing information and structural knowledge of a and b) we simply represent their equivalence class as the square. In [15] this representation of concurrent systems turned out to be essential in finding and explaining an essential counterexample in the study of semantic equivalences.

The price to pay for this simple solution is that it is no longer possible to represent the system M of Figure 2 in such a way that both executions ab and ba end up in the same state. In order to overcome this deficiency, and to distinguish choice, as displayed in Figure 3, from mutual exclusion, as in M in Figure 2, Vaughan Pratt [24] preferred for every square, cube, hypercube etc. to indicate explicitly whether it represents concurrency or not. An n-dimensional hypercube that represents the concurrent execution of the n transitions that span its sides is thought of as being “filled in”, which is represented by an additional n-dimensional cell in the automaton. Those that represent mutual exclusion stay empty. This gives rise to what he baptised higher dimensional automata.

A totally sequential implementation of a system, in which no two actions happen in parallel, can be represented by an ordinary automaton, which is a higher dimensional automaton in which there are no higher dimensional cells, so no squares are filled in. At the other side of the spectrum, the very same ordinary automata under the concurrent interpretation of [7] form the special case of higher dimensional automata in which every (nondegenerate) square, cube or hypercube is filled in. In between, Pratt’s higher dimensional automata can model systems that feature both parallelism and mutual exclusion, without having to resort to untying the join of two branches that surround an area of mutual exclusion.

The idea of higher dimensional automata above had to some extent been contemplated before in [28] and applied in [23]. However, [24] offered the first formalisation of the idea. Pratt’s formalisation, based on n-categories, takes a globular or hemispherical approach, in which an n-cell has only two boundaries of dimension n − 1. Desperate attempts by me to fully grok the globular approach led to an exchange with Pratt in December 1990 that gave rise to the joint conclusion that a cubical approach, in which an n-cell has 2n boundaries of dimension n − 1, would be preferable (and easier to understand). A higher dimensional automaton (HDA) was henceforth defined as a presheaf over □, the category of cubical complexes.^{3} At the occasion of proposing notions of bisimulation equivalence, homotopy and unfolding for higher dimensional

3 The objects of □ are the symbols 0,1,2,... denoting the hypercubes of each dimension, and its morphisms from k to n are the embeddings of the k-dimensional hypercube as a k-dimensional face of the n-dimensional hypercube. All dimensions are directed and the morphisms preserve this direction. Thus, there are for example 6 morphisms from 2 to 3, corresponding to the fact that a cube has 6 sides. A presheaf over a category C is a functor F : C^{op} → Set. Thus a presheaf F over □ associates a set F (n) to every object n in □. F (n) is thought of as the set of n-dimensional hypercubes in the HDA. Also, for every morphism m : k → n, recognising the k-dimensional hypercube as a face of the n-dimensional one, there exists a function F (m) : F (n) → F (k), giving for every n-dimensional hypercube its k-dimensional face on the side indicated by m. These functions must satisfy exactly those composition laws that hold for the morphisms in □. The advantage of the categorical approach is that the concept of an HDA is thus completely defined without the need for figuring out these laws.

automata in [9], I reworded this definition in set-theoretical terms as follows.

Definition 1 A cubical set consists of a family of sets (Q_{n})_{n≥0} and for every n∈IN a family of maps s_{i}, t_{i} : Q_{n} → Q_{n−1} for 1 ≤ i ≤ n, such that

α_{i} ∘ β_{j} = β_{j−1} ∘ α_{i}  for all 1 ≤ i < j ≤ n and α, β ∈ {s, t}.  (*)

A higher dimensional automaton, labelled over an alphabet A, is a tuple (Q, s, t, I, F, l)^{4} with (Q, s, t) a cubical set, I ∈ Q_{0}, F ⊆ Q_{0} and l : Q_{1} → A, such that l(s_{i}(q)) = l(t_{i}(q)) for all q ∈ Q_{2} and i = 1, 2.

The elements of Q_{0} are called nodes and those of Q_{1}, Q_{2} and Q_{3} are edges, squares and cubes, respectively. In general, the elements of Q_{n} are called ndimensional hypercubes, or n-cells. An n-dimensional hypercube represents a state of a concurrent system in which n transitions are firing concurrently. Because the dimensions of the hypercube are numbered 1, …, n, these n transitions are de facto stored as a list.

An edge q connects 2 nodes: its source s_{1}(q) and its target t_{1}(q). Likewise, an n-dimensional hypercube q has n sources s_{i}(q) and n targets t_{i}(q), one in each dimension i = 1, ..., n, and each being an (n − 1)-dimensional hypercube. The source s_{i}(q) represents the possible state prior to q in which n − 1 out of n transitions are already firing, but the i^{th} one has not yet started. Likewise, t_{i}(q) represents the possible state past q in which n − 1 out of n transitions are still firing, but the i^{th} one has terminated.

When removing the i^{th} transition out of a list of n transitions, an implicit renumbering takes place, and what was formerly the j^{th} transition, for j > i, is now called the (j − 1)^{th} transition. Hence, first leaving out the j^{th} and then the i^{th}, with i < j, leaves us with the same list as first removing the i^{th} and then the (j − 1)^{th} transition. This is the content of the cubical laws (*).

I is the initial state, and F the set of final states of the represented system. These states are required to have dimension 0, meaning that no transition is currently firing. An edge q ∈ Q_{1} represents a state where exactly 1 transition is firing, and l indicates the label of that transition. It is required that opposite sides of a square have the same label. This is because they represent the same transition, scheduled before and after the firing of another one. The labelling function can trivially be extended to a labelling of arbitrary n-dimensional hypercubes by lists of n actions (cf. Section 7.2).

Based on this definition, and the computational motivation of Pratt [24], numerous papers on higher dimensional automata have emerged [33–72].

A semantics of CCS in terms of higher dimensional automata is provided in Goubault & Jensen [62], and also studied by Lanzmann [65]. In Goubault [54], higher dimensional automata are used as a semantic domain for richer lan-

4 I write Q for ⋃_{k=0}^{∞} Q_{k} and the families of all maps s_{i} and t_{i} are denoted s and t. The components of an HDA A are called Q^{A}, s^{A}, t^{A}, I^{A}, F^{A} and l^{A}, a convention that also applies to other structures given as tuples. When clear from context, the index A is omitted.

guages, and to compute local invariants which can decide a few computational properties of interest. Cridlig & Goubault [39] provide a semantics of Linda in terms of higher dimensional automata. Applications of higher dimensional automata to scheduling problems and wait-free protocols for distributed systems are studied by Goubault [55,56,58], and model checking applications by Cridlig [37,38]. Algorithms for deadlock detection in terms of higher dimensional automata appear in Fajstrup et al. [41,40]. Takayama [70,71,72] studies parallelisation algorithms by means of higher dimensional automata. Extensions of higher dimensional automata with time are investigated by Goubault [55,57].

In Goubault [60] the relations between 1-dimensional automata, asynchronous transition systems [28,2], and higher dimensional automata are cast in a categorical framework, following the work of Winskel & Nielsen [32]. To this end it appears to be fruitful to equip the cubical sets of Definition 1 with degeneracy mappings, so that they become exactly the cubical sets studied before in algebraic topology [27].

Homotopy for higher dimensional automata is defined in Pratt [24] and Van Glabbeek [9], and further investigated by Goubault [55,61] and Raussen [68]. Gunawardena [64] uses homotopy theory to show that 2-phase locking is safe. Goubault & Raussen [63] show, using homotopy theory, how geometric models of concurrency like higher dimensional automata are suitable for attacking the state-explosion problem.

Homology theories for higher dimensional automata are proposed by Goubault and Gaucher [62,55,42–52]. Gaucher [42–47], like Pratt [24], takes a globular approach to higher dimensional automata, and relates it to the cubical approach. Variations and generalisations of this approach are studied by Gaucher & Goubault [52,48–51].

Buckland et al. [34,35] study a simplified version of globular higher dimensional automata, and equip it with process algebraic operations. A generalisation of higher dimensional automata suitable for modelling continuous rather than discrete processes has been proposed by Sokolowsky [69].

In Cattani & Sassone [36] a simplified form of higher dimensional automata is proposed, called higher dimensional transition systems. The simplification is payed for in expressive power though: not all higher dimensional automata that arise as the image of a Petri net under the self-concurrent collective token interpretation (see Section 6) exist as higher dimensional transition systems.

An event oriented form of higher dimensional automata, called labelled step transition systems, appears in Van Glabbeek [53] and Badouel [33], where it is used to represent the behaviour of Petri nets.

In [66,67], Pratt argues that acyclic higher dimensional automata can be seen as subsets of a single infinite dimensional cube, which in turn can be modelled as Chu spaces over 3.

An overview of work related to higher dimensional automata and the use of other geometric methods in computer science is presented in Goubault [59].

3 Isomorphism of reachable parts

When used for representing concurrent systems, HDA need to be considered modulo a suitable semantic equivalence. One of the finest possible candidates is the following notion of isomorphism of reachable parts.

Definition 2 Two higher dimensional automata A and B are isomorphic if they differ only in the names of their cells, i.e. if there exists a dimension preserving bijection I : Q^{A} → Q^{B} between their cells, such that

• s_{i}^{B}(I(q)) = I(s_{i}^{A}(q)),

• t_{i}^{B}(I(q)) = I(t_{i}^{A}(q)),

• I(I^{A}) = I^{B},

• I(q) ∈ F^{B} ⇔ q ∈ F^{A},

• l^{B}(I(q)) = l^{A}(q) for q ∈ Q_{1}^{A}.

Definition 3 A cell q ∈ Q^{A} = ⋃_{n=0}^{∞} Q_{n}^{A} in a higher dimensional automaton A is reachable if it belongs to the smallest set R(A) ⊆ Q^{A} such that

• I^{A} ∈ R(A),

• if s_{i}(q) ∈ R(A) for some 1 ≤ i ≤ d(q) then q ∈ R(A), and

• if q ∈ R(A) and 1 ≤ i ≤ d(q) then t_{i}(q) ∈ R(A). Here d(q), the dimension of q, is n when q ∈ Q_{n}.

Thus, a cell q ∈ Q in an HDA A is reachable iff it occurs in a path of A as will be defined in Section 7.3. By definition R(A) is closed under the maps t_{i}. The following lemma shows that R(A) is also closed under the maps s_{i}. Its proof applies the cubical laws (*) of Definition 1.

Lemma 1 Let A be an HDA. If q ∈ R(A) and 1 ≤ i ≤ d(q) then s_{i}(q) ∈ R(A).

Proof. Define R_{k}(A) for k ∈ IN as the smallest sets of cells of A satisfying (1) I^{A} ∈ R_{0}(A),

(2) if s_{i}(q) ∈ R_{k}(A) for 1 ≤ i ≤ d(q) then q ∈ R_{k+1}(A), and

(3) if q ∈ R_{k}(A) and 1 ≤ i ≤ d(q) then t_{i}(q) ∈ R_{k+1}(A). Now R(A) = ⋃_{k=0}^{∞} R_{k}(A). With induction on k I show that if q ∈ R_{k+1}(A) and 1 ≤ i ≤ d(q) then s_{i}(q) ∈ R_{k}(A). Induction base (k = 0): If q ∈ R_{1}(A), then d(q) = 1 and s_{1}(q) = I^{A} ∈ R_{0}(A). Induction step (k > 0): Let q ∈ R_{k+1}(A) and 1 ≤ i ≤ d(q). By definition, either s_{j}(q) ∈ R_{k}(A) for some 1 ≤ j ≤ d(q), or q = t_{j}(q′) with q′ ∈ R_{k}(A) and 1 ≤ j ≤ d(q′).

Case 1: s_{j}(q) ∈ R_{k}(A) and i < j. By induction, s_{i}(s_{j}(q)) ∈ R_{k−1}(A). By a cubical law, s_{j−1}(s_{i}(q)) = s_{i}(s_{j}(q)) ∈ R_{k−1}(A), so s_{i}(q) ∈ R_{k}(A) by (2).

Case 2: The case s_{j}(q) ∈ R_{k}(A) with i = j is trivial.

Case 3: s_{j}(q) ∈ R_{k}(A) and i > j. By induction, s_{i−1}(s_{j}(q)) ∈ R_{k−1}(A). By a cubical law, s_{j}(s_{i}(q)) = s_{i−1}(s_{j}(q)) ∈ R_{k−1}(A), so s_{i}(q) ∈ R_{k}(A) by (2).

Case 4: q = t_{j}(q′) with q′ ∈ R_{k}(A) and i < j ≤ d(q′). By induction, s_{i}(q′) ∈ R_{k−1}(A), so t_{j−1}(s_{i}(q′)) ∈ R_{k}(A) by (3). By one of the cubical laws, s_{i}(q) = s_{i}(t_{j}(q′)) = t_{j−1}(s_{i}(q′)) ∈ R_{k}(A).

Case 5: q = t_{j}(q′) with q′ ∈ R_{k}(A) and j ≤ i ≤ d(q), i.e. j < i+1 ≤ d(q′). By induction, s_{i+1}(q′) ∈ R_{k−1}(A), so t_{j}(s_{i+1}(q′)) ∈ R_{k}(A) by (3). By a cubical law, s_{i}(q) = s_{i}(t_{j}(q′)) = t_{j}(s_{i+1}(q′)) ∈ R_{k}(A). □

By Lemma 1, the following concept of isomorphism of reachable parts, ≅_{R}, is well-defined.

Definition 4 The reachable part R(A) of an HDA A is the HDA consisting of its reachable cells: (R(A), s^{A} ^{\}R(A), t^{A} ^{\}R(A), I^{A}, F^{A} ^{\}R(A), l^{A} ^{\}R(A).

Write A ≅_{R} B if R(A) and R(B) are isomorphic.

When two HDA are isomorphic, then also their reachable parts are isomorphic. Thus, to check A ≅_{R} B it suffices to restrict A and B to subsets of Q^{A} and Q^{B} that contain all reachable states, and construct an isomorphism between the resulting HDA. This method will be applied in the proof of Theorem 2.

4 Embedding ordinary automata in HDA

A (1-dimensional) automaton is a tuple (Q_{0}, Q_{1}, s_{1}, t_{1}, I, F, l), the special case of a higher dimensional automaton in which Q_{n} = ∅ for n > 1. Often automata are required to be extensional, meaning that a transition is completely determined by its source, target and label:

s_{1}(q) = s_{1}(q′) ∧ t_{1}(q) = t_{1}(q′) ∧ l(q) = l(q′) ⇒ q = q′ for q, q′ ∈ Q_{1}.

In that case, a transition q ∈Q_{1} can be named after the triple (s_{1}(q), l(q), t_{1}(q)), and, writing S for the set of states Q_{0}, the quadruple (Q_{1}, s_{1}, t_{1}, l) can be conveniently represented by a relation T ⊆ S × A × S, thereby contracting the definition of an automaton to a quadruple (S, T, I, F).

A straightforward embedding of ordinary automata in higher dimensional automata is given by recognising them as HDA in which Q_{n} = ∅ for n > 1. However, the concurrent interpretation of automata from [7], elaborated in [10], yields a more expressive model of concurrency. Here an extensional 1dimensional automaton G = (S, T, I, F) is, in essence, seen as an abbreviation of a higher dimensional automaton A(G) by assuming that any nondegenerate n-dimensional hypercube that can be recognised in G is “filled in”, i.e. constitutes an n-dimensional cell in A(G). In [7,10] this was merely a computational interpretation of automata; here I use it to formally define A(G). An n-dimensional hypercube in G consists of a string ℓ = a_{1} ⋯ a_{n} ∈ A^{n} of n action labels and 2^{n} corners p_{ξ} ∈ S, with ξ ∈ {0, 1}^{n} ranging over the strings of n 0s and 1s, such that (p_{ξ}, a_{i}, p_{χ}) ∈ T whenever ξ and χ differ only on their i^{th} bit and that bit is 0 in ξ and 1 in χ. The source s_{i}(q) (resp. target t_{i}(q)) in dimension i of such an n-dimensional hypercube q in G is the (n − 1)- dimensional hypercube in G obtained by deleting a_{i} from ℓ and restricting the set of corners p_{ξ} of q to those in which the i^{th} bit of ξ is 0 (resp. 1).

A hypercube q = (ℓ, p_{ξ} (ξ ∈{0, 1}^{n})) in G is degenerate iff there are indices 1 ≤ i < j ≤ n such that a_{i} = a_{j} in ℓ and, for certain bits b_{k} ∈ {0, 1} (k ≠ i, j),

p_{b_{1}···b_{i−1}0b_{i+1}···b_{j−1}1b_{j+1}···b_{n}} = p_{b_{1}···b_{i−1}1b_{i+1}···b_{j−1}0b_{j+1}···b_{n}}.

In particular, a degenerate square consists of two transitions (p, a, q) and (q, a, r). It is a square by taking ℓ = aa and the corners p_{00} = p, p_{01} = p_{10} = q and p_{11} = r. The reason for not assuming this square to be filled in, is that if I do, I loose the expressive power to specify a sequence of two identical actions that have to occur in sequential order. Hence the property that at least all synchronisation trees are representable as automata under the concurrent interpretation would be lost. In general, a hypercube in G is nondegenerate iff all its 2-dimensional faces are nondegenerate. So the definition of degeneracy above is the most stringent one I could get away with.

5 Embedding event oriented models in HDA

Winskel [30,31] introduced six kinds of event structures: the prime, stable and [general] event structures, each optionally with the restriction of binary conflict. The behaviour of these event structures is fully specified by the families of configurations that can be associated to them; moreover, the family of all configurations of an event structure is fully determined by the finite configurations in the family. Hence, event structures embed faithfully in the model of (finitary) configuration structures of [12], which generalises the families of (finite) configurations of event structures.

In Figure 5, taken from [12], the six models of event structures from [30,31] are ordered with respect to their expressive power as measured by the class of (finitary) configuration structures they can denote. In addition, the figure includes the flow event structures of Boudol [5], and the bundle event structures of Langerak [18]. The synchronisation trees of Milner [20], which are just tree shaped (1-dimensional) automata, can be seen as special kinds of prime event structures with binary conflict, and, naturally, the maximal expressive power is obtained by the model of all (finitary) configuration structures.

In [11] a configuration structure was defined as follows.

Definition 5 A (labelled) configuration structure (over an alphabet A) is a triple C = (C, F, l) where C is a family of finite sets (the configurations), F ⊆ C a termination predicate, satisfying X ∈ F ∧ X ⊆ Y ∈ C ⇒ X = Y (i.e. terminating configurations must be maximal), and l : ⋃_{X∈C} X → A is a labelling function. The set E of events of C is defined by E := ⋃_{X∈C} X.

This definition differs from the one in [12] by not listing the set of events E in the tuple (E, C, F, l), thereby employing a coarser notion of isomorphism, by employing finite configurations only (this is called finitariness in [12]), and by the addition of the termination predicate, thereby distinguishing deadlock—a maximal but non-terminating configuration—from successful termination.

[figure: synchronisation trees [20]; prime event structures; with binary conflict [31]; bundle event structures [18]; flow event structures [5]; stable event structures; with binary conflict [31]; event structures; with binary conflict [31]; prime event structures [30]; stable event structures [30]; event structures [30]; rooted finitary configuration structures [11,12]]

Fig. 5. A hierarchy of event oriented models of concurrency

Definition 6 [11] A configuration structure C is

• rooted iff ∅ ∈ C^{C},

• connected iff ∅ ≠ X ∈ C^{C} ⇒ ∃e ∈ X : X − {e} ∈ C^{C},

• closed under bounded unions iff X, Y, Z ∈ C^{C}, X ∪ Y ⊆ Z ⇒ X ∪ Y ∈ C^{C},

• closed under bounded intersections iff X, Y, Z ∈C^{C}, X∪Y ⊆Z ⇒ X∩Y ∈C^{C},

• and stable iff it has all four properties above.

As observed in [30,12,11], a configuration structure arises as the family of finite configurations of an event structure iff F = ∅ and it is rooted, connected and closed under bounded intersections; it arises as the family of finite configurations of a stable event structure iff F = ∅ and it is stable.

In [10], the rooted finitary configuration structures are faithfully embedded in the model of ordinary automata under the concurrent interpretation of [7]. To this end, the concurrent interpretation of [7] was extended to cover all (extensional) automata—in [7] it applied merely to automata of a certain shape: the ones arising as the images of (labelled) prime event structures.

Definition 7 The extensional 1-dimensional automaton associated to a rooted finitary configuration structure C = (C, F, l) is G(C) = (C, T, ∅, F) with

(X, a, Y) ∈ T iff Y = X ._{∪} {e} for an event e with l(e) = a.

By composing the mappings of [12], embedding the models of Figure 5 in rooted finitary configuration structures, of [10], embedding the latter in automata under the concurrent interpretation, and of Section 4 above, embedding automata in HDA, all models of Figure 5 embed faithfully in HDA.

6 Embedding Petri nets in HDA

In this section I show that the model of higher dimensional automata is at least as expressive as the model of Petri nets, by giving translations from Petri nets to higher dimensional automata that capture exactly the dynamic behaviour of nets, as expressed by the firing rule, informally described below.

The essence of the material in this section appeared originally in [53], but using a different model of higher dimensional automata, called labelled step transition systems. Although extremely appealing as a model of concurrency, labelled step transition systems lack the expressiveness to crown the spectrum of Figure 1: they do not capture all ordinary automata under the concurrent interpretation.

Definition 8 A (labelled, marked) Petri net is a tuple (S, T, F, I, l) with • S and T two disjoint sets of places (Stellen in German) and transitions,

• F : (S × T ∪ T × S) → IN, the flow relation,

• I : S → IN, the initial marking,

• and l : T → A, for A a set of actions, the labelling function.

Petri nets are pictured by drawing the places as circles and the transitions as boxes, containing their label. For x,y ∈S∪T there are F (s,t) arcs from x to y.

When a Petri net represents a concurrent system, a global state of this system is given as a marking, a function M : S → IN. Such a state is depicted by placing M(s) dots (tokens) in each place s. The initial state is given by the marking I. A transition t can fire (occur) by taking F (s, t) tokens out of each place s, one for each arc from s to t. If this is possible in the state given by the marking M : S → IN, i.e. if F (s, t) < M(s) for all s ∈ S, one says that t is enabled under M. After t has fired, F (t, s) tokens are added to each place s, one of each arc from t to s. For t a transition in a Petri net N, let •t : S^{N} → IN be given by ^{•}t(s) = F (s, t) and t^{•} : S^{N} → IN by t^{•}(s) = F (t.s). The multiset ^{•}t describes which tokens are consumed by firing t, and t^{•} which tokens are produced.

In Van Glabbeek & Vaandrager [14], Petri nets were studied from the point of view that transitions may take time, and we introduced global states in which any number of transitions may be currently firing. The states represented by markings as defined above are those in which no transition is currently firing. In general, a state is given by a multiset of places and transitions. In order to precisely keep track of causal relationships between transition firings, we found it convenient to represent the (multi)set of transitions in a state as a list. This made it possible to distinguish different occurrences of currently firing transitions (i.e. the third and the fifth). Hence an ST-marking is defined as a pair (M, σ) ∈ ℳ(S) × T^{∗} of a multiset of places and a list of transitions. This is exactly the notion of state that I need below in my translations of Petri nets to higher dimensional automata.

As pointed out in [12], there are 2×2 = 4 computational interpretations of Petri nets, called the individual token and the collective token interpretation, and, orthogonally, the self-sequential and the self-concurrent interpretation. In the individual token interpretation one distinguishes different tokens residing in the same place, keeping track of where they come from. If a transition fires by using a token that has been produced by another transition, there is a causal link between the two. Consequently, the causal relations between the transitions in a run of a net can always be described by means of a partial order. In the collective token interpretation, on the other hand, tokens cannot be distinguished: if there are two tokens in a place, all that is present there is the number 2. This gives rise to more subtle causal relationships between transitions in a run of a net, which cannot be expressed by partial orders. In the self-concurrent interpretation, a transition may fire concurrently with itself. This is not allowed in the self-sequential interpretation.

The below can be understood as a way of formally pinpointing the differences between these computational interpretations, by giving four translations from Petri nets into higher dimensional automata, one for each interpretation. In some sense this amounts to giving four different semantics of Petri nets.

6.1 The self-concurrent collective token interpretation

First I define the higher dimensional automaton A_{CT}(N) associated to a Petri net N according to the self-concurrent collective token interpretation of nets. As cells of A_{CT}(N) I take the ST-markings of N, each being a pair (M, σ) of a multiset M of places and a list σ of transitions in N. The number of transitions in the list is the dimension of the cell. The source s_{i}(q) (resp. the target t_{i}(q)) in dimension i of a cell q = (M, σ) is obtained by omitting the i^{th} transition t from σ, and adding the multiset of places ^{•}t (resp. t^{•}) to M. Below, + denotes the union of multisets, given by (M +X)(s) = M(s)+X(s). The empty list is denoted ε. As there is no standard definition of successful termination in Petri nets, I map them to HDA without final states; however, for any definition of successful termination of Petri nets found in the literature, most likely a corresponding definition of the final states of the associated HDA can be obtained.

Definition 9 Let N be a Petri net. The higher dimensional automaton A_{CT}(N) = (Q, s, t, I, F, l) is given by

• Q_{n} = ℳ(S^{N}) × (T^{N})^{n} for n ∈ IN,

• s_{i}(M, t_{1} ⋯ t_{n}) = (M + ^{•}t_{i}, t_{1} ⋯ t_{i−1}t_{i+1} ⋯ t_{n}) for 1≤i≤n,

• t_{i}(M, t_{1} ⋯ t_{n}) = (M + t_{i}^{•}, t_{1} ⋯ t_{i−1}t_{i+1} ⋯ t_{n}) for 1≤i≤n,

• I = (I^{N}, ε) and F = ∅,

• l(M, t) = l^{N}(t) for (M, t) ∈ Q_{1}.

The source and target functions defined above correspond exactly to the start and termination of a transition firing as defined in clauses 2 and 4 of Definition 7.1.1 in [14]. They are also consistent with the informal description of the firing rule given above.

6.2 The self-concurrent individual token interpretation

Below I will define the notion of a token as it could occur in a Petri net, in such a way that all possible token occurrences have a different name. A token will be a triple (t′, k, s), with s the place where the token occurs, and t′ the transition firing that brought it there. For tokens that are in s initially, I take t′ = ∗. When the number of tokens that t′ deposits in s is n, I distinguish these tokens by giving them ordinal numbers k = 0, 1, 2, ..., n − 1. In order to define tokens as announced above I need to define transition firings simultaneously. These will be pairs (X, t) with t the transition that fires, and X the set of tokens that is consumed in the firing. Transitions t that can fire without consuming tokens can fire multiple times on the same (empty) input; these firings will be called (k, t) with k ∈ IN instead of (∅, t). I define the functions β from tokens to the places where they occur by β(x, k, s) = s, and η from transition firings to the transition that fires by η(x, t) = t. The function β extends to a function from sets of tokens X to multisets of places β(X) : S → IN, by β(X)(s) = |{s′ ∈ X | β(s′) = s}|.

Definition 10 Given a Petri net N = (S, T, F, I, l), the sets of tokens S_{•} and transition firings T_{•} of N are recursively defined by

• (∗, k, s) ∈ S_{•} for s ∈ S and k < I(s);

• (t′, k, s) ∈ S_{•} for s ∈ S, t′ ∈ T_{•} and k < F (η(t′), s);

• (X, t) ∈ T_{•} for t ∈ T and X ⊆ S_{•} such that β(X) = ^{•}t ≠ ∅;

• (k, t) ∈ T_{•} for k ∈ IN and t ∈ T such that ^{•}t = ∅.

Now I define the higher dimensional automaton A_{IT}(N) associated to a Petri net N according to the self-concurrent individual token interpretation of nets. First I will treat the case that N is a standard net, a net in which each transition has at least one incoming arc: ∀t ∈ T. ^{•}t > 0. A net is standard iff its set of spontaneous transition firings T_{∘} = {(k, t) ∈ T_{•} | k ∈IN} is empty.

As cells of A_{IT}(N) I take the ST-markings with individual tokens of N, each being a pair (M, σ) of a multiset M of tokens of N (each token allocated to a place in N) and a list σ of transition firings of N. The number of transition firings in the list is the dimension of the cell. The source s_{i}(q) in dimension i of a cell q = (M, σ) is obtained by omitting the i^{th} transition firing (X, t) from σ, and adding the set of tokens X to M. Likewise, the target t_{i}(q) of q in dimension i is obtained by omitting the i^{th} transition firing (X, t) from σ and upgrading M by adding F (t, s) tokens to each place s. Below, in applying the multiset union +, sets X are identified with multisets by taking X(s) = 1 if s∈X and X(s) = 0 otherwise.

Definition 11 Let N be a standard net. The higher dimensional automaton A_{IT}(N) = (Q,s,t,I,F, l) is given by

• Q_{n} = ℳ(S_{•}^{N}) × (T_{•}^{N})^{n} for n ∈ IN,

• s_{i}(M, t′_{1} ⋯ t′_{n}) = (M + X, t′_{1} ⋯ t′_{i−1}t′_{i+1} ⋯ t′_{n}) for 1≤i≤n and t′_{i} =(X, t),

• t_{i}(M, t′_{1} ⋯ t′_{n}) = (M + {(t′_{i}, k, s) | k <F^{N}(η(t′_{i}), s)}, t′_{1} ⋯ t′_{i−1}t′_{i+1} ⋯ t′_{n}),

• I = ({(∗, k, s) | k < I^{N}(s)}, ε) and F = ∅,

• l(M, t′) = l^{N}(η(t′)) for (M, t′) ∈ Q_{1}.

It may be helpful to observe that A_{CT}(N) can be obtained from A_{IT}(N) by applying β and η to the tokens and transition firings that make up a cell in A_{IT}(N); in particular one has s_{i}((β, η)(q)) = (β, η)(s_{i}(q)), and likewise for t_{i}.

The following proposition says that I succeeded in giving all possible token occurrences a different name: each reachable cell in A_{IT}(N) is an ST-marking with individual tokens (M, σ) of N in which M is a plain set. The reason to involve multisets of tokens in the definition above is to avoid the problems related to unions M ∪ X not being disjoint.

Proposition 1 For N a standard net and (M, σ) ∈ R(A_{IT}(N)) a reachable ST-marking with individual tokens, no token occurs twice in M, i.e. M is a plain set.

Proof. Define the direct causality relation ≺ between the tokens and transition firings of N by (1) s′ ≺ (X, t) for s′ ∈ X and (2) t′ ≺ (t′, k, s). Let <, the causality relation, be the transitive closure of ≺.

I claim that in any reachable ST-marking with individual tokens (M, σ) of N, no token occurs twice in M, no transition firing occurs twice in σ, and there are no tokens or transition firings x and y in (M, σ) such that x < y.

This follows with a straightforward induction on reachability, using for the s_{i}(q)-clause that y < (X, t) ⇔ ∃x ∈ X : y ≤ x, and for the t_{i}(q)-clause that y < (t′_{i}, k, s) ⇔ y ≤ t′_{i}. □

For non-standard nets the question arises how to generalise the second clause in Definition 11 to transition firings of the form (k, t) with k ∈ IN. The simplest solution would be to treat such firings as (∅, t). However, this would lead to a failure of Proposition 1 for non-standard nets, as a spontaneous transition firing (k, t) could occur multiple times in a firing sequence, leaving multiple copies of its output tokens in the resulting reachable ST-marking.

Instead, I want to ensure that each spontaneous transition firing may only occur once in a run of a Petri net. This requirement is motivated by the idea that every time a transition t with ^{•}t = 0 fires, its firing gets a different identifier. Thus, my notion of state should incorporate, besides the information contained in an ST-marking with individual tokens, some bookkeeping to remember which spontaneous transition firings are still possible. This I do by adding to the place-component of an ST-marking the set of names ^{t}k of all spontaneous transition firings (k, t) ∈ T_{0} that may still occur.

Definition 12 Let N be net. The HDA A_{IT}(N) = (Q,s,t,I,F, l) is given by • Q_{n} = ℳ(S_{•}^{N} ∪ {^{t}k | (k, t) ∈ T_{0}}) × (T_{•}^{N})^{n} for n ∈ IN,

• s_{i}(M, t′_{1} ⋯ t′_{n}) = (M + X, t′_{1} ⋯ t′_{i−1}t′_{i+1} ⋯ t′_{n}) for 1≤i≤n and t′_{i} =(X, t), s_{i}(M, t′_{1} ⋯ t′_{n}) = (M + {^{t}k}, t′_{1} ⋯ t′_{i−1}t′_{i+1} ⋯ t′_{n}) for 1≤i≤n and t′_{i} =(k, t),

• t_{i}(M, t′_{1} ⋯ t′_{n}) = (M + {(t′_{i}, k, s) | k <F^{N}(η(t′_{i}), s)}, t′_{1} ⋯ t′_{i−1}t′_{i+1} ⋯ t′_{n}),

• I = ({(∗, k, s) | k < I^{N}(s)} ∪ {^{t}k | (k, t) ∈ T_{0}}, ε) and F = ∅,

• l(M, t′) = l^{N}(η(t′)) for (M, t′) ∈ Q_{1}.

With this definition, Proposition 1 generalises straightforwardly.

Corollary 1 For N a net and (M, σ) ∈ R(A_{IT}(N)), M is a plain set. □

6.3 The self-sequential interpretations

A self-sequential version A_{CT}^{ss} of the collective token interpretation of Petri nets into higher dimensional automata is obtained by only allowing, in the first clause of Definition 9, cells (M, σ) in which no transition occurs twice in σ. Likewise, on standard nets, a self-sequential version of the individual token interpretation above is obtained by only allowing cells (M, t′_{1} ⋯ t′_{n}) such that η(t′_{i}) = η(t′_{j}) ⇒ i = j.

On non-standard nets, before employing the same definition, I take the opportunity to rectify an unfortunate aspect of the map A_{IT} that was unavoidable under the self-concurrent interpretation. Namely, if a net contains a transition t without input places, Definition 12 yields an infinitely branching HDA: the initial transition firing can be any (k, t) for k ∈ IN. The reason this is unavoidable under the self-concurrent interpretation is that any number of transition firings (k, t) can happen simultaneously (can occur in one ST-marking with individual tokens), and I want the interpretation to preserve the fundamental property of Petri nets that whenever a number of transition firings can happen in one step, they can happen in any order; so any of the firings (k, t) can happen first. Under the self-sequential interpretation, on the other hand, it is much more natural so take the point of view that although the transition t allows arbitrary many firings to occur sequentially, there is no point in distinguishing different kinds of first firings. Thus, I will use k not merely as a label taken from an arbitrary countable set, but as an actual number, (k, t) denoting the k+1^{th} firing of transition t. Thus, the presence of t_{k} in a state signifies that the k+1^{th} firing of t is enabled.

Definition 13 Let N be net. The HDA A_{IT}^{ss}(N) = (Q,s,t,I,F, l) is given by • Q_{n} ={(M, t′_{1} ⋯ t′_{n}) ∈ ℳ(S_{•}^{N} ∪ {^{t}k | (k, t)∈T_{0}}) × (T_{•}^{N})^{n} |

η(t′_{i}) = η(t′_{j}) ⇒ i = j} for n ∈ IN,

• s_{i}(M, t′_{1} ⋯ t′_{n}) = (M + X, t′_{1} ⋯ t′_{i−1}t′_{i+1} ⋯ t′_{n}) for 1≤i≤n and t′_{i} =(X, t), s_{i}(M, t′_{1} ⋯ t′_{n}) = (M + {^{t}k}, t′_{1} ⋯ t′_{i−1}t′_{i+1} ⋯ t′_{n}) for 1≤i≤n and t′_{i} =(k, t),

• t_{i}(M, t′_{1} ⋯ t′_{n}) = \begin{matrix}(M + \{(t′_{i}, k, s) | k <F^{N}(η(t′_{i}), s)\} ∪ \{^{t}(k+1) | t′_{i} = (k, t)\}, \\ t′_{1} ⋯ t′_{i−1}t′_{i+1} ⋯ t′_{n}), \end{matrix}

• I = ({(∗, k, s) | k < I^{N}(s)} ∪ {^{t}0 | t ∈ T_{0} ∧^{•}t = 0}, ε) and F = ∅,

• l(M, t′) = l^{N}(η(t′)) for (M, t′) ∈ Q_{1}.

Corollary 2 For N a net and (M, σ) ∈ R(A_{IT}^{ss}(N)), M is a plain set. □

6.4 The relative expressiveness of the four interpretations

Each of the four computational interpretations above makes a different model of concurrency out of Petri nets. These models can now be compared with respect to their expressive power in denoting higher dimensional automata. A first result is easily obtained: Petri nets under the self-concurrent collective token interpretation are at least as expressive as Petri nets under the self-concurrent individual token interpretation, in the sense that any higher dimensional automaton that can be denoted by a net under the self-concurrent individual token interpretation can also be a denoted by a net under the selfconcurrent collective token interpretation.

Theorem 1 For every net N there is a net N_{•} such that A_{CT}(N_{•}) = A_{IT}(N).

Proof. N_{•} = (S_{•} ∪ {^{t}k | (k, t) ∈ T_{0}}, T_{•}, F_{•}, I_{•}, l_{•}) with

• S_{•} and T_{•} as in Definition 10.

• F_{•}(s′, t′) = 1 if t′ = (X, t) with s′ ∈ X, or t′ = (k, t) ∈ T_{∘} and s′ = ^{t}k; F_{•}(s′, t′) = 0 otherwise.

• F_{•}(t′, s′) = 1 if s′ has the form (t′, k, s); F_{•}(t′, s′) = 0 otherwise.

• I_{•}(∗, k, s) = I_{•}(^{t}k) = 1 and I_{•}(t′, k, s) = 0 for t′ ∈ T_{•}.

• l_{•}(t′) = l^{N}(η(t′)) for t′ ∈ T_{•}.

That A_{CT}(N_{•}) = A_{IT}(N) is straightforward. □

The net N_{•} constructed above is a close relative of the unfolding of a Petri net into an occurrence net, as defined in [30,6,19]. The difference is that I have not bothered to eliminate unreachable places and transitions. In [53] I define the unfolding of an arbitrary Petri net N as the reachable part of N_{•}. This construction extends the unfolding construction of [30,6,19] by applying also to non-standard nets.

In general, results as strong as Theorem 1 can not be obtained: in order to compare expressiveness in a meaningful way, processes represented by higher dimensional automata, Petri nets, or other models of concurrency should be regarded modulo some semantic equivalence relation. A particularly fine equivalence relation that allows one to totally order the computational interpretations of Petri nets is isomorphism of reachable parts of HDA.

The following theorem shows that, up to isomorphism of reachable parts of associated HDA, the behaviour of nets under the self-sequential interpretations can easily be encoded into the behaviour of nets under the corresponding selfconcurrent interpretation.

Theorem 2 For any net N there is a net N^{ss} such that A_{CT}(N^{ss}) ≅_{R} A_{CT}^{ss}(N) and A_{IT}(N^{ss}) ≅_{R} A_{IT}^{ss}(N).

Proof. Following [17], N^{ss} is obtained from N by adding for every transition t a self-loop, consisting of a place s_{t} with I(s_{t}) = F (s_{t}, t) = F (t, s_{t}) = 1 and F (s_{t}, u) = F (u, s_{t}) = 0 for all u ≠ t. Write S_{new} for the set of new places s_{t}.

To check that A_{CT}(N^{ss}) ≅_{R} A_{CT}^{ss}(N), restrict the cells of A_{CT}(N^{ss}), i.e. the ST-markings (M, σ) of N^{ss}, to the ones in which each transition t occurs at most once in σ, M(s_{t}) = 1 when t does not occur in σ, and M(s_{t}) = 0 when t does occur in σ. This set of cells surely contains all reachable ones. Let I(M, σ) ∈ ℳ(S^{N}) × (T^{N})^{∗} be obtained by restricting the domain of M : S ∪ S_{new} → IN to S, and leaving σ invariant. The bijection I constitutes an isomorphism of reachable parts between A_{CT}(N^{ss}) and A_{CT}^{ss}(N).

To check that A_{IT}(N^{ss}) ≅_{R} A_{IT}^{ss}(N), restrict the cells of A_{IT}(N^{ss}), i.e. the ST-markings with individual tokens (M, t′_{1} ⋯ t′_{n}) of N^{ss}, to the ones satisfying η(t′_{i}) = η(t′_{j}) ⇒ i = j, such that there is at most one token of the form (x, 0, s_{t}) in M for each s_{t} ∈ S_{new}, and none when η(t_{i}) = t for some 1 ≤ i ≤ n. This set of states surely contains all reachable ones. Also, in view of Corollaries 1 and 2, the cells of A_{IT}(N^{ss}) and A_{IT}^{ss}(N) may be restricted to pairs (M, σ) with M a set of tokens and names of spontaneous transition firings, rather than a multiset. Let S_{∘} = {s_{t} ∈ S_{new} | ^{•}t = 0 (in N)}. For s_{t} ∈ S_{∘}, let s_{t}^{0} = (∗, 0, s_{t}) and s_{t}^{k+1} = (({s_{t}^{k}}, t), 0, s_{t}). Then all tokens (x, k, s_{t}) of N^{ss} are of the form s_{t}^{k} for k ∈ IN. Now the mappings \overline{η} from the transition firings in N^{ss} to the transition firings in N, for convenience extended with \overline{η}(∗) = ∗, and \overline{β} from sets of tokens in N^{ss} to sets of tokens and names of spontaneous transition firings in N, are defined with recursion on the structure of transition firings

and sets of tokens by \overline{η}(X, t) = \begin{cases}(\overline{β}(X), t) if & ^{•}t ≠ 0 \\ (k, t) if & ^{•}t = 0 ∧ X = \{s_{t}^{k}\} \end{cases}

and \overline{β}(X) = \{(\overline{η}(x), k, s) | (x, k, s)∈X ∧ s∉S_{new}\} ∪ \{^{t}k | s_{t}^{k} ∈X ∧ s_{t} ∈S_{∘}\}. The bijection I given by I(M, t′_{1} ⋯ t′_{n}) = (\overline{β}(M), \overline{η}(t_{1}) ⋯ \overline{η}(t_{n})) constitutes an isomorphism of reachable parts between A_{IT}(N^{ss}) and A_{IT}^{ss}(N). □

By Theorem 2, any HDA that can be denoted by a Petri net under the selfsequential collective token interpretation, can also be denoted by a net under the self-concurrent collective token interpretation, and likewise for nets under the individual token interpretations. The construction of N^{ss} above, reducing the self-sequential to the self-concurrent interpretation of nets, is well known [17]. The point of the proof above is to some extent just a sanity check on the definitions of A_{CT}, A_{CT}^{ss}, A_{IT} and A_{IT}^{ss}.

The following strengthening of Theorem 2 says that the self-sequential collective token interpretation is subsumed by the self-concurrent collective token interpretation, in the sense that, up to isomorphism of reachable parts of associated HDA, the class of all Petri nets under the self-sequential collective token interpretation is equally expressive as a subclass of nets on which the two interpretations coincide. Likewise, the self-sequential individual token interpretation is subsumed by the self-concurrent individual token one.

Definition 14 A Petri net is self-sequential if in no reachable ST-marking a transition occurs twice.

Theorem 3 Let N be a Petri net.

(1) Then N^{ss} is self-sequential, A_{CT}^{ss}(N^{ss})≅_{R} A_{CT}^{ss}(N) and A_{IT}^{ss}(N^{ss})≅_{R} A_{IT}^{ss}(N).

(2) If N is self-sequential, then A_{CT}^{ss}(N) ≅_{R} A_{CT}(N) and A_{IT}^{ss}(N) ≅_{R} A_{IT}(N).

Proof. If N is self-sequential, trivially R(A_{CT}^{ss}(N)) = R(A_{CT}(N)), and therefore A_{CT}^{ss}(N) ≅_{R} A_{CT}(N). Likewise, R(A_{IT}^{ss}(N)) = R(A_{IT}(N)), considering that self-sequential nets can have no transitions t with ^{•}t = 0. This yields (2).

That N^{ss} is self-sequential is trivial, and, using this, the remaining statements in (1) follow from (2) and Theorem 2. □

Theorem 4 below says that, up to isomorphism of reachable parts of associated HDA, the two individual token interpretations are equally expressive, and subsumed by each of the collective token interpretations: the class of all Petri nets under either of the individual token interpretations is equally expressive as a subclass of nets on which all four interpretations coincide.

Definition 15 A Petri net is a unique-occurrence net if ∀t ∈ T. ^{•}t > 0 (i.e. it is a standard net), ∀s ∈ S. I(s) + Σ_{t∈T} F (t, s) = 1 and the flow relation F is well-founded, i.e. there is no infinite alternating sequence x_{0}, x_{1}, … of places and transitions such that F (x_{i+1}, x_{i}) > 0 for i ∈ IN.

This class of nets is a close relative of the class of occurrence nets of Winskel [30]; it just lacks the requirements that cause the elimination of unreachable places and transitions.

Definition 16 Two Petri nets P and Q are isomorphic, written P ≅ Q, if they differ only in the names of their places and transitions, i.e. if there are bijections β : S^{P} → S^{Q} and η : T^{P} → T^{Q} such that, for s ∈ S^{P} and t ∈ T^{P}: I^{Q}(β(s)) = I^{P}(s), F^{Q}(β(s), η(t)) = F^{P}(s, t), F^{Q}(η(t), β(s)) = F^{P}(t, s) and l^{Q}(η(t)) = l^{P}(t).

Lemma 2 For every Petri net N, the net N_{•} is a unique-occurrence net. Moreover, if N is a unique-occurrence net, then N_{•} ≅ N.

Proof. The first statement follows immediately from the construction of N_{•}, the well-foundedness of F (i.e. the well-foundedness of ≺ in the proof of Proposition 1) being a consequence of the recursive nature of Definition 10.

The second statement follows with induction on the well-founded order F, using the mappings β and η of Section 6.2. □

Lemma 2 tells that in a unique-occurrence net there is a bijective correspondence between places and token occurrences, and between transitions and transition firings. In particular, in a run of a net each place will be visited at most once, and each transition will fire at most once. Hence the name “uniqueoccurrence nets”. It follows that unique-occurrence nets are self-sequential.

Theorem 4 Let N be a Petri net.

(1) Then N_{•} is a unique-occurrence net satisfying A_{IT}(N_{•}) ≅_{R} A_{IT}(N).

(2) (N^{ss})_{•} is a unique-occurrence net satisfying A_{IT}^{ss}((N^{ss})_{•}) ≅_{R} A_{IT}^{ss}(N).

(3) If N is a unique-occurrence net, then

A_{IT}^{ss}(N) ≅_{R} A_{IT}(N) ≅_{R} A_{CT}(N) ≅_{R} A_{CT}^{ss}(N).

Proof. The left and right statement of (3) follow from Theorem 3, given that unique-occurrence nets are self-sequential. As it is easy to check that P ≅ Q ⇒ A_{CT}(P) ≅ A_{CT}(Q) for Petri nets P and Q, Lemma 2 implies that A_{CT}(N_{•}) ≅ A_{CT}(N) for unique-occurrence nets N. Together with Theorem 1, this yields the middle statement of (3). By Lemma 2, N_{•} and (N^{ss})_{•} are unique-occurrence nets. Finally, A_{IT}(N_{•}) ≅_{R} A_{CT}(N_{•}) ≅_{R} A_{IT}(N) by (3) and Theorem 1, and A_{IT}^{ss}((N^{ss})_{•}) ≅_{R} A_{CT}((N^{ss})_{•}) ≅_{R} A_{IT}(N^{ss}) ≅_{R} A_{IT}^{ss}(N) by (3), Theorem 1 and Theorem 2. □

Together, Theorems 1 and 2 yield the expressiveness hierarchy of Figure 6.

[figure: self-sequential individual token interpretation; self-concurrent individual token interpretation; self-sequential collective token interpretation; self-concurrent collective token interpretation]

Fig. 6. Relative expressiveness of four computational interpretations of Petri nets

Motivated by this hierarchy, the self-concurrent collective token interpretation of Petri nets will be my default; this is the interpretation that comes with the Petri net entries in Figure 1. Instead of comparing the expressiveness of Petri nets under any of the other interpretations with that of other models of concurrency one can just as well talk about the expressiveness of the relevant subclass of Petri nets.

In order to integrate the hierarchies of Figures 5 and 6, it pays to consider higher dimensional automata up to a semantic equivalence coarser than isomorphism of reachable parts. I will define such equivalences in Section 8, using the material of Section 7. It turns out that up to history preserving bisimulation equivalence the self-sequential and the self-concurrent collective token interpretations of Petri nets coincide.

7 Homotopy for higher dimensional automata

7.1 Naming the faces of n-cells

In order to name the faces of a hypercube, following [67], I use the bits 0, and 1 to indicate whether a transition has not yet started, is active, or has terminated, respectively. In other work, the bit is sometimes called \frac{1}{2}, A, or T for active or in transition, and yet others use the bits 0, 1, 2, or −, 0, +.

Since an n-cell represents a list of n transitions being active concurrently, each of its 3^{n} faces can be represented by a list b_{1} ⋯ b_{n} of n such bits, where b_{i} indicates the status of the i^{th} transition in the list. Thus, the dimension of the face b_{1} ⋯ b_{n} is given by the number of s in the list, ⋯ is the identity map, and ⋯ 0 ⋯ (resp. · · · 1 ⋯), with only b_{i} ≠ , denotes the map s_{i} (resp. t_{i}). The face b_{1} ⋯ b_{n} can also be expressed as α_{1} ∘ … ∘ α_{n} with α_{i} = s_{i} if b_{i} = 0, α_{i} = t_{i} if b_{i} = 1, and α_{i} = Id, the identity map, if b_{i} = . Using this convention, the 2^{n} 0-dimensional corners of an n-cell q are named by lists b_{1} ⋯ b_{n} with b_{i} ∈ {0, 1}, and the n · 2^{n−1} 1-dimensional edges of q by lists containing exactly one occurrence of .

7.2 Labelling n-cells

As an HDA is required to satisfy l(s_{i}(q)) = l(t_{i}(q)) for all q ∈ Q_{2} and i = 1, 2, it follows that, for each q ∈ Q_{n} and each 1 ≤ i ≤ n, the 2^{n−1} edges b_{0} ⋯ b_{i−1} b_{i+1} ⋯ b_{n} of q, with b_{j} ∈ {0, 1} for j ≠ i, all have the same label. Calling this label l_{i}(q), the labelling function l : Q_{1} → A can be extended to Q := ⋃_{k=0}^{∞} Q_{k} by l(q) = l_{1}(q) ⋯ l_{n}(q) for q ∈ Q_{n}. Thus, the label of an n-dimensional hypercube q is the list of the labels of the n transitions whose concurrent execution is represented by q.

7.3 Paths and their observable content

Definition 17 A path in a higher dimensional automaton (Q, s, t, I, F, l) is a sequence of pairs (∂_{1}, q_{1})(∂_{2}, q_{2}) ⋯ (∂_{m}, q_{m}), denoted I^{\underline{∂_{1}}} q_{1}^{\underline{∂_{2}}} q_{2}^{\underline{∂_{3}}} ⋯ ^{\underline{∂_{m}}} q_{m}, with q_{k} ∈ Q and ∂_{k} ∈ {s_{i}, t_{i} | i ≥ 1} for 1 ≤ k ≤ m, such that

q_{k−1} = s_{i}(q_{k}) if ∂_{k} = s_{i}  and  q_{k} = t_{i}(q_{k−1}) if ∂_{k} = t_{i}.

Here q_{0} := I, i.e. I consider only paths starting from the initial state. One writes end(π) for q_{m}.

A path π in an HDA A represents a partial run of the system represented by A in which between every two consecutive states an action starts or terminates. It represents a total run iff end(π) ∈ F. If ∂_{k} = s_{i}, the transition from q_{k−1} to q_{k} represents the start of the action l_{i}(q_{k}), and if ∂_{k} = t_{i}, it represents the termination of the action l_{i}(q_{k−1}).

Definition 18 Write split-trace(π) for the sequence σ_{1} ⋯ σ_{m}, where σ_{k} = l_{i}(q_{k})^{+} if ∂_{k} = s_{i}, and σ_{k} = l_{i}(q_{k−1})^{−} if ∂_{k} = t_{i}.

Split-trace(π) approximates the observable content of a path π. It consists of the sequence of starts a^{+} and terminations a^{−} of actions a occurring during the run represented by π. The HDA of Figure 2 in which the square is not filled in, for instance, has only two maximal paths, whose split-traces are a^{+}a^{−}b^{+}b^{−} and b^{+}b^{−}a^{+}a^{−}. (The prefixes of these sequences are also split-traces of paths.) The HDA of Figure 2 in which the square is filled in moreover has paths with split-traces like a^{+}b^{+}b^{−}a^{−}.

If it is possible to keep track of parallel occurrences of the same action, a split-trace falls short of representing the full observable content of a path. The observable behaviour of a real-time execution would consist of a set of action occurrences, with for each action occurrence an interval given by a start time and a termination time, indicating the period during with the action takes place. Abstracting from real-time information, what remains is a splittrace σ—a sequence σ = σ_{1} ⋯ σ_{m} of action phases, each being a start a^{+} or a termination a^{−} of an action a—together with an injective function start from the (indices of) termination phases in σ to the (indices of) start phases in σ. This function tells for every termination of an action occurrence in σ where that action occurrence starts. Naturally, for every termination phase σ_{ℓ} = a^{−} in σ, one has start(ℓ) < ℓ and σ_{start(ℓ)} = a^{+}. Such an annotated split-trace is called an ST-trace. It can be compactly represented by writing a^{start(ℓ)} for σ_{ℓ} whenever σ_{ℓ} = a^{−}. A formal definition of the ST-trace of a path in a higher dimensional automaton will follow in Section 7.5.

b^{+} a^{+} a^{+} b^{−} a^{+} a^{−} b^{+} a^{−}

Fig. 7. An ST-trace

A typical ST-trace is depicted as Figure 7. It lists the starts and terminations of actions occurring in a path, and additionally links the start and termination of the same action. Its compact representation is b^{+}a^{+}a^{+}b^{1}a^{+}a^{3}b^{+}a^{5}. Note that it contains more information than the underlying split-trace. ST-traces were introduced in [8] in the context of event structures. Arguably, they constitute the best formalisation of the observable content of execution paths.

Paths and their ST-traces lack the possibility to express that action phases happen simultaneously. However, in higher dimensional automata two action phases can occur simultaneously iff they can occur in either order. Therefore, considering only paths in which all action phases are totally ordered does not lead to a decrease in expressive power.

7.4 Homotopy

Two paths in a higher dimensional automaton can be considered equivalent if they differ merely in the timing of causally independent actions. This applies for instance to the path ab and the path ba in the automaton of Figure 4, given that the actions a and b are causally independent. However, it would not apply when the square is not filled in, as this signifies mutual exclusion, and the relative order of a and b would matter. As observed by Pratt [24], this notion of equivalence can be formalised beautifully by means of what he calls “monoidal homotopy”. When seeing a higher dimensional automaton as a structure composed of higher dimensional cubes embedded in a higher dimensional Euclidean space, two paths are homotopic if one can be obtained out of the other by a continuous transformation, keeping the begin and endpoints the same, and allowing as intermediate stages of the transformation arbitrary paths going through the insides of higher dimensional cells, as long as they are monotonically increasing when projected on the axes of the cells they are going through. The path drawn in Figure 4 for instance could be one of the uncountably many stages in the continuous transformation of ab into ba.

This form of homotopy differs from the standard homotopy used in topology in that the directed nature of the underlying space needs to be preserved during transformations. Therefore it is called monoidal homotopy [24], or directed homotopy (dihomotopy) [63], as opposed to group homotopy, although in the context of higher dimensional automata it is simply called homotopy.

The following discrete analog of continuous deformation defines the same concept of homotopy without involving the notion of Euclidean space.

Definition 19 Two paths π and π′ are adjacent—denoted π ↔ π′—if one can be obtained from the other by replacing, for q, q′ ∈ Q and i < j,

• a segment ^{\underline{s_{i}}} q^{\underline{s_{j}}} by ^{\underline{s_{j−1}}} q′^{\underline{s_{i}}},

• a segment ^{\underline{t_{j}}} q^{\underline{t_{i}}} by ^{\underline{t_{i}}} q′^{\underline{t_{j−1}}} ,

• a segment ^{\underline{s_{i}}} q^{\underline{t_{j}}} by ^{\underline{t_{j−1}}} q′^{\underline{s_{i}}},

• or a segment ^{\underline{s_{j}}} q^{\underline{t_{i}}} by ^{\underline{t_{i}}} q′^{\underline{s_{j−1}}} . Homotopy is the reflexive and transitive closure of adjacency.

The third adjacency replacement above can be motivated as follows: suppose we have a list of n actions, numbered 1 to n, and we first insert an action a at position i (thereby incrementing the slot-numbers ≥ i by one) and subsequently delete the j^{th} action (j > i) from the list (thereby decrementing the slot-numbers >j by one), then we get the same result as when we first delete the (j − 1)^{th} action (thereby decrementing the slot-numbers ≥ j by one) and subsequently insert the action a at position i (incrementing the slot-numbers ≥i). The other replacements are motivated in a similar way.

The paths with split-traces a^{+}a^{−}b^{+}b^{−} and b^{+}b^{−}a^{+}a^{−} in Figure 4 for instance are homotopic, because the first can be transformed into the second through four adjacency replacements, namely (on the level of split-traces)

a^{+}a^{−}b^{+}b^{−} ↔ a^{+}b^{+}a^{−}b^{−} ↔ b^{+}a^{+}a^{−}b^{−} ↔ b^{+}a^{+}b^{−}a^{−} ↔ b^{+}b^{−}a^{+}a^{−}.

Homotopic paths share their endpoints. A homotopy class of paths in a higher dimensional automaton (with endpoint q) is called a history (of q). Histories form the analog of paths, after abstraction from the order of causally independent action occurrences.

7.5 Matching starts and terminations of action occurrences in paths

The following proposition illustrates the agreement between Definition 19 and the cubical laws of Definition 1.

Proposition 2 For every segment p^{\underline{s_{i}}} q^{\underline{t_{j}}} r with i ≠ j, and for every segment p^{\underline{s_{i}}} q^{\underline{s_{j}}} r or p^{\underline{t_{i}}} q^{\underline{t_{j}}} r in a path π in an HDA A, there exists a unique path π′ in A, adjacent to π, that can be obtained from π by replacing the indicated segment in the manner described in Definition 19 (going either right or left).

Proof. Suppose π contains p^{\underline{s_{i}}} q^{\underline{t_{j}}} r, with i < j. Then p = s_{i}(q) and r = t_{j}(q). By the cubical laws in Definition 1, t_{j−1}(p) = t_{j−1}((s_{i}(q)) = s_{i}(t_{j}(q)) = s_{i}(r). Hence the unique replacement is p^{\underline{t_{j−1}}} q′^{\underline{s_{i}}} r with q′ = t_{j−1}(p) = s_{i}(r).

Likewise, suppose π contains p^{\underline{s_{i}}} q^{\underline{s_{j}}} r, with i < j. Then p = s_{i}(q) and q = s_{j}(r). By the cubical laws (*) in Definition 1 one has p = s_{j−1}(s_{i}(r)). So the unique replacement is p^{\underline{s_{j−1}}} q′^{\underline{s_{i}}} r with q′ = s_{i}(r).

The other four cases go similarly. □

The intuition is that when two actions happen concurrently, they can start in either order as well as terminate in either order; moreover, if it is possible for action a to start before b terminates, b could just as well terminate before a starts, provided a and b are distinct action occurrences. Note, however, that Proposition 2 does not apply to segments p^{\underline{t_{i}}} q^{\underline{s_{j}}} r. If the termination of one action precedes the start of another, it may be that there is a causal link between the two that prevents this order from being interchanged.

Definition 20 Two paths π and π′ are ℓ-adjacent—denoted π ↔^{ℓ} π′—if π′ can be obtained from π = I^{\underline{∂_{1}}} q_{1}^{\underline{∂_{2}}} q_{2}^{\underline{∂_{3}}} ⋯ ^{\underline{∂_{m}}} q_{m} (m > ℓ) by an adjacency replacement of the segment ^{\underline{∂_{ℓ}}} q_{ℓ}^{\underline{∂_{ℓ+1}}} of π, inducing a swap of the action phases σ_{ℓ} and σ_{ℓ+1} in the split-trace σ = σ_{1} ⋯ σ_{m} of π.

Assume ∂_{ℓ+1} = t_{i}, i.e. σ_{ℓ+1} is the termination l_{i}(q_{ℓ})^{−} of an action l_{i}(q_{ℓ}). In case ∂_{ℓ} = s_{i} we have that σ_{ℓ} is the start l_{i}(q_{ℓ})^{+} of the very same occurrence of the action l_{i}(q_{ℓ}) in π. In this case σ_{ℓ} and σ_{ℓ+1} cannot be swapped: there is no path π′ such that π ↔^{ℓ} π′. Proposition 2 tells that in all other cases (i.e. when ∂_{ℓ} ≠ s_{i}) σ_{ℓ} and σ_{ℓ+1} can be swapped: there exists a unique path π′ in A with π ↔^{ℓ} π′. This makes it possible to tell which action phase in split-trace(π) is the start of the action occurrence whose termination happens as phase σ_{ℓ+1}: it is

the unique phase σ_{k} such that π ⟷^{ℓ} π_{ℓ} ⟷^{ℓ−1} π_{ℓ−1} ⟷^{ℓ−2} ⋯ ⟷^{k+1} π_{k+1} ↚→^{k} π_{k}.

Definition 21 Let π = I^{\underline{∂_{1}}} q_{1}^{\underline{∂_{2}}} q_{2}^{\underline{∂_{3}}} ⋯ ^{\underline{∂_{m}}} q_{m} be a path in a higher dimensional automaton. For 1 ≤ ℓ ≤ m such that ∂_{ℓ} denotes a termination phase, let start(ℓ) denote the unique number k such that

π ⟷^{ℓ−1} π_{ℓ−1} ⟷^{ℓ−2} ⋯ ⟷^{k+1} π_{k+1} ↚→^{k} π_{k}.

Now ST-trace(π) is the sequence obtained from split-trace(π) = σ_{1} ⋯ σ_{k}, by replacing σ_{ℓ} by a^{start(ℓ)} whenever σ_{ℓ} = a^{−}.

8 Bisimulation semantics for HDA

Using the material of Section 7, I now extend the main forms of bisimulation equivalence found in the literature that do not involve a special treatment of hidden or internal actions, to higher dimensional automata. For interleaving bisimulation equivalence this is trivial: it is just the standard notion of bisimulation equivalence on ordinary automata found in the literature [20,1], applied to higher dimensional automata by ignoring their higher dimensional cells. ST-bisimulation equivalence [14] is a branching time respecting equivalence that takes causality into account to the extent that it is expressible by durational actions overlapping in time. History preserving bisimulation equivalence [26,11] is the coarsest equivalence that fully respects branching time, causality and their interplay. Hereditary history preserving bisimulation equivalence [3] is a variant of the latter that strongly respects the internal structure of processes, while still collapsing choices between indistinguishable courses of action (i.e. satisfying the CCS law x + x = x [20]).

By Definition 17, the empty path in a higher dimensional automaton A starts and ends in the initial state of A and hence is denoted I^{A}. I write π → π′ if π is a prefix of a path π′, i.e., if π′ is an extension of π.

Definition 22 Two higher dimensional automata A and B are history preserving bisimulation equivalent if there exists a binary relation R between their paths—a history preserving bisimulation—such that

(1) the empty paths in A and B are related: I^{A}RI^{B},

(2) if πRρ then then ST-trace(π) = ST-trace(ρ),

(3) if πRρ and π ↔^{ℓ} π′ then ∃ρ′ with ρ ↔^{ℓ} ρ′ and π′Rρ′,

(4) if πRρ and ρ ↔^{ℓ} ρ′ then ∃π′ with π ↔^{ℓ} π′ and π′Rρ′,

(5) if πRρ and π → π′ then ∃ρ′ with ρ → ρ′ and π′Rρ′,

(6) if πRρ and ρ → ρ′ then ∃π′ with π → π′ and π′Rρ′,

(7) and if πRρ then end(π) ∈ F^{A} ⇔ end(ρ) ∈ F^{B}.

A and B are hereditary history preserving bisimulation equivalent if there exists a history preserving bisimulation R between their paths that moreover satisfies (8) if πRρ and π′ → π then ∃ρ′ with ρ′ → ρ and π′Rρ′, and

(9) if πRρ and ρ′ → ρ then ∃π′ with π′ → π and π′Rρ′.

ST-bisimulation equivalence between HDA is defined exactly as history preserving bisimulation equivalence, but dropping clauses (3) and (4).

Note that in the presence of clause (2), related paths have the same length. Hence clauses (8) and (9) are equivalent. I listed them both solely to stress the symmetric nature of the definition. It is not hard to see that the notion of ST-bisimulation equivalence would not change upon adding clauses (8) and (9), but because of clauses (3) and (4), this does not apply to history preserving bisimulation equivalence. The clauses (3) and (4) express that the causal relations between action phases in the ST-traces of two related paths are the same, for these relations are determined by the space of all allowed permutations of action phases. It follows from the material in Section 7.5 that in the presence of clauses (3) and (4), clause (2) can be simplified to

if πRρ then split-trace(π) = split-trace(ρ).

This clause can be omitted altogether when writing the names of action phases above the arrows in clauses (5), (6), (8) and (9), as is customary in many accounts of bisimulation relations found in the literature.

8.1 History preserving bisimulation semantics for 1-dimensional automata

The definitions of paths, their observable content, adjacency, homotopy and (hereditary) history preserving bisimulation equivalence can be drastically simplified when dealing with higher dimensional automata of the form A(G) with G an extensional 1-dimensional automaton; the reason being that all higher dimensional information is encoded in their 1-dimensional parts. As it is not necessary to consider paths that travel through the inside of squares, paths may be built from entire transitions rather than transition phases. Below I define the mentioned concepts directly on extensional 1-dimensional automata under the concurrent interpretation.

Definition 23 A path in an extensional automaton (S, T, I, F) is a sequence of pairs (a_{1}, q_{1})(a_{2}, q_{2}) ⋯ (a_{m}, q_{m}), denoted I^{\underline{a_{1}}} q_{1}^{\underline{a_{2}}} q_{2}^{\underline{a_{3}}} ⋯ ^{\underline{a_{m}}} q_{m}, with q_{k} ∈ S and a_{k} ∈ A for 1 ≤ k ≤ m, such that (q_{k−1}, a, q_{k}) ∈ T. Here q_{0} := I, i.e. I consider only paths starting from the initial state. One writes end(π) for q_{m}.

Write trace(π) for the sequence a_{1} ⋯ a_{m}.

Two paths π and π′ are ℓ-adjacent—denoted π ↔^{ℓ} π′—if π = I^{\underline{a_{1}}} ⋯ ^{\underline{a_{m}}} q_{m} with m > ℓ and π′ is obtained from π by replacing, for some q ∈ Q, the segment ^{\underline{a_{ℓ}}} q_{ℓ}^{\underline{a_{ℓ+1}}} by ^{\underline{a_{ℓ+1}}} q^{\underline{a_{ℓ}}}, provided that a_{ℓ} ≠ a_{ℓ+1} or q ≠ q_{ℓ}.

Trace(π) is the observable content of a path π. Again homotopy can be defined as the reflexive and transitive closure of adjacency, obtained by abstracting from ℓ. As before, I write π → π′ if π is a prefix of a path π′.

Definition 24 Two extensional automata G and H are history preserving bisimulation equivalent if there exists a binary relation R between their paths —a history preserving bisimulation—such that

(1) the empty paths in G and H are related,

(2) if πRρ then then trace(π) = trace(ρ),

(3) if πRρ and π ↔^{ℓ} π′ then ∃ρ′ with ρ ↔^{ℓ} ρ′ and π′Rρ′,

(4) if πRρ and ρ ↔^{ℓ} ρ′ then ∃π′ with π ↔^{ℓ} π′ and π′Rρ′,

(5) if πRρ and π → π′ then ∃ρ′ with ρ → ρ′ and π′Rρ′,

(6) if πRρ and ρ → ρ′ then ∃π′ with π → π′ and π′Rρ′,

(7) and if πRρ then end(π) ∈ F^{G} ⇔ end(ρ) ∈ F^{H}.

The equivalence is hereditary if R moreover satisfies

(8) if πRρ and π′ → π then ∃ρ′ with ρ′ → ρ and π′Rρ′.

The next proposition says that this simplified definition for 1-dimensional automata agrees with the general definition for higher dimensional automata.

Proposition 3 Two extensional automata G and H are (hereditary) history preserving bisimulation equivalent in the sense of Definition 24 iff their higher dimensional representations A(G) and A(H) are (hereditary) history preserving bisimulation equivalent in the sense of Definition 22.

Proof. Straightforward, albeit a bit tedious. □

Dropping clauses (3) and (4) in Definition 24 yields a definition of interleaving bisimulation; ST-bisimulation equivalence on extensional automata cannot be defined that way.

8.2 History preserving bisimulation semantics for configuration structures

Any semantic equivalence ∼ on 1- or higher dimensional automata is inherited by rooted finitary configuration structures by letting C ∼ D iff G(C) ∼ G(D). In particular, Definition 24 extends (hereditary) history preserving bisimulation equivalence to arbitrary rooted finitary configuration structures. However, on stable configuration structures (Definition 6) these equivalences were already defined in [11]. Therefore I need to prove that for stable configuration structures the new definition (24) agrees with the one of [11]. As a first step, I reformulate the new definition for rooted finitary configuration structures by eliminating the reference to the embedding G.

Definition 25 A path in a configuration structure C is a sequence of distinct events e_{1}e_{2} ⋯ e_{m} such that ∀k ≤ n. {e_{1}, …, e_{k}} ∈ C^{C}. Write end(π) for {e_{1}, …, e_{m}} and trace(π) for the sequence l^{C}(e_{1}) ⋯ l^{C}(e_{m}). Two paths π and π′ in C are ℓ-adjacent—denoted π ↔^{ℓ} π′—if π = e_{1} ⋯ e_{m} with m > ℓ and π′ is obtained from π by swapping e_{ℓ} and e_{ℓ+1}. Write π → π′ if π is a prefix of π′.

Proposition 4 Let C and D be rooted configuration structures. Then G(C) and G(D) are (hereditary) history preserving bisimulation equivalent iff there exists a relation between the paths of C and D (defined above) such that

(1) the empty paths in C and D are related,

(2) if πRρ then then trace(π) = trace(ρ),

(3) if πRρ and π ↔^{ℓ} π′ then ∃ρ′ with ρ ↔^{ℓ} ρ′ and π′Rρ′,

(4) if πRρ and ρ ↔^{ℓ} ρ′ then ∃π′ with π ↔^{ℓ} π′ and π′Rρ′,

(5) if πRρ and π → π′ then ∃ρ′ with ρ → ρ′ and π′Rρ′,

(6) if πRρ and ρ → ρ′ then ∃π′ with π → π′ and π′Rρ′,

(7) and if πRρ then end(π) ∈ F^{C} ⇔ end(ρ) ∈ F^{D}.

The equivalence is hereditary if R moreover satisfies

(8) if πRρ and π′ → π then ∃ρ′ with ρ′ → ρ and π′Rρ′.

Proof. Trivial. □

Let C be a stable configuration structure, and X ∈ C^{C}. The causality relation on X is given by d ≤_{X} e iff for all Y ∈ C^{C} with Y ⊆ X one has e ∈ Y ⇒ d ∈ Y.

Proposition 5 Let C be a stable configuration structure, and X ∈ C^{C}. Then ≤_{X} is a partial order, and the paths π in C with end(π) = X are exactly the linearisations of ≤_{X}.

Proof. The first statement is Proposition 5.2 in [11]. That paths ending in X are linearisations of ≤_{X} is immediate from the definitions. That each linearisation of ≤_{X} is a path in C is a restatement of Proposition 5.3 in [11].□

Corollary 3 Any two paths π and ρ in a stable configuration structure that satisfy end(π) = end(ρ) are homotopic.

In [11] it is shown that a rooted finitary configuration structure is stable if and only if it satisfies the mentioned Propositions 5.2 and 5.3, hence if and only if it satisfies Proposition 5 above. Thus the stable ones are the largest class of rooted finitary configuration structures on which causality can faithfully be expressed in terms of partial orders.

Using this causality relation, (hereditary) history preserving bisimulation equivalence was defined in [11] on stable configuration structures as follows.

Definition 26 Two stable configuration structures C and D are history preserving bisimulation equivalent if there is a relation R ⊆ C^{C}×C^{D}×P(E^{C}×E^{D}) such that (∅, ∅, ∅) ∈ R and whenever (X, Y, f) ∈ R then

• f is an isomorphism between (X, ≤_{X}, l^{C} ^{\}X) and (Y, ≤_{Y} , l^{D} ^{\}Y),

• X ⊆ X′ ∈ C^{C} ⇒ ∃Y′, f′ with Y ⊆ Y′ ∈ C^{D}, (X′, Y′, f′) ∈ R and f′ ^{\}X=f,

• Y ⊆ Y′ ∈ C^{D} ⇒ ∃X′, f′ with X ⊆ X′ ∈ C^{C}, (X′, Y′, f′) ∈ R and f′ ^{\}X=f,

• X ∈ F^{C} ⇔ Y ∈ F^{D}. The equivalence is hereditary if R moreover satisfies

• (X, Y, f) ∈ R ∧ X ⊇ X′ ∈ C^{C} ⇒ (X′, f(X′), f ^{\}X′) ∈ R.

This definition also applies to various kinds of event structures, through natural embeddings into stable configuration structures [11].

Theorem 5 Two stable configuration structures C and D are (hereditary) history preserving bisimulation equivalent in the sense of Definition 26 iff their automata representations G(C) and G(D) are (hereditary) history preserving bisimulation equivalent in the sense of Definition 24.

Proof. Let R be a relation between the paths of C and D satisfying the properties of Proposition 4. Define the relation R̃ ⊆ C^{C} × C^{D} × P(E^{C} × E^{D}) by (X, Y, f) ∈ R̃ iff there are paths π = e_{1} ⋯ e_{m} in C and ρ = d_{1} ⋯ d_{m} in D with πRρ, X = end(π), Y = end(ρ) and f(e_{k}) = d_{k} for k = 1, ..., m.

I will show that R̃ is a history preserving bisimulation between C and D. Using property (1), one obtains (∅, ∅, ∅) ∈ R̃. Now suppose (X, Y, f) ∈ R̃.

• By construction f is a bijection between X and Y, and by (2) it satisfies l^{D}(f(e)) = l^{C}(e) for e ∈ X. Suppose d ≰_{X} e. By Proposition 5 and Corollary 3 there is a path π′ in C, homotopic with π, in which e precedes d. So by (3) there is a path ρ′ in D, homotopic with ρ, in which f(e) precedes f(d). Hence f(d) ≰_{Y} f(e). Likewise, using (4), one has f(d) ≰_{Y} f(e) ⇒ d ≰_{X} e. It follows that f is an isomorphism between (X, ≤_{X}, l^{C} ^{\}X) and (Y, ≤_{Y} , l^{D} ^{\}Y).

• Suppose X ⊆ X′ ∈ C^{C}. By Lemma 5.2.5 in [11], there is a path π′ in C with π → π′ and end(π′) = X′. Thus, using (5), ∃Y′, f′ with Y ⊆ Y′ ∈ C^{D}, (X′, Y′, f′) ∈ R and f′ ^{\}X=f.

• Likewise, using (6), one finds that Y ⊆ Y′ ∈ C^{D} implies ∃X′, f′ with X ⊆ X′ ∈ C^{C}, (X′, Y′, f′) ∈ R and f′ ^{\}X=f.

• X ∈ F^{C} ⇔ end(π) ∈ F^{C} ⇔ end(ρ) ∈ F^{D} ⇔ Y ∈ F^{D}, using (7). In case R also satisfies property (8), the relation R̃ is hereditary. Namely if X ⊇ X′ ∈ C^{C} then by Lemma 5.2.5 in [11] there are paths π′ and π′′ in C with π′ → π′′, end(π′) = X′ and end(π′′) = X. By Corollary 3 π′′ and π are homotopic. So by (3) there is a path ρ′′ in D, homotopic with ρ, with π′′Rρ′′. Using (8) one obtains (X′, f(X′), f ^{\}X′) ∈ R.

Conversely, let R̃ be a history preserving bisimulation between C and D. Define the binary relation R between the paths of C and D by πRρ iff |π| = |ρ|, say π = e_{1} ⋯ e_{m} and ρ = d_{1} ⋯ d_{m}, and (end(π), end(ρ), f) ∈ R̃ for f the function given by f(e_{k}) = d_{k} for k = 1, ..., m. I will show that R satisfies the properties of Proposition 4.

Property (1) follows because (∅, ∅, ∅) ∈ R̃, and (2) because f is an isomorphism. For (3), suppose π ↔^{ℓ} π′. As π′ is a path in C, by Proposition 5 it must be a linearisation of ≤_{end(π)}. Since f is an isomorphism between (end(π), ≤_{end(π)}, l^{C} ^{\}end(π)) and (end(ρ), ≤_{end(ρ)}, l^{D} ^{\}end(ρ)), the sequence f(π′) := d_{1} ⋯ d_{ℓ−1}d_{ℓ+1}d_{ℓ}d_{ℓ+2} ⋯ d_{m} must be a linearisation of ≤_{end(ρ)}, and hence a path in D. It follows that ρ ↔^{ℓ} f(π′) and π′Rf(π′). Property (4) follows likewise, and (5), (6) and (7) are trivial. In case R̃ is hereditary, also (8) holds trivially. □

9 A hierarchy of concurrency models

After having defined precisely what the arrows in Figure 1 mean, I will now proceed to argue for their soundness and completeness in describing the relative expressiveness of the models of concurrency under investigation.

9.1 Soundness of the inclusions of Figure 1

It is well known that stable event structures with binary conflict [31] are more expressive than flow event structures [5], which are more expressive than bundle event structures [18], which are in turn more expressive than prime event structures with binary conflict [31], cf. Figure 5. However, this holds when comparing the families of configurations they can express; the difference disappears when working up to history preserving bisimulation. This follows immediately from the fact that prime and stable event structures with binary conflict specify the same Scott domains [30,31], and thus also the same [higher dimensional] automata. Alternatively, a direct proof can be found in [16]. In [16] and [22] it has furthermore been shown that, up to history preserving bisimulation, finitary conflict can be expressed in terms of binary conflict. Thus, by the criteria of this paper, the stable event structures of [30] do not rank higher in expressive power than the ones with binary conflict in [31]. Likewise, the general event structures of [30] do not rank higher in expressive power than the ones with binary conflict in [31]. This shows that up to history preserving bisimulation Figure 5 collapses into the bottom of Figure 1.

A Petri net is safe if no reachable marking will every have two tokens in the same place. In [21] the expressive equivalence has been established of the model of safe Petri nets with that of prime event structures with binary conflict. This was done by means of translations between these models that preserve more than history preserving bisimulation equivalence.

Up to history preserving bisimulation equivalence, on safe Petri nets there is no difference between any of the four computational interpretations of Petri nets discussed in Section 6. Moreover, the nets N_{•}, constructed in the proof of Theorem 1, are safe. It follows that under the self-sequential individual token interpretation, as well as under the self-concurrent individual token interpretation, the class of all Petri nets is equally expressive as the class of safe Petri nets (and as the subclass of unique-occurrence nets).

In [12] two forms of 1-unfolding are defined, one for Petri nets under the self-concurrent collective token interpretation, and one for Petri nets under the self-sequential collective token interpretation. Each of them converts any Petri net into a so-called 1-occurrence net, a net in which each transition can fire only once. And each of these 1-unfoldings respects history preserving bisimulation equivalence w.r.t. to the computational interpretation of nets that comes with this 1-unfolding. Trivially, on 1-occurrence nets there is no difference between the self-concurrent and the self-sequential interpretation of nets. It follows that, up to history preserving bisimulation equivalence, Petri nets under the self-sequential collective token interpretation are equally expressive as Petri nets under the self-concurrent collective token interpretation.

A Petri net is pure if it has no self-loops, i.e. there are no places s and transitions t with F (s, t) > 0 and F (t, s) > 0. In [12] we showed that rooted finitary configuration structures are equally expressive as pure Petri nets under the collective token interpretation (or precisely, each of the two collective token interpretations). Taking into account that pureness is preserved by the two 1-unfoldings, this was done by means of translations between rooted finitary configuration structures and pure 1-occurrence nets that preserve more than history preserving bisimulation equivalence.

This concludes the justification of the arrows in Figure 1.

c • a  •b • • • a • c  • b • b c • b • a c a \begin{aligned}E & = & \{a, b, c\} \\ # & = & ∅ \\ ∅ & ⊢ & a \\ ∅ & ⊢ & b \\ a & ⊢ & c \\ b & ⊢ & c \end{aligned}  ac # bc

Fig. 8. A system with disjunctive causality represented as an event structure of [31], a [higher dimensional] automaton in which the dashed lines indicate that all three squares are filled in, and a Petri net. The last picture is the best representation of the same system as a prime event structure [21,31]. It requires the decomposition of the event c, which is causally dependent on the disjunction of a and b, into two events c_{1} and c_{2}, only one of which may happen: c_{1} being causally dependent only on a, and c_{2} on b. This prime event structure is ST-bisimulation equivalent to the original one, but not history preserving bisimulation equivalent.

9.2 Completeness of the inclusions of Figure 1

That the model of synchronisation trees is less expressive than that of safe Petri nets is witnessed by the process a∥b, the parallel composition of two actions a and b. This process can be represented by the safe Petri net P in Figure 2. However, there is no synchronisation tree which is history preserving bisimulation equivalent, or even ST-bisimulation equivalent, to this process.

The models of prime and stable event structures are less expressive than that of (general) event structures of [31]. This is witnessed by the process of Figure 8, which is representable as an event structure of [31], but, up to history preserving bisimulation equivalence, not as a prime event structure.

In [13], a generalisation of Winskel’s event structures called rooted event structures with finite conflict is proposed that (up to history preserving bisimulation equivalence) is equally expressive as Petri nets under the collective token interpretation. Also a subclass of pure rooted event structures with finite conflict is defined that matches the expressive power of rooted finitary configuration structures and pure nets. An example of a pure Petri net and a pure rooted event structure with finite conflict as in [13] that cannot be represented as an event structure of [30,31] appears in Figure 9.

Figure 10 shows a system represented as a Petri net, that cannot be represented as a pure Petri net, or as an automaton under the concurrent interpretation.

9.2.1 Beyond Petri nets The final counterexample witnessing the completeness of the expressiveness hierarchy of Figure 1 concerns the process of Figure 11, that is representable as a higher dimensional automaton, and even as an ordinary automaton under the concurrent interpretation, but not as a Petri net.

•c• • a  •b  • • a • c  • b • c a  • b •c ba \begin{aligned}E & = & \{a, b, c\} \\ c & ⊢ & \{a, b\} \\ ∅ & ⊢ & X & for X ≠ \{a, b\} \end{aligned}  a # # a # c b # b

Fig. 9. A system with resolvable conflict represented as a pure Petri net, a pure rooted event structure with finite conflict as introduced in [13], and a [higher dimensional] automaton. The events a and b are initially in conflict (only one of them may happen), but as soon as c occurs this conflict is resolved. The last picture is the best representation of the same system as a prime event structure. It yields a system with two maximal runs, in one of which c causes just a, and in the other just b. Again it is ST-bisimulation equivalent to the original, but not history preserving bisimulation equivalent. There is no event structure as in [30,31] that is history preserving bisimulation equivalent to the system above.

•• a • b • c •  [figure: a; b; c; b; a; c; c; a; b; c; b; a]

Fig. 10. A 2-out-of-3 semaphore, represented as a Petri net and as a higher dimensional automaton. In the latter, all six squares are supposed to be filled in, but the interior of the cube is not. Up to history preserving bisimulation equivalence this system cannot be represented as an automaton under the concurrent interpretation, because, due to the filled-in squares, the cube shape is unavoidable, and interior of the cube would by default be understood to be filled in. Hence the system can also not be represented as a pure Petri net.

The process displayed in Figure 11 was implemented during my presentation at EXPRESS 2004. Two computer scientists A and B were travelling from one end of the podium to the other. Their task to was perform the actions a resp. b of crossing a line on the podium. Due to strategic placing of obstacles, the only place where this was possible was at a narrow opening between the obstacles that had room for only one of the scientists A and B at a time. This made the actions a and b mutually exclusive, in the sense that they could not occur simultaneously. A third computer scientist, C, was assigned the task c of removing an obstacle that caused the bottleneck to exist. The action c was executed causally independent of a and b. The actions a and b were mutually exclusive only until c occurred, after which they became causally

[figure: a; b; d; c; c; b; c; a; b; b; a; e; c; c; a]

Fig. 11. A process, represented as an ordinary automaton under the concurrent interpretation, that, up to history preserving bisimulation equivalence, cannot be represented as a Petri net.

independent. Finally, a fourth participant was assigned the task of making a statement when a and b had both occurred before the action c started. This statement was going to be d in case A passed the bottleneck before B did, and e in case B passed the bottleneck before A did. Hearing this statement would prevent computer scientist C from carrying out the action c. The resulting process is described by the automaton above, in which all five squares are filled in.

In order to represent the process of Figure 11, up to history preserving bisimulation equivalence, as a Petri net, there must be a single transition representing the action a, regardless of whether it is scheduled before or after b or c. This is because of the concurrency inherent in the example. The same holds for b. However, in a Petri net, firing just these two transitions labelled a and b necessarily leads to a unique state, independent of the order in which a and b occur. This is in contradiction with the fact that the process under consideration has two states reachable by doing only a and b, in which different further actions are possible.

9.3 Comparisons modulo other notions of equivalence

If I compare the models of Figure 1 up to hereditary history preserving bisimulation equivalence the same hierarchy results. This is because all translations used in Section 9.1 even preserve hereditary history preserving bisimulation equivalence. If I compare them merely up to interleaving bisimulation equivalence, all models turn out to be equally expressive. This is because every higher dimensional automaton is trivially interleaving bisimulation equivalent to the 1-dimensional automaton resulting from ignoring its higher dimensional cells, and to the unfolding of that 1-dimensional automaton into a tree.

If I compare the models up to ST-bisimulation equivalence, the model of synchronisation trees is still less expressive than that of event structures, as explained in Section 9.2. I conjecture that all models of Figure 1 other than synchronisation trees are equally expressive, in the sense that any process representable in any of the models can be translated into an ST-bisimulation equivalent prime event structure. For rooted finitary configuration structures this is Theorem 1 in [12]. My conjecture is that this result extends to higher dimensional automata; in other words, that up to ST-bisimulation equivalence the prime event structures have universal expressivity.

References

[1] Baeten, J.C.M. and W.P. Weijland, “Process Algebra,” Cambridge Tracts in Theoretical Computer Science 18, Cambridge University Press, 1990.

[2] Bednarczyk, M., “Categories of asynchronous systems,” Ph.D. thesis, Computer Science, University of Sussex, Brighton (1987).

Available at ftp://ftp.ipipan.gda.pl/marek/phd.ps.gz.

[3] Bednarczyk, M., Hereditary history preserving bisimulation, or what is the power of the future perfect in program logics, Technical report, Polish Academy of Sciences, Gdansk (1991).

Available at ftp://ftp.ipipan.gda.pl/marek/historie.ps.gz.

[4] Best, E., R. Devillers, A. Kiehn and L. Pomello, Concurrent bisimulations in Petri nets, Acta Informatica 28 (1991), pp. 231–264.

[5] Boudol, G., Flow event structures and flow nets, in: I. Guessarian, editor, Semantics of Systems of Concurrent Processes, Proceedings LITP Spring School on Theoretical Computer Science, La Roche Posay, France, LNCS 469 (1990), pp. 62–95.

[6] Engelfriet, J., Branching processes of Petri nets, Acta Informatica 28(6) (1991), pp. 575–591.

[7] Glabbeek, R.J. van, An operational non-interleaved process graph semantics of CCSP (abstract), in: E.-R. Olderog, U. Goltz and R.J. van Glabbeek, editors, Combining Compositionality and Concurrency, Summary of a GMD-Workshop, Königswinter, March 1988, Arbeitspapiere der GMD 320 (1988), pp. 18–19.

[8] Glabbeek, R.J. van, The refinement theorem for ST-bisimulation semantics, in: M. Broy and C.B. Jones, editors, Proceedings IFIP TC2 Working Conference on Programming Concepts and Methods, Sea of Gallilee, Israel (1990), pp. 27–52,

available at http://kilby.stanford.edu/~rvg/pub/STbisimulation.pdf.

[9] Glabbeek, R.J. van, Bisimulations for higher dimensional automata, email

message (July 7, 1991), available at http://theory.stanford.edu/~rvg/hda.

[10] Glabbeek, R.J. van, History preserving process graphs, draft, available at

http://kilby.stanford.edu/~rvg/pub/history.draft.dvi (1996).

[11] Glabbeek, R.J. van and U. Goltz, Refinement of actions and equivalence notions for concurrent systems, Acta Informatica 37 (2001), pp. 229–327, available at

http://boole.stanford.edu/pub/refinement.ps.gz.

[12] Glabbeek, R.J. van and G.D. Plotkin, Configuration structures (extended abstract), in: D. Kozen, editor, Proceedings 10^{th} Annual IEEE Symposium on Logic in Computer Science, LICS’95, San Diego, USA (1995), pp. 199–209,

available at http://boole.stanford.edu/pub/conf.ps.gz.

[13] Glabbeek, R.J. van and G.D. Plotkin, Event structures for resolvable conflict, in: V. Koubek and J. Kratochvil, editors, Proceedings 29^{th} International Symposium on Mathematical Foundations of Computer Science, MFCS 2004, Prague, Czech Republic, LNCS (August 2004),

available at http://boole.stanford.edu/pub/resolv.ps.gz.

[14] Glabbeek, R.J. van and F.W. Vaandrager, Petri net models for algebraic theories of concurrency (extended abstract), in: J.W. de Bakker, A.J. Nijman and P.C. Treleaven, editors, Proceedings PARLE, Parallel Architectures and Languages Europe, Eindhoven, The Netherlands, June 1987, Vol. II: Parallel Languages, LNCS 259 (1987), pp. 224–242, available at

http://kilby.stanford.edu/~rvg/pub/petri.pdf.

[15] Glabbeek, R.J. van and F.W. Vaandrager, The difference between splitting in n and n + 1, Information and Computation 136 (1997), pp. 109–142, available

at http://boole.stanford.edu/pub/split.pdf.

[16] Glabbeek, R.J. van and F.W. Vaandrager, Bundle event structures and CCSP, in: R. Amadio and D. Lugiez, editors, Proceedings CONCUR 2003, 14^{th} International Conference on Concurrency Theory, Marseille, France, September 2003, LNCS 2761 (2003), pp. 57–71, available at

http://boole.stanford.edu/pub/bundle.ps.gz.

[17] Goltz, U. and W. Reisig, The non-sequential behaviour of Petri nets, Information and Computation 57 (1983), pp. 125–147.

[18] Langerak, R., “Transformations and Semantics for LOTOS,” Ph.D. thesis, Department of Computer Science, University of Twente (1992).

[19] Meseguer, J., U. Montanari and V. Sassone, On the semantics of Petri nets, in: W. Cleaveland, editor, Proceedings CONCUR ’92, Second International Conference on Concurrency Theory, Stony Brook, NY, USA, LNCS 630 (1992), pp. 286–301.

[20] Milner, R., “A Calculus of Communicating Systems,” LNCS 92, Springer, 1980.

[21] Nielsen, M., G.D. Plotkin and G. Winskel, Petri nets, event structures and domains, part I, Theoretical Computer Science 13 (1981), pp. 85–108.

[22] Nielsen, M. and G. Winskel, Petri nets and bisimulation, Theoretical Computer Science 153 (1996), pp. 211–244.

[23] Papadimitriou, C., “The Theory of Database Concurrency Control,” Computer Science Press, 1986.

[24] Pratt, V.R., Modeling concurrency with geometry, in: Proc. 18th Ann. ACM Symposium on Principles of Programming Languages (1991), pp. 311–322,

available at http://boole.stanford.edu/pub/cg.ps.gz.

[25] Pratt, V.R., Chu spaces, a summary and large collection of papers available at

http://chu.stanford.edu/ (1993–2002).

[26] Rabinovich, A. and B.A. Trakhtenbrot, Behavior structures and nets, Fundamenta Informaticae 11 (1988), pp. 357–404.

[27] Serre, J., Homology singulière des espaces fibrés. application, Ph.D. thesis, École Normale Supérieure (1951).

[28] Shields, M.W., Concurrent machines, The Computer Journal 28 (1985), pp. 449–465.

[29] Stark, E.W., Concurrent transition systems, Theoretical Computer Science 64 (1989), pp. 221–269.

[30] Winskel, G., Event structures, in: W. Brauer, W. Reisig and G. Rozenberg, editors, Petri Nets: Applications and Relationships to Other Models of Concurrency, Advances in Petri Nets 1986, Part II; Proceedings of an Advanced Course, Bad Honnef, September 1986, LNCS 255 (1987), pp. 325–392.

[31] Winskel, G., An introduction to event structures, in: J.W. de Bakker, W.P. d. Roever and G. Rozenberg, editors, REX School and Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Noordwijkerhout, The Netherlands, May/June 1988, LNCS 354 (1989), pp. 364–397.

[32] Winskel, G. and M. Nielsen, Models for concurrency, in: Handbook of Logic in Computer Science, Oxford University Press, 1995 pp. 1–148.

Bibliography on Higher Dimensional Automata (besides [24] and [9])

[33] Badouel, E. Splitting of actions, higher-dimensional automata, and net synthesis, Rapport de recherche RR-3013, INRIA, France (1996).

Available at http://www.inria.fr/rrrt/rr-3013.html.

[34] Buckland, R., Choice as a first class citizen, in: M. Orgun and E. Ashcroft, editors, Proceedings Intensional Programming I (1996), pp. 249–259.

[35] Buckland, R., M. Johnson and D. Verity, On the specification of higher dimensional automata, Electronic Notes in Theoretical Computer Science 68(1) (2002), pp. 1–11.

[36] Cattani, G.L. and V. Sassone, Higher dimensional transition systems, in: Proceedings LICS ’96, Eleventh Annual IEEE Symposium on Logic in Computer Science, New Brunswick, USA (1996), pp. 55–62.

Available at ftp://ftp.cl.cam.ac.uk/users/glc25/hdts.dvi.gz.

[37] Cridlig, R., Semantic analysis of shared-memory concurrent languages using abstract model-checking, in: Proceedings PEPM 1995, ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, La Jolla, USA, June 1995 (1995), pp. 214–225.

Available at http://portal.acm.org/citation.cfm?doid=215465.215577.

[38] Cridlig, R., Implementing a static analyzer of concurrent programs: Problems and perspectives, in: M. Dam, editor, Selected Papers of Analysis and Verification of Multiple-Agent Languages, 5th LOMAPS Workshop, Stockholm, Sweden, June 1996, LNCS 1192 (1997), pp. 244–259.

[39] Cridlig, R. and E. Goubault, Semantics and analysis of Linda-based languages, in: Proceedings WSA ’93, 3rd International Workshop on Static Analysis, Padova, Italy, September 1993, LNCS 724 (1993), pp. 72–86.

Available at http://www.di.ens.fr/~goubault/papers/Linda.ps.gz.

[40] Fajstrup, L., Loops, ditopology and deadlocks, Mathematical Structures in Computer Science 10(4) (2000), pp. 459–480.

[41] Fajstrup, L., E. Goubault and M. Raussen, Detecting deadlocks in concurrent systems, in: D. Sangiorgi and R. de Simone, editors, Proceedings CONCUR ’98, 9th International Conference on Concurrency Theory, Nice, France, September 1998, LNCS 1466 (1998), pp. 332–347.

Available at http://www.di.ens.fr/~goubault/papers/concur98.ps.gz.

[42] Gaucher, P., From concurrency to algebraic topology, Electronic Notes in Theoretical Computer Science 39(2) (2000).

Available at http://www.pps.jussieu.fr/~gaucher/expose.ps.gz.

[43] Gaucher, P., Homotopy invariants of higher dimensional categories and concurrency in computer science, Mathematical Structures in Computer Science 10(4) (2000), pp. 481–524.

Available at http://www.pps.jussieu.fr/~gaucher/homotopie_cat.ps.gz.

[44] Gaucher, P., Combinatorics of branchings in higher dimensional automata, Theory and Applications of Categories 8(12) (2001), pp. 324–376.

Available at http://www.pps.jussieu.fr/~gaucher/coin.ps.gz.

[45] Gaucher, P., About the globular homology of higher dimensional automata, Cahiers de Topologie et Géométrie Différentielle Catégoriques XLIII(2) (2002),

pp. 107–156. At http://www.pps.jussieu.fr/~gaucher/sglob.ps.gz.

[46] Gaucher, P., Investigating the algebraic structure of dihomotopy types, Electronic Notes in Theoretical Computer Science 52(2) (2002).

Available at http://www.pps.jussieu.fr/~gaucher/dihomotopy.ps.gz.

[47] Gaucher, P., The branching nerve of HDA and the Kan condition, Theory and Applications of Categories 11(3) (2003), pp. 75–106.

Available at http://www.pps.jussieu.fr/~gaucher/fibrantcoin.ps.gz.

[48] Gaucher, P., A model category for the homotopy theory of concurrency, Homology, Homotopy and Applications 5(1) (2003), pp. 549–599.

Available at http://www.pps.jussieu.fr/~gaucher/modelflow.ps.gz.

[49] Gaucher, P., Comparing globular complex and flow, New-York Journal of Mathematics 11 (2005), pp. 97–150.

Available at http://www.pps.jussieu.fr/~gaucher/glcompflow.ps.gz.

[50] Gaucher, P., Homological properties of non-deterministic branchings and mergings in higher dimensional automata, Homology, Homotopy and Applications 7(1) (2005), pp. 51–76.

Available at http://www.pps.jussieu.fr/~gaucher/exbranching.ps.gz.

[51] Gaucher, P., Flow does not model flows up to weak dihomotopy, to appear in Applied Categorical Structures (2005).

Available at http://www.pps.jussieu.fr/~gaucher/nonexistence.ps.gz.

[52] Gaucher, P. and E. Goubault, Topological deformation of higher dimensional automata, Homology, Homotopy and Applications 5(2) (2003), pp. 39–82.

Available at http://www.pps.jussieu.fr/~gaucher/diCW.ps.gz.

[53] Glabbeek, R.J. van, The individual and collective token interpretations of Petri nets, in: M. Abadi and L. de Alfaro, editors, Proceedings CONCUR 2005, 16^{th} International Conference on Concurrency Theory, San Francisco, USA, August 2005, LNCS 3653 (2005), pp. 323–337, available at

http://boole.stanford.edu/pub/individual.ps.gz.

[54] Goubault, E., Domains of higher-dimensional automata, in: E. Best, editor, Proceedings CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 1993, LNCS 715 (1993), pp. 293–307.

Available at http://www.di.ens.fr/~goubault/papers/Domains.ps.gz.

[55] Goubault, E., The geometry of concurrency, Ph.D. thesis, École Normale

Supérieure (1995), http://www.di.ens.fr/~goubault/papers/these.ps.gz.

[56] Goubault, E., Schedulers as abstract interpretations of higher-dimensional automata, in: Proceedings PEPM 1995, ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, La Jolla, USA, June 1995 (1995), pp. 134–145.

Available at http://www.di.ens.fr/~goubault/papers/schedule2.ps.gz.

[57] Goubault, E., Durations for truly-concurrent actions, in: H. R. Nielson, editor, Proceedings Programming Languages and Systems - ESOP’96, 6th European Symposium on Programming, Linköping, Sweden, April 1996, LNCS 1058 (1996), pp. 173–187. Available as Transitions take time at

http://www.di.ens.fr/~goubault/papers/Timed_HDA.ps.gz.

[58] Goubault, E., A semantic view on distributed computability and complexity, in: Proceedings 3rd Theory and Formal Methods Workshop (1996).

Available at http://www.di.ens.fr/~goubault/papers/Imperial.ps.gz.

[59] Goubault, E., Geometry and concurrency: a user’s guide, Mathematical Structures in Computer Science 10(4) (2000), pp. 411–425.

Available at http://www.di.ens.fr/~goubault/papers/introMSCS2.ps.gz

and as A historical note on “Geometry and Concurrency” at

http://www.di.ens.fr/~goubault/index1.html.

[60] Goubault, E., Labelled cubical sets and asynchronous transition systems: an adjunction (2002),

Available at http://www.di.ens.fr/~goubault/papers/cmcim02.ps.gz.

[61] Goubault, E., Some geometric perspectives in concurrency theory, Homology, Homotopy and Applications 5(2) (2003), pp. 95–136.

Available at http://www.di.ens.fr/~goubault/papers/stanford.ps.gz.

[62] Goubault, E. and T.P. Jensen, Homology of higher dimensional automata, in: R. Cleaveland, editor, Proceedings CONCUR ’92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 1992, LNCS 630 (1992), pp. 254–268.

Available at http://www.di.ens.fr/~goubault/papers/Homology.ps.gz.

[63] Goubault, E. and M. Raussen, Dihomotopy as a tool in state space analysis, in: Proceedings LATIN ’02, 5th Latin American Symposium on Theoretical Informatics, Cancun, Mexico, 2002, pp. 16–37.

Available at http://www.di.ens.fr/~goubault/papers/final.ps.gz.

[64] Gunawardena, J., Homotopy and concurrency, Bulletin of the EATCS 54 (1994), pp. 184–193, also in: G. Paun, G. Rozenberg and A. Salomaa, editors, Current trends in Theoretical Computer Science: Entering the 21st Century, World Scientific, 2001.

Available at http://www.jeremy-gunawardena.com/papers/hac.pdf.

[65] Lanzmann, E., Automates d’ordre supérieur, Master’s thesis, Université d’Orsay (1993).

[66] Pratt, V.R., Higher dimensional automata revisited, Mathematical Structures in Computer Science 10(4) (2000), pp. 525–548.

Available at http://boole.stanford.edu/pub/hda.ps.gz.

[67] Pratt, V.R., Transition and cancellation in concurrency and branching time, Mathematical Structures in Computer Science 13(4) (2003), pp. 485–529.

Available at http://boole.stanford.edu/pub/seqconc.ps.gz.

[68] Raussen., M., On the classification of dipaths in geometric models for concurrency, Mathematical Structures in Computer Science 10(4) (2000), pp. 427–457.

[69] Sokolowski, S., A case for po-manifolds: in chase after a good topological model for concurrency, Electronic Notes in Theoretical Computer Science 81 (2003),

at ftp://ftp.ipipan.gda.pl/stefan/reports/73-pomanif.ps.gz.

[70] Takayama, Y., Parallelization of concurrent processes in higher dimensional automata, in: Proceedings RIMS Workshop on Term Rewriting Systems and its Applications, RIMS Kyoto University, 1995.

[71] Takayama, Y., Extraction of concurrent processes from higher dimensional automata, in: H. Kirchner, editor, Proceedings CAAP ’96, 21st International Colloquium on Trees in Algebra and Programming, Linköping, Sweden, April 1996, LNCS 1059 (1996), pp. 72–86.

[72] Takayama, Y., Towards cycle filling as parallelization, in: Proceedings 4th International RIMS Workshop on Concurrency Theory and Applications, RIMS Kyoto University, 1996.