History Preserving Process Graphs

R.J. van Glabbeek^{∗}

Computer Science Department, Stanford University Stanford, CA 94305, USA.

                                        rvg@cs.stanford.edu

In this paper I argue that, contrary to what is widely believed, process graphs, or labeled transition systems, have enough structure to model non-interleaved features of concurrency.^{1} To this end I introduce a class of process graphs obeying the restriction that any state not only uniquely characterizes the future of a concurrent behaviour, but also its concurrent history, and show how any process graph can be unfolded into such a graph. These history preserving process graphs capture branching time, conjunctive (partial order) causality and disjunctive causality, just like Winskel’s event structures, as well as phenomena like resolved conflict that can not be modeled by event structures. They generalize the Scott domains which arise as the duals of general event structures and can be regarded as a step towards a geometric model of concurrency.

1 Modeling concurrency with process graphs

Definition 1.1 A process graph (over an alphabet Act) is a triple (S, T, I) where

• S is a set of states or nodes,

• T ⊆ S × Act × S, the transitions or edges,

• I ∈ S, the initial state or root.

Process graphs are also called automata or state transition diagrams. They model systems that are capable of performing actions from Act. The presence of a transition (p, a, q) indicates that the represented system can evolve from state p to state q by performing the action a. The domain of process graphs (over arbitrary alphabets) will be denoted ^{|}G. The components of a process graph G ∈ ^{|}G are denoted by S_{G}, T_{G} and I_{G} (a convention that also applies to other structures given as tuples). Moreover p ⟶^{a}_{G} q denotes the statement (p, a, q) ∈ T_{G}. If p ⟶^{a}_{G} q then (p, a, q) is said to be an outgoing edge of p with label a. When clear from the context, the index G is omitted.

Two process graphs G and H are isomorphic—notation G ≅ H—iff there is a bijective mapping between their sets of states that preserves T and I. Usually one does not distinguish isomorphic process graphs. This means that one abstracts from the identity of the nodes. In drawings of process graphs states are represented as dots, a transition (p, a, q) is represented by an a-labeled arrow from p to q and the initial state is represented by an incoming arrow (not originating from an other state). Hence these drawings represent process graphs only up to isomorphism.

Process graphs are suited for representing nondeterministic systems while abstracting from their real-time behaviour and stochastic aspects. They are often used in interleaving semantics where parallel composition is modeled as arbitrary interleaving [Mil89, BW90]. In interleaving semantics the systems a ∥ b (performing the actions a and b independently in parallel) and ab+ba (performing either first a and then b or first b and then a) can each be represented by either

∗This work was supported by ONR under grant number N00014-92-J-1974.

1This argument stems, in a weaker form, from [Gla88].

[figure: a; b; b; a; or; a; b; b; a]

which are considered semantically equivalent. As a consequence, information about causal dependence is lost in this model. Now the idea behind the history preserving process graphs is simple: squares represent concurrency and branching represents choice or conflict. Moreover, opposite edges in a square represent the same occurrence of an action. So a ∥ b is represented by the graph on the left and ab + ba is represented by the graph on the right. These graphs are no longer equivalent. It turns out that this simple feature makes process graphs capturing all causal subtleties that are expressible by means of event structures, and more.

Outline In Sections 2 and 3, respectively, I will formalize the interleaving interpretation and concurrent interpretation of process graphs. In both cases I will do so by defining an equivalence relation that preserves the semantically essential structure and abstracts from the inessential structure of process graphs. In the interleaving case this will be tree equivalence, which can be regarded as the finest reasonable equivalence that identifies the two graphs above. In the concurrent case the equivalence will be called history preserving graph equivalence. In every such equivalence class there will, up to isomorphism, be exactly one so-called history preserving process graph, which can be obtained from an arbitrary member of the class by means of unfolding. These play the same rôle as trees do in interleaving semantics.

In order to facilitate the comparison with event oriented models of concurrency I associate, in Section 4, with every process graph a collection of events and a collection of configurations. These notions give rise to a classification of process graphs. A particularly well-behaved class are the configuration preserving ones.

Sections 5–7 illustrate the power of process graphs (in particular those that are both history and configuration preserving) in modeling features of concurrency. These sections focus on the representation of (5) causal independence, (6) branching time, conjunctive and disjunctive causality, and the local nature of causality, and (7) overlap in time. Section 6 also shows that process graphs can model features of concurrency that cannot be modeled with event structures.

In Sections 8–8.5 I establish translations from event oriented models to process graphs, and argue that no relevant information is lost in these translations. Sections 8–8.4 and 8.5 deal with event automata, this being one of the most general event oriented models, and Sections 9–9.1 with event structures, one of the most popular.

Finally, in Sections 10 and 11 I discuss the relations with Scott domains and geometric models of concurrency. The independence of the sections is displayed on the right.

[figure: 1; 2; def. 3.1; 7; 4; 3; 8; 6; 5; 8.4; 8.4; 9; 9.1; 8.5; 10; 11]

2 Tree equivalence

The following notion of tree equivalence formalizes the idea that in interleaving semantics a state characterizes no more than the future behaviour of the represented system from that state onwards.

Definition 2.1 A path π in a process graph G is a sequence of edges of the form p_{0} ⟶^{a_{1}} p_{1} ⟶^{a_{2}} p_{2} ⟶^{a_{3}} ⋯ ⟶^{a_{n}} p_{n}. In this paper all paths are taken to be finite. Such a path is rooted if p_{0} = I_{G}. If π is rooted, write end(π) for the endnode p_{n} of π. In case π is empty, end(π) = I_{G}. G is reachable if there is at least one rooted path ending in any given node; it is a tree if there is exactly one.

Definition 2.2 The unfolding Π(G) of a process graph G into a tree is given by

• S_{Π(G)} is the set of rooted paths in G,

• I_{Π(G)} is the empty rooted path,

• π ⟶^{a}_{Π(G)} π′ iff end(π) ⟶^{a}_{G} end(π′) and π′ is π, extended with the edge (end(π), a, end(π′)).

Two graphs G and H are tree equivalent—notation G =_{Π} H—if their unfoldings are isomorphic.

It is easy to see that the unfolding of any process graph is indeed a tree, and the unfolding of a tree is isomorphic to itself. It follows that up to isomorphism every tree equivalence class of process graphs contains exactly one tree, which can be obtained from an arbitary member of the class by means of unfolding.

How do we know that this unfolding preserves the (interleaving) semantics of process graphs? The argument is (roughly) that any state of the unfolding correponds to a state of the original in such a way that there is a bijective correspondence between the outgoing transitions of these two states. This argument can be formalized by means of the following notion of a folding.

Definition 2.3 Let G, H ∈ ^{|}G. A folding from H into G is a function f : S_{H} → S_{G} such that

• f(I_{H}) = I_{G},

• q ⟶^{a}_{H} q′ ⇒ f(q) ⟶^{a}_{G} f(q′),

• and f(q) ⟶^{a}_{G} p′ ⇒ ∃!q′ : q ⟶^{a}_{H} q′ ∧ f(q′) = p′.

If there is a folding from H into G then H is a partial unfolding of G—notation G ≤_{Π} H.

A folding induces a bijection between the outgoing edges of p and f(p) for any node p in H. If G ≤_{Π} H then G and H have the same behaviour in interleaving semantics, and moreover G is smaller (more folded) than H. Now I can formally state that unfolding preserves interleaving semantics:

Proposition 2.1 G ≤_{Π} Π(G) for any process graph G. Proof: The function end is a folding from Π(G) into G. □

Note that a bijective folding is the same as an isomorphism. Moreover, the identity function on S_{G} is a folding from any graph G into itself. The following proposition says that the process graphs with foldings form a category.

Proposition 2.2 The composition of two foldings is again a folding.

Proof: Let h be a folding from K into H and g a folding from H into G. I check that g ∘ h is a folding from K into G.

• (g ∘ h)(I_{K}) = g(h(I_{K})) = g(I_{H}) = I_{G}.

• Suppose q ⟶^{a}_{K} q′. Then h(q) ⟶^{a}_{H} h(q′) and hence g(h(q)) ⟶^{a}_{G} g(h(q′)).

• Suppose g(h(q)) ⟶^{a}_{G} p′. Then ∃!r′ : h(q) ⟶^{a}_{H} r′ ∧ g(r′) = p′. Moreover, ∃!q′ : q ⟶^{a}_{K} q′ ∧ h(q′) = r′. So I have ∃q′ : q ⟶^{a}_{K} q′ ∧ (g ∘ h)(q′) = p′. However, it remains to be shown that q′ is unique. To this end, assume that q ⟶^{a}_{K} q′′ ∧ (g ∘ h)(q′′) = p′. Let r′′ be h(q′′). Then h(q) ⟶^{a}_{H} r′′ ∧ g(r′′) = p′. As r′ is unique in satisfying this property, r′′ = r′, and I have q ⟶^{a}_{K} q′′ ∧ h(q′′) = r′. As q′ is unique in satisfying that property, q′′ = q′. □

Corollary 2.1 It follows that the relation ≤_{Π} is reflexive and transitive, and hence a preorder. □

I now show that tree equivalence is the equivalence closure of ≤_{Π}.

Lemma 2.1 Let f be a folding from H into G. Then there is a unique folding f̃ from Π(G) into H, such that f ∘ f̃ = end.

Proof: The definition of f̃, satisfying the first two properties of a folding, and the proof of f ∘ f̃ = end proceed with simultaneous induction on the length of paths.

Induction base: Let f̃(I_{Π(G)}) := I_{H}. Now f(f̃(I_{Π(G)}) = f(I_{H}) = I_{G} = end(I_{Π(G)}).

Induction step: Suppose f̃(π) has been defined for certain path π, and π ⟶^{a}_{Π(G)} π′. Then f(f̃(π)) = end(π) ⟶^{a}_{G} end(π′), so there is a unique q′ ∈ S_{H} such that f̃(π) ⟶^{a}_{H} q′ and f(q′) = end(π′). Hence let f̃(π′) := q′. Then f̃(π) ⟶^{a}_{H} f̃(π′) and f(f̃(π′) = end(π′).

As there is no freedom in the above construction, f̃ is unique.

In order to establish the third property of a folding, suppose that f̃(π) ⟶^{a}_{H} p′. In that case end(π) = f(f̃(π)) ⟶^{a}_{G} f(p′). Let π′ be the path π, extended with the edge (end(π), a, f(p′)). Then π ⟶^{a}_{Π(G)} π′, so f̃(π) ⟶^{a}_{H} f̃(π′). As f(f̃(π′)) = end(π′) = f(p′) it must be that f̃(π′) = p′.

Now suppose there is a(nother) path π′′ with π ⟶^{a}_{Π(G)} π′′ and f̃(π′′) = p′. Then end(π′′) = f(p′) and π′′ = π′ by Definition 2.2. □

Lemma 2.2 Every folding from a reachable process graph into a tree is an isomorphism. Proof: Let G be a reachable process graph, T a tree, and f be a folding from G into T. Note that end is an isomorphism from Π(T) to T. By Lemma 2.1 there is a folding f̃ from Π(T) into G, such that f ∘f̃ = end. By the first and third requirements of foldings, any folding into a reachable graph is surjective. As end is injective, f has to be injective as well, and hence is an isomorphism. □

Proposition 2.3 If G ≤_{Π} H then Π(G) ≅ Π(H). Proof: Let G ≤_{Π} H. Then, by two applications of Lemma 2.1, G ≤_{Π} H ≤_{Π} Π(G) ≤_{Π} Π(H). Now Lemma 2.2 gives Π(G) ≅ Π(H). □

Theorem 1 =_{Π} is the smallest equivalence containing ≤_{Π}. Proof: If G =_{Π} H then G ≤_{Π} Π(G) ≅ Π(H) ≥_{Π} H by Proposition 2.1. Hence =_{Π} is contained in the smallest equivalence containing ≤_{Π}. The reverse follows since ≤_{Π}⊆=_{Π}, by Proposition 2.3. □

Digression: Tree equivalence in terms of bisimulations

Tree equivalence preserves the branching structure of processes [Gla94] and in addition denies the idempotence of choice (x+x ≠ x). It can be regarded as the finest reasonable equivalence on ^{|}G that allows the unfolding of cyclic graphs into acyclic ones and identifies the two graphs of Section 1. As tree equivalence refines the classical notion of bisimulation equivalence [Mil89], it is tempting to define it directly on process graphs by adding a requirement to the definition of a bisimulation. Here is a failed attempt:

Definition 2.4 A restrictive tree bisimulation is a relation R ⊆ S_{G} × S_{H} satisfying

• I_{G}RI_{H},

• pRq ∧ p ⟶^{a}_{G} p′ ⇒ ∃!q′ : q ⟶^{a}_{H} q′ ∧ p′Rq′ and

• pRq ∧ q ⟶^{a}_{H} q′ ⇒ ∃!p′ : p ⟶^{a}_{G} p′ ∧ p′Rq′.

Note that the classical bisimulation [Mil89] can be obtained by replacing ∃! (there is a unique ...) by ∃. In the light of Theorem 1 and Definition 2.3, one might expect that two graphs are tree equivalent iff there is a restrictive tree bisimulation between them. However, the graphs G_{1} and G_{3} of Figure 1 are tree equivalent, and nevertheless they are not related by such a bisimulation. Namely, in order to satisfy the properties for the labels a and c, any restrictive tree bisimulation has to relate both the top and the bottom node of G_{3} to the top node of G_{1}. This implies that the b transition to the top node in G_{1} can be mimicked in two ways in G_{3}, violating the uniqueness requirement ∃! in Definition 2.4. Moreover, there are restrictive tree bisimulations between G_{1} and

G_{1}  b c a b  G_{2} b ac b  G_{3} b ac b

Figure 1: “Restrictive tree equivalence” is not transitive

G_{2}, and between G_{2} and G_{3}, as indicated in the figure, so defining tree equivalence in terms of restrictive tree bisimulations would give rise to a nontransitive relation.

A form of bisimulation that does characterize tree equivalence appears in [CDL95].

Definition 2.5 Two process graphs G and H are resource bisimilar—notation G \underline{↔}_{R} H—if there exists a relation R ⊆ S_{G} × S_{H}—called a resource bisimulation—such that I_{G}RI_{H} and whenever two states p and q are related (i.e. pRq) then there is a bijective correspondence C_{pq} between their outgoing transitions, such that corresponding transitions have the same label and the endpoints of corresponding transitions are again related.

Note that every restrictive tree bisimulation is a resourse bisimulation. The reverse does not hold, as there exists a resource bisimulation between G_{1} and G_{3}. If fact, the composition of two recourse bisimulations is again a resource bisimulation, and resource bisimililarity is an equivalence relation. This time the classical notion of bisimulation equivalence [Mil89] can be obtained by weaking the bijectivity of C_{pq} into surjectivity and co-surjectivity.

The notion of a resource bisimulation stems from [CDL95]. There, however, the requirement of the bijection took the shape of the apparantly weaker requirement of two injections in either direction. In this shape the resulting equivalence was shown, for finitely branching processes, to be the kernel of a preorder called resource simulation. By the following proposition both definitions are equivalent.

Proposition 2.4 (Schröder-Bernstein) Let S and T be two sets and R ⊆ S × T. If there are injections f : S → T and g : T → S with f, g^{−1} ⊆ R then there is a bijection b : S → T with b ⊆ R.

S g(T) g(f(S)) g(f(g(T))) g(f(g(f(S))))  ··· ⋂_{n=0}^{∞}(g∘f)^{n}(S) = ⋂_{n=0}^{∞}(g∘f)^{n}(g(T))  T f(S) f(g(T)) f(g(f(S))) f(g(f(g(T))) ···  ⋂_{n=0}^{∞}(f ∘g)^{n}(T) = ⋂_{n=0}^{∞}(f ∘g)^{n}(f(S))

Figure 2: Blending two injections into a bijection

Proof: As indicated in Figure 2, the set S can be partitioned into S−g(T), g(T −f(S)), g∘f(S−g(T)), g∘f ∘g(T −f(S)), … and ⋂_{n=0}^{∞}(g∘f)^{n}(S), and likewise for T. The mapping b, given

by b(x) = \begin{cases}f(x) & if x ∈ (g∘f)^{n}(S−g(T)) for n ∈ IN \\ g^{−1}(x) & otherwise \end{cases} turns out to be a bijection with b ⊆ R. □

The following is a characterization of resource bisimilarity in terms of a relation between the transitions of related process graphs, rather than their states. It is useful as an intermediate step in the proof that resource bisimilarity coincides with tree equivalence.

Definition 2.6 A counting bisimulation between G and H ∈ ^{|}G is a relation R ⊆ T_{G} ×T_{H} satisfying

• pR̃q ∧ p ⟶^{a}_{G} p′ ⇒ ∃!q′ : q ⟶^{a}_{H} q′ ∧ (p, a, p′)R(q, a, q′) and

• pR̃q ∧ q ⟶^{a}_{H} q′ ⇒ ∃!p′ : p ⟶^{a}_{G} p′ ∧ (p, a, p′)R(q, a, q′),

where R̃ ⊆ S_{G} × S_{H} is the smallest relation satisfying I_{G}R̃I_{H} and (p, a, p′)R(q, a, q′) ⇒ p′R̃q′.

Proposition 2.5 Two process graphs are resource bisimilar iff there is a counting bisimulation between them.

Proof: “If”: If R is a counting bisimulation then R̃ is a resource bisimulation.

“Only if”: Let R be a resource bisimulation between two process graphs. For any pair of related nodes (p, q) ∈ R pick a bijective correspondence C_{pq} between the outgoing edges of p and q with the required properties. Now ⋃_{(p,q)∈R} C_{pq} is a counting bisimulation. □

Proposition 2.6 If G ≤_{Π} H then G \underline{↔}_{R} H. Moreover, if G \underline{↔}_{R} H then there is a process graph K with G ≤_{Π} K ≥_{Π} H. Hence \underline{↔}_{R} is the smallest equivalence relation containing ≤_{Π} and therefore coincides with tree equivalence.

Proof: The first statement follows since any folding is a resource bisimulation.

Let R be a counting bisimulation between G and H. Interpret R as a process graph by

S_{R} = R̃; I_{R} = (I_{G}, I_{H}); and (p, q) ⟶^{a}_{R} (p′, q′) iff (p, q) ∈ S_{R} and (p, a, p′)R(q, a, q′).

Now the projection of R to its first component is a folding from R into G, whereas the projection of R to its second component is a folding from R into H. □

3 History preserving graph equivalence

Below, I define the notion of a history as an abstraction of the notion of a rooted path. As in the concurrent interpretation of process grahs squares represent concurrency, in a history it doesn’t matter if a path traverses a square on the left or on the right. Just as trees and unfolding were defined in terms of rooted paths, I will define history preserving process graphs and the history unfolding in terms of histories. This gives rise to a notion of history preserving graph equivalence that preserves the concurrent interpretation of process graphs and still allows the unfolding of cyclic graphs into acyclic ones.

Definition 3.1 Two different paths are adjacent if they ‘differ by a square’, that is if one can be obtained from the other by replacing a segment p ⟶^{a} q ⟶^{b} t by p ⟶^{b} s ⟶^{a} t. Homotopy is the smallest equivalence relation on the paths of a graph containing adjacency. Now a history h of a node p in a process graph G is an equivalence class of homotopic paths from the root of G to p; write end(h) = p. G is history preserving if every node has exactly one history.

Definition 3.2 The history unfolding H(G) of a process graph G is given by

• S_{H(G)} is the set of histories of states of G,

• I_{H(G)} is the history consisting of the empty rooted path,

• h ⟶^{a}_{H(G)} h′ iff a path in h can be prolonged with an a-labeled edge to a path in h′.

Two graphs G and H are history preserving graph equivalent—notation G =_{H} H—if H(G) ≅ H(H).

Note that if h ⟶^{a}_{H(G)} h′ then end(h) ⟶^{a}_{G} end(h′) and any path in h can be prolonged with the edge (end(h), a, end(h′)) to a path in h′. Figure 3 shows an example of a history unfolding.

a  b  a  ba  ba  b a a  b  ba a  b  ba  b

Figure 3: A process graph and its history unfolding

Proposition 3.1 For H a history preserving process graph, H(H) ≅ H.

Proof: Let H be a history preserving process graph. For any node p in H, let h(p) be the unique history of p. Then h is a bijective folding from H into H(H), and hence an isomorphism. □

Note that h in this proof is the inverse of end, which is therefore an isomorphism from H(H) to H.

For any path π of length n in a process graph, let π_{i} be the initial segment of π consisting of the first i transitions (i = 0, ..., n), and let [π] denote the unique history containing π.

Proposition 3.2 The history unfolding of any process graph is history preserving.

Proof: Let G ∈ ^{|}G. For any path π in G of the form I_{G} = p_{0} ⟶^{a_{1}} p_{1} ⟶^{a_{2}} p_{2} ⟶^{a_{3}} ⋯ ⟶^{a_{n}} p_{n}, let [[π]] be the path [π_{0}] ⟶^{a_{1}} ⋯ ⟶^{a_{n}} [π_{n}] in H(G). If ρ is adjacent with π, there must be a 0 < k < n such that π_{i} = ρ_{i} for 0 ≤ i < k, (a_{k} ≠ a_{k+1} or end(π_{k}) ≠ end(ρ_{k})) and π_{i} is adjacent with ρ_{i} for

k < i ≤ n. In that case [π_{k−1}] ⟶^{a_{k}} [π_{k}] ⟶^{a_{k+1}} [π_{k+1}], [π_{k−1}] ⟶^{a_{k+1}} [ρ_{k}] ⟶^{a_{k}} [π_{k+1}], [π_{k}] ≠ [ρ_{k}], and

[π_{i}] = [ρ_{i}] for i = 0, ..., k − 1, k + 1, ..., n, so [[π]] and [[ρ]] are adjacent. By transitivity it follows that

if π and ρ are homotopic paths in G, then [[π]] and [[ρ]] are homotopic paths in H(G).

Note that [[·]] is a folding from Π(G) into Π(H(G)), which must be an isomorphism by Lemma 2.2. Now suppose π′ and ρ′ are two paths in H(G) ending in the same state. Let π and ρ be paths in G such that π′ = [[π]] and ρ′ = [[ρ]]. Then [π] = end(π′) = end(ρ′) = [ρ], i.e. π and ρ are homotopic. By the above it follows that also π′ are ρ′ are homotopic, which had to be establised. □

It follows that up to isomorphism every history preserving graph equivalence class contains exactly one history preserving process graph, which can be obtained as the history unfolding of any member of the class.

When two states are related by a folding between two process graphs, this folding induces a bijection between the outgoing transitions of these states. Under the concurrent interpretation of process graphs it is important whether two (or more) transitions leaving a state represent concurrent actions or conflicting ones. This is modeled geometrically: if these transition span a consistently labeled square (or [hyper]cube) they are concurrent; otherwise they are in conflict. A folding is said to be history preserving if this structure is preserved.

Definition 3.3 A folding f from H into G is history preserving if it satisfies

f(q) ⟶^{a}_{G} p_{1} ⟶^{b}_{G} p_{3} ∧ f(q) ⟶^{b}_{G} p_{2} ⟶^{a}_{G} p_{3} ⇒

∃q_{1}, q_{2}, q_{3} ∈ S_{H} : q ⟶^{a}_{H} q_{1} ⟶^{b}_{H} q_{3} ∧ q ⟶^{b}_{H} q_{2} ⟶^{a}_{H} q_{3} ∧ f(q_{i}) = p_{i} (i = 1, 2, 3).

Write G ≤_{H} H if such a folding exists.

In this definition a square in the folded process is required to exist also in the original. It is not difficult to see that a similar requirement for (hyper)cubes is derivable (thanks to the unicity requirement in the third clause of Definition 2.3). That squares or (hyper)cubes in the original can also be found in the folded process follows already from the second clause of Definition 2.3.

Suppose one writes, for L a multiset of actions, p ⟶^{L}_{G} q if the represented system can evolve from state p to state q by concurrently performing the actions in L. I will not give the definition in general, but in the typical case that L = a + a + b it amounts to:

p ⟶^{a+a+b}_{G} q iff there are p_{ijk} ∈ S_{G} for i, j, k ∈ {0, 1}, such that p = p_{000}, q = p_{111},

p_{0jk} ⟶^{a} p_{1jk} for j, k ∈ {0, 1}, p_{i0k} ⟶^{a} p_{i1k} for i, k ∈ {0, 1} and p_{ij0} ⟶^{b} p_{ij1} for i, j ∈ {0, 1}.

Then, for any folding f one has

p ⟶^{L}_{H} p′ ⇒ f(p) ⟶^{L}_{G} f(p′),

and for a history preserving folding f also

f(p) ⟶^{L}_{G} q′ ⇒ ∃!p′ : p ⟶^{L}_{H} p′ ∧ f(p′) = q′.

Proposition 3.3 ≤_{H} is a preorder. Proof: The identity folding from a graph into itself is history preserving, and the composition of two history preserving foldings is also history preserving. □

The following proposition states that the history unfolding preserves the concurrent interpretation of process graphs. Employing similar techniques as in the previous section, I then show that =_{H} is the equivalence closure of ≤_{H}.

Proposition 3.4 G ≤_{H} H(G) for any process graph G. Proof: The function end is a history preserving folding from H(G) into G. □

Lemma 3.1 Let f be a history preserving folding from H into G. Then there is a history preserving folding f̄ from H(G) into H, such that f ∘ f̄ = end.

Proof: According to Lemma 2.1 there is a unique folding f̃from Π(G) into H, such that f ∘f̃ = end. Let π be a path I_{G} ⟶^{a_{1}}_{G} p_{1} ⟶^{a_{2}}_{G} p_{2} ⟶^{a_{3}}_{G} ⋯ ⟶^{a_{n}}_{G} p_{n}, let ρ be adjacent with π, and let k < n be the first index for which π_{k} ≠ ρ_{k}. With induction on i, I show that f̃(π_{i}) = f̃(ρ_{i}) for k + 1 ≤ i ≤ n.

Induction base: As f(f̃(π_{k−1})) = p_{k−1} ⟶^{a_{k+1}}_{G} end(ρ_{k}) ⟶^{a_{k}}_{G} p_{k+1} and f is history preserving, there must be q_{k}, r_{k} and q_{k+1} ∈ S_{H} such that f(q_{k}) = p_{k}, f(r_{k}) = end(ρ_{k}), f(q_{k+1}) = p_{k+1} and

f̃(π_{k−1}) ⟶^{a_{k}}_{H} q_{k} ⟶^{a_{k+1}}_{H} q_{k+1} ∧ f̃(π_{k−1}) ⟶^{a_{k+1}}_{H} r_{k} ⟶^{a_{k}}_{H} q_{k+1}.

As f is a folding, q_{k} is the only node in H with f̃(π_{k−1}) ⟶^{a_{k}}_{H} q_{k} and f(q_{k}) = p_{k}, thus q_{k} = f̃(π_{k}). Likewise, r_{k} = f̃(ρ_{k}) and q_{k+1} = f̃(π_{k+1}) = f̃(ρ_{k+1}).

Induction step: Suppose f̃(π_{i−1}) = f̃(ρ_{i−1}). As f(f̃(π_{i−1})) = p_{i−1} ⟶^{a_{i}}_{G} p_{i} and f is a folding, there is exactly one node q_{i} in H with f̃(π_{i−1}) ⟶^{a_{i}}_{H} q_{i} and f(q_{i}) = p_{i}. Hence f̃(π_{i}) = f̃(ρ_{i}).

So in particular f̃(π) = f̃(ρ). By transitivity it follows that

if π and ρ are homotopic paths in G, then f̃(π) = f̃(ρ).

Therefore I may define f̄ by f̄([π]) = f̃(π). This is clearly a folding satisfying f ∘ f̄ = end. In order to check that f̄ is history preserving, suppose that

f̄([π]) ⟶^{a}_{H} p_{1} ⟶^{b}_{H} p_{3} ∧ f̄([π]) ⟶^{b}_{H} p_{2} ⟶^{a}_{H} p_{4} = p_{3}.

As f̃ is a folding, there are (unique) paths π_{i} in G (i=1–4), such that f̃(π_{i}) = p_{i} and

π ⟶^{a}_{Π(G)} π_{1} ⟶^{b}_{Π(G)} π_{3} ∧ π ⟶^{b}_{Π(G)} π_{2} ⟶^{a}_{Π(G)} π_{4}.

As end(π_{3}) = f(p_{3}) = f(p_{4}) = end(π_{4}), the paths π_{3} and π_{4} are adjacent or equal, so [π_{3}] = [π_{4}]. This yields the desired result [π] ⟶^{a}_{H(G)} [π_{1}] ⟶^{b}_{H(G)} [π_{3}] ∧ [π] ⟶^{b}_{H(G)} [π_{2}] ⟶^{a}_{H(G)} [π_{3}]. □

Now the remaining results are proved exactly as in the previous section.

Lemma 3.2 Every folding from a reachable into a history preserving process graph is an isomorphism.

Proposition 3.5 If G ≤_{H} H then H(G) ≅ H(H).

Theorem 2 =_{H} is the smallest equivalence containing ≤_{H}.

It is nontrivial to characterize =_{H} in terms of bisimulations (the straightforward history preserving adaptation of a counting bisimulation for instance would gave rise to a nontransitive relation). Probably such a characterization would convey less insight in the nature of history preserving graph equivalence than does its charcterization in terms of history preserving foldings.

4 Events and configurations

In order to connect process graphs with event oriented models of concurrency I formalize the postulate that opposite edges in a consistently labeled square represent the same action occurrence.

Definition 4.1 Let G ∈ ^{|}G. Then ∼ is the smallest equivalence relation on T_{G} satisfying

p ⟶^{a} q ⟶^{b} s, p ⟶^{b} r ⟶^{a} s, (a ≠ b ∨ q ≠ r) ⇒ (p, a, q) ∼ (r, a, s).

If u ∼ v then the edges u and v are said to represent the same event. The equivalence classes are called events of G. Let E_{G} be the set of events of G. [p, a, q] denotes the event containing (p, a, q).

In a history preserving process graph an event denotes an occurrence of an action in a possible run of the represented system. It thus represents a level of abstraction between actions and transitions. The graph on the right for instance has 4 transitions, grouped together into 2 events, in turn grouped together into 1 action. Events can be thought of as the basic building blocks of the represented system. An action then represents an equivalence class of events that are indistinguishable on the cho-

[figure: a; a; a; a]

sen level of abstraction at which the system is represented. A transition on the other hand represents an event as it can be totally ordered in time w.r.t. other events occurring in the same run. As in reality it may be meaningless to order independent events in time (they could happen lightyears apart in space and happen more or less simultaneously), transitions are not so fundamental as events; they are merely a convenience in the representation of a system as a process graph.

In process graphs that are not history preserving an event also represents a level of abstraction between actions and transitions, but somewhat more abstract, like the events in condition/event systems (Petri nets). In the leftmost process graph of Figure 3 for instance, the only event labeled a can happen many times in one run of the represented system. It takes a history unfolding to split up a single event into subevents that can be regarded as true action occurrences.

Proposition 4.1 Let f be a folding from process graph H into G. Then there exists a mapping f^{∗} : E_{H} → E_{G} satisfying f^{∗}([p, a, q]) = [f(p), a, f(q)]. If G is reachable then f^{∗} is surjective. Proof: If (p, a, q) ∼ (r, a, s) then (f(p), a, f(q)) ∼ (f(r), a, f(s)). □

As an edge determines an event, a rooted path in a process graph determines a sequence of events that can be performed by the represented system. Since some of the events in such a sequence may be causally independent, and the order of these events is semantically irrelevant, it makes sense to consider the multiset representation of such a sequence. This I will call a configuration.

Definition 4.2 A configuration of a node p in a process graph G is a multiset Σ_{i=1}^{n}[p_{i−1}, a_{i}, p_{i}] determined by a rooted path (p_{0}, a_{1}, p_{1})(p_{1}, a_{2}, p_{2})(p_{2}, a_{3}, p_{3}) ⋯ (p_{n−1}, a_{n}, p) ending in p. G is

• nonrepetitive iff all configurations are plain sets;

• event-deterministic if (p, a, q) ∼ (p, a, r) ⇒ q = r for every reachable state p;

• configuration-deterministic if no two different nodes share the same configuration;

• configuration-unique if every node has exactly one configuration;

• and configuration preserving if it is both configuration-deterministic and configuration-unique.

Let C_{G} be the set of configurations of nodes of G. The unique configuration of a node p in a configuration-unique graph is denoted C(p).

A process graph is nonrepetitive iff its reachable part is acyclic and has no rooted paths containing two edges representing the same event. A graph is configuration preserving iff

• each node is reachable from the root by at least one path

• and two rooted paths end in the same node iff they determine the same configuration.

In a configuration preserving process graph a state p uniquely determines, and is uniquely determined by, the (multi)set of events that occur before the represented system reaches that state.

If two rooted paths are homotopic they surely determine the same configuration. Hence a configuration is a more abstract version of a history. It follows that any history preserving process graph is configuration-unique. In many process graphs two rooted paths determine the same configuration iff they are homotopic. This is not the case however in the two graphs of Figure 5, which are both configuration-unique. In the first one the two rooted paths ending in p determine the same configuration but are not homotopic; in the second the same holds for the two rooted paths ending in q and r. The first graph is configuration preserving, but not history preserving. The second one, which is the history unfolding of the first, is history preserving as well as event-deterministic, but not configuration-deterministic.

Proposition 4.2 Configuration preserving process graphs are nonrepetitive.

Proof: Suppose (p, a, q) and (p′, a, q′) are the first two different edge-occurrences (possibly different occurrences of the same edge) in a rooted path in a configuration preserving process graph G that represent the same event e. Then e ∈ C(q) ⊆ C(p′) but e ∉ C(p). It follows that p ≠ p′ and hence G is acyclic. As (p, a, q) ∼ (p′, a, q′) there must be a sequence of edges (p_{i}, a, q_{i}) (i = 0, ..., n) and

labels c_{i} (i < n) with p = p_{0}, q = q_{0}, p′ = p_{n} and q′ = q_{n}, such that either p_{i} ⟶^{c_{i}} p_{i+1} ∧ q_{i} ⟶^{c_{i}} q_{i+1}

or q_{i+1} ⟶^{c_{i}} q_{i} ∧ p_{i+1} ⟶^{c_{i}} p_{i} with a ≠ c_{i} ∨ q_{i} ≠ p_{i+1} for i < n. Thus there is an index i < n with

e ∈ C(p_{i+1}) but e ∉ C(p_{i}). Therefore the edge (p_{i}, c_{i}, p_{i+1}) is representing e, and c_{i} = a. However, (p_{i}, a, q_{i}) also represents e and q_{i} ≠ p_{i+1}. As p_{i} is reachable from the root one finds two different rooted paths that determine the same configuration C(p_{i}) ∪ {e}, contradicting the assumptions. □

From the proof it even follows that if a graph is event-deterministic and configuration-unique, it is nonrepetitive. Moreover, any event-deterministic process graph is also configuration-deterministic. Hence the various classes of process graphs are ordered by inclusion as indicated in Figure 4.

config. preserving all process graphs config.- unique history preserving configuration-deterministic event-deterministic non-repetitive H C  H H

Figure 4: Several classes of process graphs

c a  a b c  b p  d  dc d a dc a d bdc b  c a  a b c q  b r  d  dc d a dc a d b d d c  b

Figure 5: The history unfolding can introduce configuration-nondeterminism

Proposition 4.3 The nonrepetitive as well as the event-deterministic process graphs are closed under history unfolding.

Proof: Let G ∈ ^{|}G. As there is a folding from H(G) into G, any cycle in H(G) can be mapped to a cycle in the reachable part of G. Moreover, if H(G) has a rooted path containing two edges representing the same event, then, by Proposition 4.1, so does G. Thus, if G is nonrepetitive then so is H(G). Likewise, if H(G) has a reachable state with two outgoing transitions representing the same event, then, by Proposition 4.1 and the unicity requirement in Definition 2.3, so does G. □

However, the configuration-deterministic process graphs are not closed under history unfolding, as illustrated in Figure 5. Therefore, I introduce another unfolding that allows me to show that any configuration-deterministic process graph is history preserving graph equivalent to a nonrepetitive configuration-deterministic process graph.

Definition 4.3 The configuration unfolding C(G) of a process graph G is given by

• S_{C(G)} is the set of pairs (X, p) with p ∈ S_{G} and X a configuration of p,

• I_{C(G)} = (∅, I_{G}),

• (X, p) ⟶^{a}_{C(G)} (X′, p′) iff p ⟶^{a}_{G} p′ ∧ X′ = X ∪ {[p, a, p′]}.

Proposition 4.4 There is a history preserving folding from C(G) into G. Proof: The projection to the second component constitutes such a folding. □

Proposition 4.5 The configuration-deterministic process graphs are closed under this unfolding.

Proof: Suppose G is configuration-deterministic and C(G) has two nodes (Y, q) and (Z, r) which share the same configuration. By applying the folding of Proposition 4.4 to the responsible paths in C(G) one finds paths in G to q and r that by Proposition 4.1 determine the same configuration. Hence q = r. Moreover, by Definition 4.3, this configuration must be Y as well as Z. □

Proposition 4.6 Process graphs of the form C(G) with G event-deterministic are nonrepetitive.

Proof: Let G be an event-deterministic process graph. Let ((X, p), a,(Y, q)) and ((X′, p′), a,(Y′, q′)) be the first two different edge-occurrences (possibly different occurrences of the same edge) in a rooted path in C(G) that represent the same event. As ((X, p), a, (Y, q)) ∼ ((X′, p′), a, (Y′, q′)) there must be a sequence of edges ((X_{i}, p_{i}), a, (Y_{i}, q_{i})) (i = 0, ..., n) and labels c_{i} (i < n) with (X, p) = (X_{0}, p_{0}), (Y, q) = (Y_{0}, q_{0}), (X′, p′) = (X_{n}, p_{n}) and (Y′, q′) = (Y_{n}, q_{n}), such that either

(X_{i}, p_{i}) ⟶^{c_{i}} (X_{i+1}, p_{i+1}) ∧ (Y_{i}, q_{i}) ⟶^{c_{i}} (Y_{i+1}, q_{i+1}) or (Y_{i+1}, q_{i+1}) ⟶^{c_{i}} (Y_{i}, q_{i}) ∧ (X_{i+1}, p_{i+1}) ⟶^{c_{i}} (X_{i}, p_{i})

with a ≠ c_{i} ∨ Y_{i} ≠ X_{i+1} ∨ q_{i} ≠ p_{i+1} for i < n. It follows that Y′ − X′ = Y − X =^{def} {e}. As Y ⊆ X′,

X′ contains more occurrences of e than X. So X ≠ X′ and hence C(G) is acyclic. Moreover, there is an index i < n such that X_{i+1} contains more occurrences of e than X_{i}. Therefore the edge (p_{i}, c_{i}, p_{i+1}) is representing e, which implies c_{i} = a and X_{i+1} = Y_{i}. However, (p_{i}, a, q_{i}) also represents e and q_{i} ≠ p_{i+1}, contradicting the assumptions. □

Thus, if G is configuration-deterministic, then C(G) is a nonrepetitive and configuration-deter-ministic process graph equivalent to G. Although the counterexamples are too complex to display here, it need not be the case that C(G) is configuration preserving, nor that C(C(G)) ≅ C(G).

5 Local states

In the process ab∥cd, displayed in Figure 6 as a Petri net, a prime event structure and a process graph, the actions a and b are independent of c and d. It could be that the component ab is executed on earth, while cd takes place on the moon, without any communication between them. This independence is very well represented by the Petri net, which consists of two disconnected

ab cc a process graph with local state c b d d a d b  ab c a local execution b d ab ab cd prime event structure • a p b  • Petri net cd

Figure 6: Three representations of ab∥cd, and a local execution

parts. The same holds for the event structure, but not for the graph representation. It appears as though the process graph tries to specify all possible execution sequences of the system, each of which is given by a total order in which the events are executed. In reality, however, the order in which the events happen may be undetermined or irrelevant. This is especially the case if the time taken by the components ab and cd individually is small compared with the time it takes light to travel between earth and the moon. But also if relativistic effects play no rôle it appears to be silly to specify ab∥cd in terms of the possible interleavings of ab and cd, as these give less insight in the architecture of the system than the simple statement that ab and cd are independent. For this reason process graphs are generally deemed inadequate to represent ‘true’ concurrency.

Here I argue that this verdict is only adequate for a particular ‘reading’ of process graphs, the ‘standard reading’ in fact. Instead I suggest another reading in which process graphs display causal independence rather well. Under this reading, a process graph should not be seen as a collection of rooted paths, glued together in various places. A better way of viewing the process graph of ab∥cd is as a two-dimensional structure obtained as the product of ab and cd. The following serves to partly formalize this viewpoint for the class of configuration preserving process graphs.

Besides global states, represented by configurations, one can define a notion of local state: a state as it appears to an observer that is local to only part of the represented system. In the case of ab∥cd, one can imagine an observer on earth registering a state in which a has happened and b has not, while the precise status of the component cd is of no concern and moreover too difficult to ascertain. This local state corresponds to the place p in the Petri net representation of ab∥cd. In a process graph it can be represented as the subgraph encircled in Figure 6.

Definition 5.1 Let G be a configuration preserving process graph. A local state in G is a nonempty set of states of the form {p ∈ S_{G} | C ⊆ C(p) ⊆ C ∪ I} for certain disjoint sets of events C and I. Write L ⟶^{a} L′ with L and L′ local states involving the same set I of independent events if there is a bijection b from L to L′ such that p ⟶^{a} b(p) for p ∈ L and p ⟶^{c} q ⇔ b(p) ⟶^{c} b(q) for p, q ∈ L.

C contains the events that are certainly executed, and C ∪ I the ones that are possibly executed. Thus I are the ones one doesn’t know or care about. A local state with I = ∅ has only one element, and can be regarded as a global state. L ⟶^{a} L′ can be thought of as a local transition between two local states at the same location. This gives rise to (fragments of) local executions, such as the one displayed in Figure 6. It states that it is possible in ab∥cd to perform a c followed by a d, while being independent of ab.

The idea of local states and transitions could perhaps—with appropriate modifications—be used in the analysis of concurrent systems. Here, however, I introduce it only to illustrate how configuration preserving process graphs can be interpreted as displaying true concurrency.

6 Modeling causality and conflict with process graphs

Branching time In a model where systems are represented by their sets of possible execution sequences, one may encounter a system representation such as {ab, ac}, which gives no information on the branching point of these executions. It can be that the choice between ab and ac is made after execution of a, but it is also possible that it is made in the initial state of the system. In the latter case if after doing a it turns out that action b is blocked by the environment it may be too late to choose for c. One says that sets of execution sequences constitute a linear time model of concurrency. It is very well known that process graphs constitute a branching time model of concurrency. This means that from the system representation one can see where a particular choice between conflicting runs is made.

Conjunctive causality In partial order models of concurrency, such as the model of stable event structures [Win87], a particular kind of causal dependence between events in system representations is modeled, namely the kind that can be fully described in terms of partial orders. This kind I call conjunctive causality. A state is typically modeled by the set of events that happened before the represented system reached that state (a configuration), and with every configuration X of a system, a partial order <_{X} is associated^{2}, where d <_{X} e means that in any run of the system in which (some of) the events in X are executed e happens only after d. If there is no causal link between two events, they are independent. In that case these events can happen in either order, but it is also possible that they happen simultaneously, or with a partial overlap, or that the order in which they happen is undetermined.

2In some partial order models, such as the model of prime event structures [Win87], there is a global partial order in the sense that <_{X} is independent of X.

This kind of causality can be faithfully modeled by configuration preserving process graphs. A configuration X of a system corresponds with exactly one node in its graph representation, and any rooted path leading to this node contains exactly one edge for each of the events in X. Now d <_{X} e iff in any rooted path leading to X the representative of d occurs before the representative of e, and two events are independent in X iff there are rooted paths to X containing representatives of both in either order.

In order to see how process graphs capture the interplay of branching time and conjunctive causality, consider the process graph H depicted in Figure 7. Like J and K, this graph is both history and configuration preserving. By Definition 4.1, H has five events, two of which are labeled b. Call the event which is the equivalence class of three b-labeled edges b_{1}, and the one which is the equivalence class of two edges b_{2}. The event which arises as the equivalence class of the three a-edges can be safely called a, and likewise for c and d. The events b_{1} and b_{2} are in conflict, in the sense that they cannot happen in the same run. In fact, the represented system has two maximal runs; one involving the events a, c, d and b_{1}, the other involving a, c, d and b_{2}. The causal relationships between the events in these runs is as indicated by the two partial orders p_{1} and p_{2}. There is a choice between a b-action that is causally dependent on c, and one that is not. One can see that this choice is made at the last possible moment; it is left open by execution of a, c and d.

H: a b  c c  a c  b  d d  a d b conjunctive causality and branching time b  b d  J: ab c b c ba c a disjunctive causality  K: a c c ab  b c ba resolved conflict a b_{1} cd p_{1}  a b_{2} cd p_{2}  • a  c  •b•  •c• a •  b•

Figure 7: Illustrating the expressive power of history preserving process graphs

Disjunctive causality In H, the events a and c are both prerequisites for the event b_{2}. Thus b_{2} is enabled by a conjunction of other events. This is the case in all systems where causality can be described in terms of partial orders, and therefore I call this type of causality conjunctive. In general event structures [Win87] an event is enabled by a disjunction of conjunctions of other events. This type of causality I call disjunctive. The process graph J displays a system that can be modeled as an event structure, but not as a prime or stable one. The event c is caused by the disjunction of a and b. This behaviour can not be expressed in terms of partial orders. As shown, it can be expressed by process graphs however.

Resolved conflict In the initial state of K the events a and b can both happen, but not independently. For if they could happen independently one would expect a configuration {a, b}. Therefore, one might say that they are in conflict. That, however, pertains only to the initial state of K; as soon as c has happened the events a and b become independent. This phenomena could therefore be described as a resolved conflict or postponed concurrency. In event structures [Win87] the conflict relation is static, and conflicts cannot be resolved. Hence, together with the forthcoming Theorem 7—saying that any event structure can be translated, in a behaviour preserving way, to a history and configuration preserving process graph—, K shows that such graphs are in some sense more expressive than event structures. They do not exceed the expressive power of Petri nets however. For the benefit of those familiar with nets I also show the net representation of J and K. In [GP95] the connection with Petri nets is investigated formally.

Local causality through hypercubes In event structures and many other models of concurrency, causality has to some degree a global structure. In configuration preserving process graphs on the other hand, one can express causal relationships between sets of events that differ from state to state. The events a and b in process graph K for instance are independent in the state with configuration {c}, but not in the initial state. In general a set U of n events can happen independently of each other in a state p_{0} if they span an n-dimensional hypercube, i.e. if for any sequence e_{1}, ..., e_{n}

such that U = {e_{1}, ..., e_{n}} there is a path p_{0} ⟶^{a_{1}} p_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{n}} p_{n} with C(p_{i}) = C(p) ._{∪} {e_{1}, ..., e_{i}}

for i = 0, ..., n. This generalizes smoothly to X being a local state in the sense of Definition 5.1.

7 Traveling through the inside of a square

Modeling 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 on the right for instance passes through a point in which 50% of a and about 20% of b has happened.

b a a b

Hence a rooted path is no more than a very special kind of execution, in which never two actions happen simultaneously. When one doesn’t want to distinguish between executions that only differ in the relative timing of progress in ongoing actions, it makes sense to identify two executions if one can be obtained from the other by means of a continuous transformation in the (hyper)space in which the underlying process graph has been layed out. This gives rise to exactly the concept of homotopy of Definition 3.1.

In [GV95] it is established that durational and structural aspects of actions can in general not be modeled in interleaving semantics, even when a time-consuming action is represented by a pair of instantaneous events denoting its start and finish. The main argument consists of an example showing that it makes a difference whether actions are split in 2 or in 3 parts. This example is explained easiest, and was in fact found, in the shape of a process graph (rather than for instance a Petri net or event structure). Here the notion of executions going through the inside of a square is extremely helpful.

8 Event automata

I claim that process graphs capture the behaviour of concurrent systems at least as well as event oriented models. In order to substantiate this claim I have to present behaviour preserving translations between a suitable class of process graphs and an event oriented model. For the last one I take labeled rooted event automata [PP95], because they have a very simple definition and generalize most other event oriented models. I will apply the findings to event structures [Win87] in Section 9.1.

Definition 8.1 A (labeled) event automaton (over an alphabet Act) is a tuple (E, C, ↦, l) where

• E is a set of events,

• C is a collection of sets of events, the configurations or states,

• ↦⊆ C × C is a relation (the transition relation) such that X ↦ Y only if Y = X ._{∪} {e}.

• l : E → Act, the labeling function.

Such an event automaton is finitary if all configurations are finite; it is rooted if ∅ ∈ C.

A rooted event automaton represents a concurrent system in the following way: action names a ∈ Act represent actions the system may perform, an event e ∈ E labeled with a represents an occurrence of a in a possible run of the system, X ∈ C represent the (unique) state of the system in which exactly the events from X have occurred, ∅ is the initial state, and X ↦ Y means that the system can evolve from state X into state Y by executing the unique event in Y − X. The domain of rooted event automata (over arbitrary alphabets) will be denoted IE.

An (event) isomorphism between two event automata is a bijective mapping between their sets of events that preserves C, ↦ and l. Usually one does not distinguish isomorphic event automata. This means that one abstracts from the identity of the events.

Definition 8.2 An event automaton (E, C, ↦, l) is reachable if it is rooted and finitary and

∅ ≠ X ∈ C ⇒ ∃e ∈ X : X − {e} ∈ C ∧ X − {e} ↦ X,

i.e. every state is reachable from the initial one by following the ↦ relation.

8.1 From event automata to process graphs and vice versa

It is straightforward to associate a process graph to a rooted event automaton:

Definition 8.3 Let A = (E, C, ↦, l) be a rooted event automaton. The associated process graph G(A) is (C, T_{A}, ∅), where (X, a, Y) ∈ T_{A} iff X ↦ Y and a is the label of the unique event in Y − X.

Proposition 8.1 A process graph of the form G(A) is nonrepetitive and configuration-deterministic.

Proof: Edges in G(A) have the form (X, a, Y), where X and Y are configurations in A. It follows immediately from the definitions that if (X, a, Y) ∼ (W, a, Z) then Y − X = Z − W. Hence, a rooted path in A(G) cannot contain two edges representing the same event. Moreover, if two rooted paths in G(A) determine the same events, they must end in the same configuration of A. □

Definition 8.4 Let G be a nonrepetitive configuration-deterministic process graph. The associated event automaton A(G) is (E_{G}, C_{G}, ↦_{G}, l_{G}), where

• X ↦_{G} Y iff there is an edge p ⟶^{a}_{G} q with X a configuration of p and Y = X ∪ {[p, a, q]}

• and l_{G} : E_{G} ↦ Act is defined by l_{G}([p, a, q]) = a.

Proposition 8.2 Let ≅ denote isomorphism, on process graphs as well as on event automata.

• If G ≅ H for nonrepetitive configuration-deterministic graphs G and H then A(G) ≅ A(H);

• and if A ≅ B for rooted event automata A and B then G(A) ≅ G(B).

Proof: Straightforward. □

The next proposition says that up to history preserving graph equivalence a nonrepetitive configuration-deterministic process graph can be recovered from its associated event automaton. It follows that no essential information is lost in the translation.

Proposition 8.3 If G ∈ ^{|}G is nonrepetitive and configuration-deterministic, then G ≤_{H} G(A(G)). Proof: It is easy to see that G(A(G)) ≅ C(G). Hence G ≤_{H} G(A(G)) by Proposition 4.4. □

In case G is configuration preserving, one even has G ≅ G(A(G)), through the isomorphism C.

It remains to be shown that also no essential information is lost in translating a rooted event automaton to a process graph. To this end I will first calculate how much information is lost in the translation and then argue that this information is inessential. In this process also a new semantic equivalence on event automata will be proposed.

8.2 Foldings on event automata

In this section I translate the notions of a folding and a history preserving folding, defined earlier on process graphs, to the realm of event automata. I also introduce a configuration preserving folding, that folds nontrivially on event automata, but corresponds with isomorphism on process graphs.

Definition 8.5 Let A, B ∈ IE. A folding from B into A is a function f : E_{B} → E_{A} such that

• l_{A}(f(e)) = l_{B}(e) for e ∈ E_{B},

• f ^{\}X′ is injective for X′ ∈ C_{B} and f̄(X′) =^{def} {f(d) | d ∈ X′} ∈ C_{A},

• the lifted function f̄: C_{B} → C_{A} satisfies

– X′ ↦_{B} Y′ ⇒ f̄(X′) ↦_{A} f̄(Y′)

– and f̄(X′) ↦_{A} Y ⇒ ∃!Y′ ∈ C_{B} : X′ ↦_{B} Y′ ∧ f̄(Y′) = Y.

The folding f is history preserving if it furthermore satisfies

f̄(X′) ↦_{A} X_{1} ↦_{A} X_{3} ∧ f̄(X′) ↦_{A} X_{2} ↦_{A} X_{3} ⇒
∃X′_{1}, X′_{2}, X′_{3} ∈ C_{B} : X′ ↦_{B} X′_{1} ↦_{B} X′_{3} ∧ X′ ↦_{B} X′_{2} ↦_{B} X′_{3} ∧ f̄(X′_{i}) = X_{i} (i = 1, 2, 3).

It is configuration preserving if f̄ is bijective. Write A ≤_{Π} B, A ≤_{H} B or A ≤_{C} B, respectively, if there is a plain, history preserving, or configuration preserving folding from B into A.

Exactly as in Propositions 2.2 and 3.3 one shows that the relations ≤_{Π}, ≤_{H} and ≤_{C} are preorders. Note that A ≅ B ⇒ A ≤_{C} B ⇒ A ≤_{H} B ⇒ A ≤_{Π} B. Using the translations G and A I now show that these notions match properly with their counterparts on process graphs.

Proposition 8.4

• If G ≤_{Π} H for nonrepetitive configuration-deterministic graphs G and H then A(G) ≤_{Π} A(H).

• If G ≤_{H} H for nonrepetitive configuration-deterministic graphs G and H then A(G) ≤_{H} A(H).

• If A ≤_{Π} B for rooted event automata A and B then G(A) ≤_{Π} G(B).

• If A ≤_{H} B for rooted event automata A and B then G(A) ≤_{H} G(B).

• If A ≤_{C} B for rooted event automata A and B then G(A) ≅ G(B).

Proof: Let f be a folding from H into G. Then the mapping f^{∗} from Proposition 4.1 is a folding from A(H) into A(G). Namely:

• l_{A(G)}(f^{∗}([p, a, q])) = l_{A(G)}([f(p), a, f(q)]) = a = l_{A(H)}([p, a, q]) for [p, a, q] ∈ E_{A(H)}.

• Let X′ ∈ C_{A(H)}. Then there is a rooted path q_{0} ⟶^{a_{1}}_{H} q_{1} ⟶^{a_{2}}_{H} ⋯ ⟶^{a_{n}}_{H} q_{n} in H, such that

X′ = {[q_{i−1}, a_{i}, q_{i}] | 0 < i ≤ n}. As f(q_{0}) ⟶^{a_{1}}_{G} f(q_{1}) ⟶^{a_{2}}_{G} ⋯ ⟶^{a_{n}}_{G} f(q_{n}) is a rooted path in G,

and G is nonrepetitive, f^{∗} ^{\}X′ is injective and f̄^{∗}(X′) = {[f(q_{i−1}), a_{i}, f(q_{i})] | 0 < i ≤ n} ∈ C_{A}.

• By the above if follows that if X′ ∈ C_{A(H)} is a configuration of q ∈ S_{H}, then f̄^{∗}(X′) ∈ C_{A(G)} is a configuration of f(q) ∈ S_{G}.

– Suppose X′ ↦_{A(H)} Y′. Then there is an edge q ⟶^{a}_{H} q′ in H with X′ a configuration of q and Y′ = X′ ∪ {[q, a, q′]}. As f is a folding, G has an edge f(q) ⟶^{a}_{G} f(q′), so f̄^{∗}(X′) ↦_{A(G)} f̄^{∗}(X′) ∪ {[f(q), a, f(q′)]} = f̄^{∗}(Y′).

– Suppose f̄^{∗}(X′) ↦_{A(G)} Y. Then there is an edge p ⟶^{a}_{G} p′ in G with f̄^{∗}(X′) a configuration of p and Y = f̄^{∗}(X′) ∪ {[p, a, p′]}. X′ must be a configuration of a node q ∈ S_{H}, so f̄^{∗}(X′) is a configuration of f(q) ∈ S_{G}. As G is configuration-deterministic, f(q) = p. Since f is a folding, there is a unique q′ ∈ S_{H} with q ⟶^{a}_{H} q′ and f(q′) = p′. It follows that there is a configuration Y′ ∈ C_{A(H)} with X′ ↦_{A(H)} Y′ and f̄^{∗}(Y′) = Y, namely X′ ∪ {[q, a, q′]}. As for uniqueness, suppose that Y′ has the required properties, then there is an edge (r, b, r′) in H with X′ a configuration of r and Y′ = X′ ∪ {[r, b, r′]}. As H is configurationdeterministic, r = q, and as f̄^{∗}(Y′) = Y it must be that f^{∗}([r, b, r′]) = [p, a, p′]. Thus b = a and f(r′) = p′. By the uniqueness requirement on f it follows that r′ = q′ and hence Y′ = X′ ∪ {[q, a, q′]}.

Now assume in addition that f is history preserving. I will show that also f^{∗} is history preserving. Suppose f̄^{∗}(X′) ↦_{A(G)} X_{1} ↦_{A(G)} X_{3} ∧ f̄^{∗}(X′) ↦_{A(G)} X_{2} ↦_{A(G)} X_{4} = X_{3}. The case X_{1} = X_{2} follows by an application of the last property of a (plain) folding, so assume X_{1} ≠ X_{2}. If follows that

X_{1} − f̄^{∗}(X′) = X_{3} − X_{2} and X_{2} − f̄^{∗}(X′) = X_{3} − X_{1}.  (1)

X′ must be a configuration of a node q ∈ S_{H}, so f̄^{∗}(X′) is a configuration of f(q) (and of no other node in G). Thus there exist edges f(q) ⟶^{a}_{G} p_{1} ⟶^{b}_{G} p_{3} and f(q) ⟶^{c}_{G} p_{2} ⟶^{d}_{G} p_{4} such that X_{i} is a configuration of p_{i} (i=1–4). As G is configuration-determistic, p_{3} = p_{4}, and by (1) a = d and b = c. Since f is history preserving there are q_{1}, q_{2}, q_{3} ∈ S_{H} such that q ⟶^{a}_{G} q_{1} ⟶^{b}_{G} q_{3} and q ⟶^{b}_{G}

q_{2} ⟶^{a}_{G} q_{3} with f(q_{i}) = p_{i} (i=1–3). Note that (q, a, q_{1}) ∼ (q_{2}, a, q_{3}) and (q, b, q_{2}) ∼ (q_{1}, b, q_{3}). Now

let X′_{1} = X′ ∪ {[q, a, q_{1}]}, X′_{3} = X′_{1} ∪ {[q_{1}, b, q_{3}]}, X′_{2} = X′ ∪ {[q, b, q_{2}]} and X′_{4} = X′_{2} ∪ {[q_{2}, a, q_{3}]}. Then X′_{3} = X′_{4} and

X′ ↦_{A(H)} X′_{1} ↦_{A(H)} X′_{3} ∧ X′ ↦_{A(H)} X′_{2} ↦_{A(H)} X′_{3} ∧ f̄(X′_{i}) = X_{i} (i = 1–3).

The last three statements of the proposition follow immediately from the definitions. □

Now I show that up to a history preserving folding any event automaton can be retrieved from its graph representation. For an important class of event automata this even holds up to a configuration preserving folding, and for a subclass up to isomorphism.

Theorem 3 A ≤_{H} A(G(A)) for any rooted event automaton A. Moreover, if G(A) is a configuration preserving process graph, then A ≤_{C} A(G(A)). Finally, if A = A(G) with G a configuration preserving process graph, then A ≅ A(G(A)).

Proof: Let A ∈ IE. For X, Y ∈ C_{A} with X ↦_{A} Y let e(X, Y) be the unique event in Y − X. If follows easily from Definition 8.1 that for X, Y, Z, W ∈ C_{A}

X ↦_{A} Y ↦_{A} Z, X ↦_{A} W ↦_{A} Z, Y ≠ W ⇒ e(X, Y) = e(W, Z).

Thus, for (X, a, Y), (W, b, Z) ∈ T_{G(A)} with (X, a, Y) ∼ (W, b, Z) one has e(X, Y) = e(W, Z) and (hence) a = b. Now the function f is well-defined by f([X, a, Y]) = e(X, Y) for [X, a, Y] ∈ E_{A(G(A))}.

Let [X, a, Y] ∈ E_{A(G(A))}. Then l_{A}(f([X, a, Y])) = l_{A}(e(X, Y)) = a = l_{A(G(A))}([X, a, Y]).

Let X′ ∈ C_{A(G(A))}. Then X′ = {[X_{i−1}, a_{i}, X_{i}] | i = 1, ..., n} with a_{i} = l_{A}(e(X_{i−1}, X_{i})) for certain sequence ∅ = X_{0} ↦_{A} X_{1} ↦_{A} X_{2} ↦_{A} ⋯ ↦_{A} X_{n}. For 1 ≤ i < j ≤ n one has

f([X_{i−1}, a_{i}, X_{i}]) = e(X_{i−1}, X_{i}) ∈ X_{i} ⊆ X_{j−1} ∌ e(X_{j−1}, X_{j}) = f([X_{j−1}, a_{j}, X_{j}]).

Hence f ^{\}X′ is injective. Moreover f̄(X′) = X_{n} ∈ C_{A}.

Note that for X′ ∈ C_{A(G(A))}, f̄(X′) is the unique node p ∈ S_{G(A)} such that X′ is a configuration of p. By Definition 8.4 this immediately yields X′ ↦_{B} Y′ ⇒ f̄(X′) ↦_{A} f̄(Y′).

Suppose f̄(X′) ↦_{A} Y for X′ ∈ C_{A(G(A))}. Let Y′ =^{def} X′∪{[f̄(X′), a, Y]} with a = l_{A}(e(f̄(X′), Y)).

Then X′ ↦_{A(G(A))} Y′ and f̄(Y′) = f̄(X′) ∪ {e(f̄(X′), Y)} = Y. Now suppose X′ ↦_{A(G(A))} Z′ and f̄(Z′) = Y. Then there must be a Z ∈ C_{A} and a b with f̄(X′) ↦_{A} Z and Z′ = X′ ∪ {[f̄(X′), b, Z]}. As Y = f̄(Z′) = f̄(X′) ∪ {e(f̄(X′), Z)} = Z, it follows that b = a and Z′ = Y′.

Finally, suppose f̄(X′) ↦_{A} X_{1} ↦_{A} X_{3} ∧ f̄(X′) ↦_{A} X_{2} ↦_{A} X_{4} = X_{3} for X′ ∈ C_{A(G(A))}. Let a = l_{A}(e(f̄(X′), X_{1})) and b = l_{A}(e(f̄(X′), X_{2})). The case X_{1} = X_{2} follows by an application of the last property of a (plain) folding, so assume X_{1} ≠ X_{2}. If follows that e(f̄(X′), X_{1}) = e(X_{2}, X_{3}),

e(f̄(X′), X_{2}) = e(X_{1}, X_{3}), (f̄(X′), a, X_{1}) ∼ (X_{2}, a, X_{3}) and (f̄(X′), b, X_{2}) ∼ (X_{1}, b, X_{3}). Let X′_{1} =^{def}

X′ ∪ {[f̄(X′), a, X_{1}]}, and define X′_{2}, X′_{3} and X′_{4} likewise. Then X′_{3} = X′_{4} and

X′ ↦_{A(G(A))} X′_{1} ↦_{A(G(A))} X′_{3} ∧ X′ ↦_{A(G(A))} X′_{2} ↦_{A(G(A))} X′_{3} ∧ f̄(X′_{i}) = X_{i} (i = 1, 2, 3).

Thus, I have shown that A ≤_{H} A(G(A)) for any rooted event automaton A.

Now suppose that A is configuration preserving. I have to show that f̄ is bijective.

Suppose f̄(X′) = f̄(Y′) = Z for X′, Y′ ∈ C_{A(G(A))}. Then X′ and Y′ are both configurations of Z ∈ S_{G(A)}. As G(A) is configuration preserving, it must be that X′ = Y′. So f̄ is injective.

By Definition 4.2 configuration preserving event automata are reachable. Hence for any configuration X ∈ C_{A} there is a sequence ∅ = X_{0} ↦_{A} X_{1} ↦_{A} ⋯ ↦_{A} X_{n} = X. Let a_{i} = l(e(X_{i−1}, X_{i})). Now X′ =^{def} {[X_{i−1}, a_{i}, X_{i}] | i = 1, ..., n} ∈ C_{A(G(A))} and f̄(X′) = X. It follows that f̄ is surjective.

The last statement of the theorem follows immediately from the remark after Proposition 8.3. □

Definition 8.6 Let A ∈ IE. The history preserving folding f : E_{A(G(A))} → E_{A} constructed above is called the canonical folding from A(G(A)) to A.

8.3 Event automata with recognizable events

In this section I characterize the event automata A that can be completely recovered from their graph representation, in the sense that the canonical folding from A(G(A)) to A is an isomorphism.

Definition 8.7 An event automaton has (graph-)recognizable events if it is reachable, every event occurs in a configuration, and every pair of transitions (X, a, Y) and (U, a, V) in G(A) with Y −X = V − U represents the same event in the sense of Definition 4.1.

This ensures that the events of the event automaton can in some sense be recognized (as equivalence classes of transitions) from its graph representation. This is just what is needed to get the following.

Proposition 8.5 Let A ∈ IE. The canonical folding from A(G(A)) to A is an isomorphism iff A has recognizable events.

Proof: Let A have recognizable events. As each event occurs in a reachable configuration, the canonical folding f is surjective, whereas the requirement on transitions ensures it is injective. As f is a moreover a folding it preserves ↦ and l. Finally, the reachablility of A ensures that the lifted function f̄ is surjective, as in the second last paragraph in the proof of Theorem 3. This implies that X ∈ C_{A} iff f̄(X) ∈ C_{A(G(A))}, i.e. f preserves configurations.

Now let f be an isomorphism. As A(G(A)) is reachable, A must be reachable too. Therefore G(A) is reachable, which implies that every event in A(G(A)) occurs in a configuration. The same must hold for A. Finally, the requirement on transitions is equivalent with f being injective. □

Although the counterexamples are infinite and too complicated to display here, it is possible that A ≅ A(G(A)) even when A doesn’t have recognizable events. In that case, however, the isomorphism between A and A(G(A)) is an ‘accidental’ one, not given by the canonical folding.

Theorem 3 gave already a condition under which A ≅ A(G(A)). The following says that that condition is equivalent to the one of Definition 8.7.

Proposition 8.6 An event automaton A has recognizable events iff A ≅ A(G) for a configuration preserving process graph G (with G ≅ G(A)).

Proof: “if”: Let G ∈ ^{|}G be configuratation preserving. A(G) is always reachable. As G is reachable, every event of A(G) occurs in a configuration. Recall that C_{A(G)} = {C(p) | p ∈ S_{G}}, by Definition 4.2. Let (C(p), a, C(q)) and (C(r), a, C(s)) be transitions in G(A(G)) with C(q)−C(p) = C(s)−C(r). Then (p, a, q) ∼ (r, a, s). As C : S_{G} → S_{G(A(G))} is an isomorphism, also (C(p), a, C(q)) and (C(r), a, C(s)) represent the same event.

“only if”: Let A ∈ IE be recognizable. Then A and hence G(A) is reachable. By Proposition 8.1, G(A) is configuration-deterministic. Now suppose there are two rooted paths in G(A) ending in the same node X ∈ C_{A} that determine different configurations. Then there must be an event in X that is the image of two different events in A(G(A)) under the canonical folding from A(G(A)) to A, contradicting Proposition 8.5. □

8.4 Configuration preserving event automata

Definition 8.8 Call a rooted event automaton A configuration preserving if G(A) is so.

This name is motivated by the configuration preserving folding between such an A and A(G(A))— inducing a bijection between their configurations—that exists by Theorem 3.

Proposition 8.7 Let A ∈ IE. The canonical folding from A(G(A)) to A is configuration preserving iff A is configuration preserving.

Proof: “if” has been established in Theorem 3. “only if”: If A is not configuration preserving, G(A) either has unreachable states, or has two rooted paths ending in the same state that determine a different configuration. In the first case A(G(A)) is reachable whereas A isn’t, so the lifted function f̄ fails to be surjective. In the second case f̄ fails to be injective. □

Again, it may be that A ≤_{C} A(G(A)) even when A is not configuration preserving. In that case, however, the configuration preserving folding between A and A(G(A)) is ‘accidental’, not canonical.

In this section I evaluate how much information is lost when translating a configuration preserving event automaton into a process graph. The following example is typical.

Example 1 Consider the event automaton B depicted below. E_{B} and l_{B} are given as a table; C_{B} and ↦_{B} are drawn like a graph. It is shown how G and A ∘ G apply to B. G(B), and hence B, is configuration preserving, and G(A(G(B))) ≅ G(B).

[figure: \begin{matrix}B : \\ e_{1} & a \\ e_{2} & b \\ e_{3} & c \\ e_{0} & d \end{matrix}; ∅; \{e_{1}\}; \{e_{2}\}; \{e_{1}, e_{2}\}; \{e_{1}, e_{3}\}; \{e_{2}, e_{3}\}; \underrightarrow{G}; a; a; c; b; b; c; \begin{matrix}A \\ ⟶ \\ ⟵ \\ G \end{matrix}; ∅; \{f_{1}\}; \{f_{2}\}; \{f_{1}, f_{2}\}; \{f_{1}, f_{3}\}; \{f_{2}, f_{4}\}; \begin{matrix}A(G(B)) \\ f_{1} & a \\ f_{2} & b \\ f_{3} & c \\ f_{4} & c \end{matrix}]

Note that event f_{1} is an equivalence class containing two edges, that can explicitly be written as f_{1} = {(∅, a, {e_{1}}), ({e_{2}}, a, {e_{1}, e_{2}})}, and likewise for f_{2}, f_{3} and f_{4}. Here I use that the identity of the states of G(B) is the same as the identity of the corresponding states of B. However, the point of this example is to show that B can to a large extend be retrieved from G(B), even when considering G(B) only up to isomorphism. If one would forget the identity of the states of G(B) and just name them s, t, ..., then by Proposition 8.2 applying A on this graph still gives an event automaton isomorphic to A(G(B)). Therefore I prefer to use fresh names for the events in A(G(B)).

The event automaton A(G(B)) fails to be isomorphic to A for two reasons: first of all the event e_{0} of B that did not occur in any configuration did not return in A(G(B)). Secondly, the event e_{3} is split into f_{3} and f_{4}. The first need not concern us, as events that do not occur in a single configuration carry no semantic significance. The second might be a concern if one wants to represent a system ‘efficiently’, using a minimum amount of events. However, from a semantic point of view an event is an occurrence of an action (in this case the action c) in a possible run of the represented system. As the run with a and c is a different one from the run with b and c, it seems appropriate to distinguish between the occurrences of c in these runs. Hence A(G(B)) describes the same system as B; applying A∘G merely results in a normalization of the description.

In general applying A ∘ G results in the spitting of an event that occurs in disconnected parts of the automaton into one copy for each in these parts. In particular the event disappears if it does not occur anywhere. Here a partition of the configurations containing a given event is disconnected if no two parts contain configurations X and Y with X ↦ Y. Below, the resulting normalization proceedure is defined directly under the name ‘configuration unfolding’. Subsequently I show that applying A ∘ G yields the same result as applying this unfolding.

Definition 8.9 Let A be an event automaton. An event occurrence in A is a pair (e, X) with X a configuration and e ∈ X. Connectedness is the least equivalence relation ≈ on event occurrences such that (e, Y) ≈ (e, Z) if Y ↦ Z. A is said to have configuration-recognizable events if every event occurs in a configuration and all occurrences of the same event are connected.

Definition 8.10 Let e_{X} denote the equivalence class containing (e, X) w.r.t. ≈ in an event automaton A; i.e. the set of all occurrences of e connected to (e, X), and write X_{X} = {e_{X} | e ∈ X}. Thus d ∈ Y ↦ Z implies d_{Y} = d_{Z} and Y_{Y} = Y_{Z}. The configuration unfolding C(A) of A is defined by:

• E_{C(A)} = {e_{X} | e ∈ X ∈ C_{A}},

• C_{C(A)} = {X_{X} | X ∈ C_{A}},

• ↦_{C(A)}= {(X_{Y} , Y_{Y}) | X ↦_{A} Y },

• l_{C(A)}(e_{X}) = l_{A}(e).

Two event automata A and B are configuration isomorphic—notation A =_{C} B—if C(A) ≅ C(B).

Proposition 8.8 The configuration unfolding of any rooted event automaton A has configurationrecognizable events, and if A has configuration-recognizable events then C(A) ≅ A. Proof: Straightforward. □

It follows that up to (event) isomorphism every configuration isomorphism class of rooted event automata contains exactly one event automaton with configuration-recognizable events, which can be obtained from an arbitary member of the class by means of configuration unfolding. Thus C brings rooted event automata in a kind of normal form. Moreover, it does so without changing their behaviour.

Next I show that configuration isomorphism is the equivalence closure of ≤_{C}. Thus configuration unfoldings relate to configuration preserving foldings in the same way as (history) unfoldings relate to (history preserving) foldings on process graphs (cf. Sections 2 and 3).

Proposition 8.9 A ≤_{C} C(A) for any rooted event automaton A.

Proof: Define f : E_{C(A)} → E_{A} by f(e_{X}) = e for e ∈ X ∈ C_{A}. Then f̄(X_{X}) = X for X ∈ C_{A}, and f satisfies the requirements of a configuration preserving folding from Definition 8.5. □

Proposition 8.10 If A ≤_{C} B then C(A) ≅ C(B).

Proof: Let f be a configuration preserving folding from B to A. For (e, X) an event occurrence in B let f(e, X) =^{def} (f(e), f̄(X)). If e ∈ Y ↦_{B} Z then f(e) ∈ f̄(Y) ↦_{A} f̄(Z), so

(e, Y) ≈_{B} (e, Z) ⇒ f(e, Y) ≈_{A} f(e, Z).

Hence I may define f′ : E_{C(B)} → E_{C(A)} by f′(e_{X}) = f(e)_{f̄(X)}. I check that f′ is an isomorphism.

• f′ is surjective because f̄ is surjective.

• Suppose f′(e_{X}) = f′(d_{Y}). Then f(e) = f(d) and (f(e), f̄(X)) ≈_{A} (f(e), f̄(Y)). Because f̄ is bijective and preserves the transition relation, this implies (e, X) ≈_{B} (d, Y). Hence e_{X} = d_{Y}.

• f′(X_{X}) ↦_{C(A)} f′(Y_{Y}) ⇔ f̄(X)_{f̄(X)} ↦_{C(A)} f̄(Y)_{f̄(Y)} ⇔ f̄(X) ↦_{A} f̄(Y) ⇔ X ↦_{B} Y ⇔ X_{X} ↦_{C(B)} Y_{Y}.

• l_{C(A)}f′(e_{X}) = l_{C(A)}(f(e)_{f̄(X)}) = l_{A}(f(e)) = l_{B}(e) = l_{C(B)}(e_{X}). □

Theorem 4 =_{C} is the smallest equivalence containing ≤_{C}. Proof: If A =_{C} B then A ≤_{C} C(A) ≅ C(B) ≥_{C} B by Proposition 8.9. Hence =_{C} is contained in the smallest equivalence containing ≤_{C}. The reverse follows since ≤_{C}⊆=_{C}, by Proposition 8.10.□

The above correspondence between =_{C} and ≤_{C} holds for arbitrary rooted event automata. However, the promised correspondence between C and A ∘ G applies to configuration preserving event automata only. For technical convenience in establishing this correspondence, I first relate the two notion of recognizablility.

Proposition 8.11 A reachable event automaton with graph-recognizable events has configurationrecognizable events.

Proof: Let (e, Y) and (e, Z) be event occurrences in a reachable event automaton A with graphrecognizable events. I have to show that (e, Y) ≈ (e, Z). Let Y′ and Z′ be configurations of minimal size such that (e, Y′) ≈ (e, Y) and (e, Z′) ≈ (e, Z). As A is reachable, it must be that Y′ − {e} ↦ Y′ and Z′ − {e} ↦ Z′. By assumption, the transitions (Y′ − {e}, l_{A}(e), Y′) and (Z′ − {e}, l_{A}(e), Z′) represent the same event. By Definitions 4.1 and 8.9 this implies that (e, Y′) and (e, Z′) are connected, and hence (e, Y) ≈ (e, Z). □

Theorem 5 Let A be a configuration preserving event automaton. Then C(A) ≅ A(G(A)).

Proof: Let A be a configuration preserving event automaton. Then A ≤_{C} A(G(A)) by Theorem 3. Hence C(A) ≅ C(A(G(A))) by Proposition 8.10. Furthermore, A(G(A)) has configuration-recogni-zable events by Propositions 8.6 and 8.11, so C(A(G(A))) ≅ A(G(A)) by Proposition 8.8. □

Corollary 8.1 A rooted event automaton has (graph-)recognizable events iff it is configuration preserving and has configuration-recognizable events. Proof: “only if” combines Propositions 8.6 (“only if”) and 8.11; “if” combines Theorem 5 and Proposition 8.8, and applies the “if”-direction of Proposition 8.6.

Thus, configuration preserving event automata with configuration-recognizable events can, up to isomorphism, be fully recovered from their graph representation. This does not hold for the larger class of configuration preserving event automata, but, as argued above, the information that is lost when representing such event automata by process graphs is semantically inessential.

8.5 Interpreting general event automata

Next I will show that any rooted event automaton can be translated into a process graph in such a way that all information on the causal and branching structure of the represented system is preserved. To a certain extent this requires equipping rooted event automata with a computational interpretation. For configuration preserving event automatas the computational interpretation is well understood, and that my translation preserves this interpretation is a statement. But other event automata do not have such a clear meaning, and for those the translation can be understood as defining an interpretation.

A rooted event automaton can fail to be configuration preserving only because (1) it is unreachable, or (2) its associated process graph has two rooted paths ending in the same state that determine the same configuration.

First I will give an example of a reachable event automaton A such that G(A) is not a configuration preserving process graph.

Example 2 Consider the event automaton C depicted below. C_{C} and ↦_{C} are drawn like a graph, E_{C} = ⋃_{X∈C_{C}} X and l_{C} is given by l(e_{i}) = i. As G(A(G(C))) ≅ G̸(C), C is not configuration preserving. However, the event automaton A(G(C)) is; it even has recognizable events, and consequently A(G(A(G(C)))) ≅ A(G(C)).

[figure: C:; ∅; \{e_{1}\}; \{e_{2}\}; \{e_{1}, e_{2}, e_{3}\}; \{e_{1}, e_{3}\}; \{e_{2}, e_{3}\}; \underrightarrow{G}; 1; 1; 3; 2; 2; 3; \underrightarrow{A}; ∅; \{f_{1}\}; \{f_{1}, f_{3}\}; \{f_{1}, f_{2}, f_{3}\}; \{g_{2}\}; \{g_{2}, g_{3}\}; \{g_{1}, g_{2}, g_{3}\}; \begin{matrix}G \\ ⟶ \\ ⟵ \\ A \end{matrix}; 1; 3; 2; 2; 3; 1]

Text

In process graphs the unreachable parts are usually taken to be semantically irrelevant. In particular any process graph is history preserving graph equivalent with its reachable part. It is possible to apply the same policy to event automata. This fits nicely with the circumstance that after translating a rooted event automaton to a process graph and back, its unreachable part is gone. It should be noted however, that, due to the nature of the transition relation, the unreachable parts include all infinite configurations. Disregarding those could be justified computationally by the postulate that in a finite time only finitely many events can happen. Computational interpretations that do not adopt this postulate, and consequently take infinite configurations seriously, may not be translatable to the realm of process graphs.

9 Event and configuration structures

Definition 9.1 A (labeled) event automaton is called a (labeled) configuration structure [GP95] when X ↦ Y iff Y = X ._{∪} {e}. Such event automata are represented by triples (E, C, l).

Various brands of event structures have been proposed in the literature. In every brand an event structure consist of a set of events and some structure. Labeled event structures moreover have a labeling function, exactly as in Definition 8.1. The behaviour of event structures is commonly given by a concept of configuration, this being a set of events representing a state or run. Usually also infinite configurations are considered, but the infinite configurations of an event structure are completely determined by its finite ones. Concentrating on the finite configurations yields an immediate translation to finitary configuration structures.

Definition 9.2 Prime, stable and [general] event structures are defined in [Win87], as well as a function F, associating with every event structure E its family of configuration F(E). For (E, l) a labeled event structure, let C(E) be the finitary configuration structure (E_{E}, C_{E}, l) with E_{E} the set of events of E and C_{E} the set of finite configurations in F(E). Furthermore, let G(E) = G(C(E)).

Proposition 9.1 The configuration structures arising from general event structures (i.e. of the form C(E) with E an event structure) can be characterized as the reachables ones satisfying

X, Y, Z ∈ C ∧ X ∪ Y ⊆ Z ⇒ X ∪ Y ∈ C.^{3}  (2)

The ones arising from stable respectively prime event structures can be characterized as the ones above, additionally satisfying

X, Y, Z ∈ C ∧ X ∪ Y ⊆ Z ⇒ X ∩ Y ∈ C,

respectively

X, Y ∈ C ⇒ X ∩ Y ∈ C.

Proof: This follows immediately from the characterization of the families of infinite configurations of general structures in [Win87], cf. [GP95]. □

It follows that the process graph K from Section 6 can not be represented as an event structure; the union of the configurations {a} and {b} is not itself a configuration. Likewise, J cannot be represented as a stable (or prime) event structure; the intersection of {a, c} and {b, c} fails to be a configuration.

9.1 Event structures are configuration preserving

In this section I substantiate my claim that process graphs capture all causal subtleties that are expressible by means of event structures. For the prime event structures this claim is of a purely mathematical nature: up to isomorphism a labeled prime event structure can be completely recovered from its process graph representation.

Theorem 6 There exists a function E, associating with every process graph G a labeled prime event structure E(G), such that E(G(E)) ≅ E for every labeled prime event structure E.

Proof: In [GV95]. □

As remarked in [Gla88], the special case of this theorem dealing with unlabeled prime event structures with a binary conflict relation can be obtained as a corollary of Theorem 9 of [NPW81].

3The term configuration structure originates from [GG90], were however it referred only to reachable configuration structures satisfying this requirement.

Theorem 6 could have been modularized by stating that for E a prime event structure, C(E) is a configuration preserving event automaton with recognizable events, and E can, up to isomorphism, be recovered from C(E). This theorem does not generalize to stable event structures, let alone to general ones. First of all information is lost in the translation of (stable) event structures to configuration structures, and secondly in the translation of the resulting structures to process graphs. The latter is illustrated by the event automaton B of Example 1, that arises as the C-image of a stable event structure. As observed in [GP95], no information is lost in the intermediate step of dropping the infinite configurations from the families of configurations of event structures. Winskel [Win87] argues that all relevant information about the behaviour of an event structure is contained in its family of configurations, i.e. the information lost in the first step is inessential. The following theorem allows application of the argument from the previous section (to a large extent also due to Winskel) to the finitary configuration structures obtained as images of event structures. It follows that also all information lost in the last step is inessential.

Theorem 7 For E an event structure, C(E) is a configuration preserving configuration structure.

Proof: By Proposition 9.1 I have to prove that for reachable configuration structures C satisfying (2), G(C) is configuration preserving. By Proposition 8.1, G(C) is configuration-deterministic, so it suffices to prove the stronger statement that G(C) is history preserving. That every node in G(C) has at least one history follows from the reachability of C. Thus it is left to show that in G(C) any two rooted paths that end in the same node are homotopic.

With induction on their length I even establish that any two paths X_{0} ↦ X_{1} ↦ ⋯ ↦ X_{n} and Y_{0} ↦ Y_{1} ↦ ⋯ ↦ Y_{m} starting and ending in the same state (i.e. X_{0} = Y_{0} and X_{n} = Y_{m}, hence n = m) are homotopic. Suppose one has two paths as above, and assume the statement holds for strictly shorter paths which share their start and endnodes. Let k be the smallest index such that Y_{1} ⊆ X_{k}. Then there is a path X_{0} ↦ X_{0} ∪ Y_{1} ↦ X_{1} ∪ Y_{1} ↦ ⋯ X_{k−1} ∪ Y_{1} = X_{k} ↦ ⋯ ↦ X_{n} in C. By induction this path is homotopic with Y_{0} ↦ Y_{1} ↦ ⋯ ↦ Y_{n} (the induction hypothesis may be invoked because X_{0} ∪ Y_{1} = Y_{1}). As X_{i} ↦ X_{i} ∪ Y_{1} for i = 0, ..., k−1 also X_{0} ↦ X_{1} ↦ ⋯ ↦ X_{n} is homotopic with this path (through k −1 adjacency steps), and the required result follows by transitivity. □

10 Scott domains

Prime event structures with a binary conflict relation were introduced in [NPW81] as a stepping stone in the translation between Petri nets and Scott domains. In short, such an event structure arises as an abstraction of a safe net, and a domain (being special kind of partial order) is obtained from an event structure as the inclusion order on its set of configurations. In [NPW81] a “curious mismatch” is observed between the domains that result from this translation, and the ones originally studied by Scott. Although mathematically of the same nature, a domain that arises from an event structure represents a process or concurrent system, namely the same one represented by the Petri net or event structure it originated from. In domain theory, processes show up at best as the points in a domain. Thus the use of domains to represent concurrent systems is novel with [NPW81].

Under the postulate that the systems described by nets, event structures or domains can do only finitely many actions in a finite time—a postulate made in virtually all further work on event structures—the infinitary parts of domains are redundant, in the sense that they can be recovered in full from the finitary parts (which can be obtained from event structures by ordering the finite configurations under inclusion). A finitary domain can, without loss of information, be trivially represented, and is often displayed, as an unlabeled rooted graph. Therefore I argue that the correspondence between event structures and domains proposed in [NPW81], and generalized to all event structures in [Win87], can equivalently, or maybe better, be regarded as a correspondence between event structures and unlabeled transition systems. In the present paper (and [Gla88]) this correspondence is extended to labeled event structures and transitions systems; the latter are easier to label then domains. Moreover, the computational interpretation of domains, inherited from that of event structures, is extended to transition systems that do not correspond to event structures or Scott domains. It can be seen as an enrichment of the classical interpretation of transition systems.

10.1 characterizations of event, stable and prime.

Duality for prime.

11 Related work

Several researchers have equipped process graphs with a concurrent interpretation by adding some extra structure. In [Shi85] and [Bed87] this structure has the shape of a global independence relation on Act, whereas [Sta89] uses explicit independence relations between the outgoing edges of any given state. The present approach in some sense reaches the same objective without introducing extra structure on transition systems.

In [RT88] the model of behavior structures is introduced. These are a class of transition systems in which the states are labeled with pomsets (partially ordered multisets of action occurrences), and the transitions with embeddings of the source pomset in the target one. This model combines causality and branching time. Abstraction to just causality occurs by forgetting the transition system and keeping the pomsets; abstraction to “interleaving semantics” by forgetting the pomsets and keeping the transition system (an operation called milnering). The results of the current paper can be understood as saying that actually no information is lost in the milnering.

As indicated at the end of Section 6, the concurrent interpretation of process graphs allows one to think of squares and cubes as being “filled in”. [Pra91] proposes a geometric model of concurrency, refining the approach of this paper by not necessarily filling in all squares and cubes, but explicitly filling in only those that we want to represent concurrency. Although the resulting model of higher dimensional automata is more complicated than plain automata, it is more expressive as well.

more geometry

References

[Bed87] M. Bednarczyk (1987): Categories of asynchronous systems. PhD thesis, Computer Science, University of Sussex, Brighton.

[BW90] J.C.M. Baeten & W.P. Weijland (1990): Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press.

[CDL95] F. Corradini, R. De Nicola & A. Labella (1995): Fully abstract models for nondeterministic regular expressions. In I. Lee & S.A. Smolka, editors: Proceedings CONCUR 95, Philadelphia, PA, USA, LNCS 962, Springer-Verlag, pp. 130–144.

[GG90] R.J. van Glabbeek & U. Goltz (1990): Refinement of actions in causality based models. In J.W. de Bakker, W.P. de Roever & G. Rozenberg, editors: Proceedings REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, Mook, The Netherlands, May/June 1989, LNCS 430, Springer-Verlag, pp. 267–300.

[Gla88] R.J. van Glabbeek (1988): An operational non-interleaved process graph semantics of CCSP (abstract). In E.-R. Olderog, U. Goltz & R.J. van Glabbeek, editors: Combining compositionality and concurrency, summary of a GMD-workshop, Königswinter, March 1988, Arbeitspapiere der GMD 320, pp. 18–19.

[Gla94] R.J. van Glabbeek (1994): What is branching time semantics and why to use it? In M. Nielsen, editor: The Concurrency Column, Bulletin of the EATCS 53, pp. 190–198. Also available as Report STAN-CS-93-1486, Stanford University, 1993, and by ftp at

ftp://Boole.stanford.edu/pub/DVI/branching.dvi.gz.

[GP95] R.J. van Glabbeek & G.D. Plotkin (1995): Configuration structures (extended abstract). In Proceedings 10^{th} Annual Symposium on Logic in Computer Science (LICS95), Philadelphia, USA. IEEE Computer Society Press.

[GV95] R.J. van Glabbeek & F.W. Vaandrager (1995): The difference between splitting in n and n+1. Report CS-R9553, CWI, Amsterdam. Abstract in E. Best and G. Rozenberg, editors: Proceedings 3^{rd} Workshop on Concurrency and Compositionality, Goslar, May 1991, GMD-Studien Nr. 191, Universität Hildesheim, pp. 117–121.

[Mil89] R. Milner (1989): Communication and Concurrency. Prentice-Hall International, Englewood Cliffs.

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

[PP95] G.M. Pinna & A. Poigné (1995): On the nature of events: another prespective in concurrency. Theoretical Computer Science 138(2), pp. 425–454.

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

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

[Shi85] M.W. Shields (1985): Concurrent machines. The Computer Journal, 28(5).

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

[Win87] G. Winskel (1987): Event structures. In W. Brauer, W. Reisig & 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, Springer-Verlag, pp. 325–392.