BRICS RS-95-57 J. van Oosten: Topological Aspects of Traces

BRICS

Basic Research in Computer Science

Topological Aspects of Traces

Jaap van Oosten

BRICS Report Series RS-95-57 ISSN 0909-0878 November 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

Topological Aspects of Traces

Jaap van Oosten BRICS^{∗} Department of Computer Science University of Aarhus, Denmark

17 November 1995

Introduction. This paper is a little mathematical study of some models of concurrency. The most elementary one is the concept of an independence structure, which is nothing but a set L with a binary, irreflexive and symmetric rlation on it, the independence relation. This leads to the notion of a trace: a string of elements of L, modulo the equivalence generated by swapping adjacent, independent elements of the string.

There are two aspects of finite traces: they form an order, hence a topology; on the other hand they form a monoid, a quotient of the free monoid on L. Unfortunately, these two points of view are hard to bring together, since the monoid structure can never be continuous or even order-preserving. It is therefore not surprising that many papers on trace theory consist of two, disjoint, parts. In this paper I concentrate on the order-theoretic and topological aspects.

In the first two sections, the set of infinite traces is considered from a topological point of view. It is well-known (e.g. [Kwi]) that taking both finite and infinite traces, yields a Scott domain. There are reasons to consider also the set of just the infinite traces, arguing that important processes are always ongoing, potentially infinite things.

The infinite traces in themselves do not constitute a Scott domain for lack of finite elements, but as a topological space they arise as what can be seen as a generalization of the ideal completion construction in domain theory: namely, soberification. This is done in section 2. Since the points of the space are traces, that is labelled partial orders, it is also shown how many important topological properties of these points can be expressed entirely in terms of this labelled poset structure.

Section 3 treats a group action on the set of all infinite L-words, depending on the independence relation, such that the orbits of the action are the equivalence classes under: finitely many swappings of independent pairs. One has a nice characterization of these orbits in terms of certain “action graphs”, called “good”. One observes that inclusion of good graphs corresponds to order-reflecting bijections between the corresponding partial orders; which is similar to the orderreflecting bijection that a map of event structures induces on a configuration by restriction.

∗

Basic Research in Computer Science,

Centre of the Danish National Research Foundation.

Therefore, in section 4, we look at a category of systems of posets and systems of order-reflecting bijections as maps. We see that labelled event structures are a full reflective subcategory of this, as are independence structures.

1 Characterization of Independence Structures

Let X be a set. The purpose of this section and the next one is to represent independence relations on X as topological spaces. The points of these spaces are X-labelled partial orders, and one can express topological properties of these points in terms of this labelled poset structure.

Some definitions:

In a partial order (P, ≤) we write x <^{d} y for “x is directly below y”, i.e. x < y ∧ ∀z(x ≤ z ≤ y ⇒ x = z ∨ y = z).

(P, ≤) is locally finite if for every p ∈ P, the set ↓ p = {q ∈ P | q ≤ p} is finite. An X-labelled partial order is a partial order (P, ≤) together with a function

l : P → X.

Lemma 1.1 A countable partial order is locally finite if and only if it has a linear extension which can be embedded in ω.

Proof. Trivial.

Definition 1.2 Let (P, ≤) be a countable, locally finite, infinite poset with labelling l : P → X, such that for every x ∈ X the set l^{−1}(x) is a linearly ordered subset of P. For α ∈ X^{ω} we say that α extends (P, ≤) if there is a bijective function f : P → ω which is order preserving and such that α ∘ f = l.

Note that by the requirements on (P, ≤), such f is unique if it exists. For two such posets (P, ≤, l) and (Q, ≤′, l′) we say that (P, ≤, l) extends (Q, ≤′, l′) if every α which extends(P, ≤, l), also extends (Q, ≤′, l′). This is equivalent to: there is a bijective function Q → P which is order preserving, i.e. the order on Q is a subset of the order on P.

Definition 1.3 Let P be a set of countably infinite, locally finite X-labelled partial orders. Such a set is called a complete system if the following conditions hold: i) For all (P, ≤, l) in P and all x ∈ X, l^{−1}(x) is a linearly ordered subset of

P;

ii) Every α ∈ X^{ω} extends exactly one (P, ≤, l) in P;

iii) If p <^{d} q in some (P, ≤, l) in P then for all (P′, ≤′, l′) in P and r, s ∈ P′ with l′(r) = l(p), l′(s) = l(q), either r ≤′ s or s ≤′ r.

Given two complete systems P, Q on X, say P ⪯ Q if for every (P, ≤, l) in P there is a unique (Q, ≤′, l′) in Q such that (P, ≤, l) extends (Q, ≤′, l′). This defines a preorder on the class of complete systems on X.

Theorem 1.4 There is an order-isomorphism between isomorphism classes of complete systems on X and independence relations on X, ordered by inclusion.

Proof. Given an independence relation I on X we define an equivalence relation ∼_{I} on X^{ω} as the smallest which contains (α, β) whenever for some i ∈ ω, (α(i), α(i + 1)) ∈ I, β(j) = α(j) for j ≠ i, i + 1, and β(i) = α(i + 1) and β(i + 1) = α(i).

Furthermore we put α ≈_{I} β if for all n ∈ ω there is both a β′ ∼_{I} β with ∀i < n.α(i) = β′(i), and an α′ ∼_{I} α with ∀i < n.β(i) = α′(i).

Any ≈_{I}-equivalence class C determines a countably infinite, locally finite poset ⋂ C since there is a set P such that all α ∈ C can be regarded as linear orders on P: writing for x ∈ X and α ∈ X^{ω}, x_{α} for the number of times x appears in α (may be ω), x_{α} = x_{β} whenever α ≈_{I} β, and P = {(x, i)| x ∈ X ∧ i < x_{α}} for some α ∈ C. So the order on P is the intersection of all the linear orders on P, determined by the elements of C.

We put l(x, i) = x, and it is clear that (P, ≤, l) is a locally finite labelled poset such that l^{−1}(x) is a linearly ordered subset. Put P_{I} = {⋂ C| C ∈ X^{ω}/ ≈_{I}}.

The operation I ↦ P_{I} is obviously injective since if (x, y) ∈ I, (x, y) ∉ J there will be P in P_{I}, p, q ∈ P with labels x, y respectively, and p, q incomparable in P; but there will be no such in P_{J}.

Conversely, given a complete system P on X, by requirement ii) of definition 1.3, we can define an equivalence relation ≈_{P} on X^{ω} by: α ≈_{P} β if α and β extend the same element of P. On the other hand we put:

I = {(x, y)| for some (P, ≤, l) ∈ P, there is p, q ∈ P with
l(p) = x, l(q) = y and p, q unrelated w.r.t. ≤}

By i) of definition 1.3, I is an independence relation. To show that P is isomorphic to P_{I} it clearly suffices to show that ≈_{P} is the equivalence relation ≈_{I} induced by I as in the first part of the proof.

One direction is clear: if α ≈_{P} β then certainly α ≈_{I} β. For the converse, assume α ≈_{I} β. Let (P, ≤, l) the element of P that α extends. I show that also β extends (P, ≤, l).

Since α ≈_{I} β there is a bijection f : P → ω such that β ∘ f = l and which is order-preserving when restricted to subsets of the form l^{−1}(x).

If β does not extend (P, ≤, l) there are p < q in P with f(q) < f(p). Since P is locally finite, we then also have for some p <^{d} q in P that f(q) < f(p). If g : P → ω is the unique order preserving bijection with α ∘ g = l, then since α extends (P, ≤, l), we must have g(p) < g(q). But from iii) in definition 1.3 it follows that (l(p), l(q)) cannot be in I. Therefore, contrary to our assumption, it cannot be that α ≈_{I} β.

So the operation I ↦ P_{I} is also, up to isomorphism, surjective; and that the 1-1 correspondence is monotone both ways, is obvious.

From the proof of theorem 1.4 it is clear that up to isomorphism, a complete system on X, corresponding to the independence relation I, can always be taken as the set of all locally finite partial orders (P, ≤) such that:

1. P ⊆ X × ω such that (x, j) ∈ P and i ≤ j implies (x, i) ∈ P and (x, i) ≤ (x, j) in P;

2. if (x, i) and (y, j) are incomparable in (P, ≤) then (x, y) ∈ I;

3. if (x, i) <^{d} (y, j) in P then (x, y) ∉ I.

The labelling function is always the first projection. In the sequel we shall always assume this representation, which despenses with the need to mention the labelling.

The elements of P_{I} will be called the (infinite) traces w.r.t. (X, I). An element p of (P, ≤, l) ∈ P_{I} (up to a suitable equivalence) is called an event. Note that, despite our representation of P as subset of X × ω, it is not sufficient to denote an event by (x, i); to specify an event, it is also necessary to give the partial order it is considered to be an element of. We return to this matter in section 4.

2 Topology on infinite traces

Theorem 1.4 displays every P_{I} as a quotient of X^{ω} by the equivalence relation ≈_{I}. Since X^{ω} has a natural topology, with basic opens determined by finite initial segments s ∈ X^{∗}:

U_{s} = {α ∈ X^{ω}| α = s ⋆ β for some β}

it seems therefore straightforward to give P_{I} the quotient topology, that is the largest topology making the quotient map π_{I} : X^{ω} → P_{I} continuous, and is defined by: U is open in P_{I} if and only if π_{I}^{−1}(U) is open in X^{ω}.

Proposition 2.1 i) With the topologies given, π_{I} : X^{ω} → P_{I} is an open map;

ii) the space P is not T_{1}, unless I = ∅; iii) a set U ⊆ P_{I} is open if and only if for each P ∈ U there is a finite initial

segment (↓-closed subset) P′ of P such that for all Q which contain P′ as initial segment, Q ∈ U.

Proof. As in the proof of theorem 1.4, we use the equivalence relations ∼_{I} and ≈_{I}.

i) This means that for every open U in X^{ω}, π_{I}[U] is an open subset of P_{I}. This is equivalent to: if U is open in X^{ω} then {α| ∃β ∈ U.α ≈_{I} β} is open in X^{ω}. It suffices to check this for basic opens U_{s}. But if α ≈_{I} β and β ∈ U_{s}, there is β′ ∈ U_{s} such that α ∼_{I} β′; since this ∼_{I}-equivalence only involves an initial segment of α, there is an open neighborhood V of α all of whose members are ∼_{I}-equivalent, hence ≈_{I}-equivalent, to some β′′ ∈ U_{s}.

ii) The T_{1} property means: for any two distinct points in the space, there is for either point an open set containing that point, but not the other point. This is equivalent to: for any point x, the set {x} is closed.

If I ≠ ∅, say (x, y) ∈ I, then the strings x^{ω} and yx^{ω} are not ≈_{I}-equivalent yet every basic open neighborhood of x^{ω} contains an element ≈_{I}-equivalent to yx^{ω}; so every open neighborhood of π_{I}(x^{ω}) contains π_{I}(yx^{ω}).

iii) Every finite initial segment of α gives a finite ↓-closed subset of π_{I}(α), and conversely for every finite ↓-closed subset Q of π_{I}(α) there is α′ ≈_{I} α which starts by enumerating Q.

Since P_{I} in general is not T_{1} it makes sense to look at its specialization ordering: x ≤ y if for every open set U, x ∈ U implies y ∈ U (Note that the T_{1} property is equivalent to the property that this ordering is discrete). To be precise, as defined it is only a preorder, but in the case of P_{I} it is a partial order (P_{I} is T_{0}). Given the topology on P_{I}, x ≤ y in the specialization order means that x embeds as initial segment (↓-closed subset) in y.

It turns out that this order is a CPO, but it is not algebraic (and in particular, not a Scott domain). By the way, note that the topology on P_{I} is not in general the Scott topology for its specialization order. This is easily seen at the case I = ∅: then P_{I} = X^{ω} and the specialization order is discrete, so every {x} is Scott-open; but X^{ω} is not a discrete space.

First, let us characterize compatible subsets of P_{I} and establish that P_{I} has joins of compatible subsets as well as directed joins. I find the proof below rather easier than the one given in Chapter 11 of [BT], where moreover a property of compatible subsets, namely countability, is derived and used, which is special to the case that X is finite, and irrelevant to the argument.

Lemma 2.2 A set {(P_{k}, ≤_{k})| k ∈ K} of elements of P_{I} is compatible (i.e., has an upper bound) if and only if for each k, l ∈ K:

• P_{k} ∩ P_{l} is an initial segment of both P_{k} and P_{l}, and the orders ≤_{k} and ≤_{l} coincide on P_{k} ∩ P_{l};

• for each (x, i) ∈ P_{k} \ P_{l} and (y, j) ∈ P_{l} \ P_{k}, (x, y) ∈ I.

If these conditions hold, the set {(P_{k}, ≤_{k})| k ∈ K} has a join ⋁_{k∈K}(P_{k}, ≤_{k}) in P_{I}, given by the order

( ⋃_{k∈K} P_{k}, ⋃_{k∈K} ≤_{k})

Proof. The necessity of the conditions is easy to verify. For example, if P_{k} and P_{l} are both initial segments of another element, and (x, i) ∈ P_{k} \ P_{l}, (y, j) ∈ P_{l} \ P_{k}, these elements must be incomparable in the larger poset, hence (x, y) ∈ I.

Conversely, if the conditions are met it is trivial to check that the given union is indeed a poset with the required properties, and the join of the P_{k}.

From the lemma, it is straightforward to deduce that two elements x and y of P_{I} are incompatible if and only if there are disjoint open sets U and V with x ∈ U and y ∈ V.

Now we will show that although, through lack of finite elements, P_{I} is not a Scott domain (nor is it continuous as a poset), it arises out of a subspace by a topological construction which is a direct generalization of the ideal completion construction in the theory of Scott domains. The generalization I mean is soberification. We need some definitions.(A good reference to these matters is [Joh])

In a topological space, we say that a closed set F is irreducible if whenever F ⊆ G_{1} ∪ G_{2} for closed G_{1}, G_{2}, then F ⊆ G_{1} or F ⊆ G_{2}.

A space X is called sober if every nonempty irreducible closed set is the closure of \{x\} for a unique x ∈ X, denoted \overline{\{x\}}.

The category of sober spaces is reflective in the category of all topological spaces. The reflector is called soberification. The soberification Sob(X) of a space X is the set of all nonempty irreducible closed subsets of X, topologized by: for each open a ⊆ X, there is an open

U_{a} = {F ∈ Sob(X)| F ∩ a ≠ ∅}

of Sob(X).

Every continuous poset with the Scott topology is sober, because a nonempty closed (that is, ↓-closed and closed under directed joins) subset F is irreducible if and only if {x| ∃f ∈ F.x ≪ f} is directed. Since directed joins exist and F is closed under them, it follows that F = ↓{⋁ F }, i.e. F is the closure of {⋁ F }.

In the case of a Scott domain D, consider D_{fin}, the set of finite elements of D, as a subspace of D with the Scott topology. A nonempty closed subset F of D_{fin} is irreducible if and only if it is an ideal, and therefore D = Sob(D_{fin}), which is just the ideal completion construction.

With respect to the Scott topology, the finite elements x have the property that \{x\} is open; in particular, \{x\} is open in \overline{\{x\}}. In fact one can show (see [Joh], exercise II.1.7) that if a sober space X is the soberification of a subspace X′, then X′ has to contain at least the subset

X_{D} = \{x ∈ X| \{x\} is open in \overline{\{x\}}\}

In our case, let us start by identifying (P_{I})_{D}.

Recall that, in a partial order, an antichain is a set of pairwise incomparable elements. A chain is (for us) a set of the form {c_{n}| n ∈ ω} with c_{0} < c_{1} < c_{2} < …

Lemma 2.3 Any infinite, locally finite partial order P contains a chain or an infinite antichain.

Proof. Let B be the tree of sequences ⟨s_{0}, …, s_{n}⟩ of elements of P with s_{0} a minimal element and s_{0} <^{d} s_{1} <^{d} … <^{d} s_{n}, as well as the empty sequence. Just mapping the empty sequence to any point of P, and ⟨s_{0}, …, s_{n}⟩ to s_{n} defines, by locally finiteness of P, a surjection of B onto P.

If P does not contain an infinite antichain, the tree B is finitely branching, and since P hence B is infinite, by König’s Lemma B must have an infinite branch, which gives a chain in P.

Proposition 2.4 For x ∈ P_{I}, the following are equivalent:

1. \{x\} is open in \overline{\{x\}};

2. for every chain C in x, x\↓C is finite, and x contains no infinite antichain;

3. there is no directed set Y ⊆ {x′| x′ < x} such that ⋁ Y = x

Proof. We prove 1) ⇒ 3) ⇒ 2) ⇒ 1).

1) ⇒ 3): it is obvious, by the characterization of the topology on P_{I}, that this topology is contained in the Scott topology for its specialization order. So opens are inaccessible for directed joins, and 3) is immediate from 1).

3) ⇒ 2): if x contains a chain C = c_{0} < c_{1} < c_{2} < … with x \ ↓C infinite, then {↓ (x\↓C)∪↓c_{n}| n ∈ ω} is a chain of elements of P_{I} below x with join x; and similiarly, if x contains an infinite antichain it is easy to write x as a nontrivial join of a chain of proper infinite initial segments.

2) ⇒ 1): by 2) and lemma 2.3, x contains an infinite chain C, and x \ ↓C is finite. This holds for any chain, so for every other chain D, ↓C ⊆ ↓D. So if P is the finite initial segment ↓(x \ ↓C), then every y ≤ x which contains P will be x, since also y will contain a chain. In other words, {x} = ↓x ∩ U_{P}, and {x} is open in ↓x = \overline{\{x\}}.

In our analogue of the construction of a Scott domain as soberification, we need more than just the subspace (P_{I})_{D}. At least when X is infinite and contains infinite I-cliques, there will be points x with the property that \overline{\{x\}} ∩ (P_{I})_{D} = ∅. These are, as is readily seen, those x that satisfy: for every chain C in x, ↓C contains an infinite antichain.

Let us first see that P_{I} is sober.

Theorem 2.5 P_{I} is a sober space.

Proof. Let F ⊂ P_{I} be irreducible, closed. Then if x, y ∈ F, x and y must be compatible, otherwise there exist disjoint opens U, V with x ∈ U, y ∈ V; and F = (F \ U) ∪ (F \ V).

Now the join x ∨ y of x and y must also be in F for if not, there is a finite initial segment P of x∨y such that U_{P} ∩F = ∅; letting Q = P ∩x and R = P ∩y, we find that U_{Q} ∩ U_{R} = U_{P}, so F = (F \ U_{Q}) ∪ (F \ U_{R}); contradiction.

So if F is nonempty, F is directed and since F is closed under directed joins, F is the closure of {⋁ F }.

Theorem 2.6 For every x ∈ P_{I}, ↑x is a Scott domain.

Proof. The finite elements in ↑x are the x ∨ P, P a finite X-labelled poset compatible with x. Every y ≥ x is a directed join of these.

Now we prove our soberification result, stated in abstract topological form. The application to P_{I} is obtained by letting the subspace X′ be

(P_{I})_{D} ∪ \{x ∈ P_{I}| \overline{\{x\}} ∩ (P_{I})_{D} = ∅\}

It is easy to see, using theorems 2.5 and 2.6, that the conditions of the next theorem are satisfied in this case.

Theorem 2.7 Let X be a sober space and X′ ⊂ X a subspace such that for all x ∈ X the following two conditions hold w.r.t. the specialization ordering:

1. x is a directed join of elements of X′;

2. For every y, y′ ∈ ↓x∩X′ we have: either there is a directed set X′′ ⊂ ↑y∩X′ such that y′ ≤ ⋁ X′′, or there is a directed X′′ ⊂ ↑y′ ∩ X′ with y ≤ ⋁ X′′.

Then X is the soberification of X′.

Proof. Since X is sober, X′ is a T_{0}-space and we know that Sob(X′) will be a subspace of Sob(X) ≅ X. It suffices therefore to establish a bijection between the nonempty, irreducible closed subsets of X and those of X′.

We define Sob(X) → Sob(X′) by F ↦ F ∩ X′, and Sob(X′) → Sob(X) by A ↦ \overline{A} (closure in X). We check that these maps are well-defined and each other’s inverses.

If F ∈ Sob(X) then by sobriety of X, F = \overline{\{x\}} for some x ∈ X. F ∩ X′ is certainly nonempty since ↓x ∩ X′ contains a directed subset with join x; suppose it is reducible in X′, then F ∩ X′ = (F_{1} ∩ X′) ∪ (F_{2} ∩ X′) for F_{1}, F_{2} closed in X. Let y_{1} ∈ (F_{1} ∩ X′) \ F_{2}, y_{2} ∈ (F_{2} ∩ X′) \ F_{1}. By symmetry we can assume there is directed X′′ ⊆ ↑y_{1} ∩ X′ with y_{2} ≤ ⋁ X′′. Since the F_{i} are downward closed and X′′ is directed, either X′′ ⊆ F_{1} or X′′ ⊆ F_{2}; a contradiction in both cases. So F ∩ X′ is irreducible in X′.

Conversely, if A ∈ Sob(X′) then \overline{A} is always irreducible closed in X. And always, for A closed in X′, A = \overline{A} ∩ X′.

Furthermore, if F closed in X then \overline{F ∩ X′} ⊆ F, and if moreover F is irreducible nonempty, so F = \overline{\{x\}} = ↓x, then since x = ⋁(↓x ∩ X′), x ∈ \overline{↓x ∩ X′} so F ⊆ \overline{F ∩ X′}.

In particular, if the set of labels X is finite (this is often imposed on independence structures, see [BT]), no x ∈ P_{I} can contain an infinite antichain because that implies the existence of an infinite I-clique. So then P_{I} = Sob((P_{I})_{D})

In trace semantics ([BT]) and other considerations on traces, e.g. fairness (see [Kwi]), one often considers the maximal elements of P_{I}. Again, maximality of x ∈ P_{I} can be expressed entirely in terms of the partial order x. The condition given here is similar to the one given in [Kwi].

First, we say that the level of ξ ∈ x is the maximal length of a sequence ξ_{1} <^{d} ξ_{2} <^{d} … <^{d} ξ_{n} = ξ. So the level of a minimal element is 1, and if the level of ξ is n > 1, there is η of level n − 1 with η <^{d} ξ. By locally finiteness, levels are well-defined; we write x_{i} for the set of elements of x of level i.

Again let π : x → X the labelling function.

Proposition 2.8 x is maximal in P_{I} if and only if the following conditions hold:

i) for every i ≥ 1 and for every a ∈ X such that (a, b) ∈ I for all b ∈ π[x_{i}], there is j ≥ i and ξ ∈ x_{j} such that (π(ξ), a) ∉ I;

ii) x contains no maximal element.

Proof. If condition i) doesn’t hold there is a minimal i with the property that for some a ∈ X, ∀j ≥ i∀ξ ∈ x_{j}.(π(ξ), a) ∈ I. Taking such a; now either i = 1 and we can simply add a minimal element of x with label a, unrelated to any other element of x, or i > 1 and we add likewise an element ξ with label a and put ξ > ζ for all ζ of level i − 1 for which (π(ζ), a) ∉ I By minimality of i, such ζ exist.

If condition ii) doesn’t hold, say ξ = (a, i) is a maximal element, we can put an element (a, i + 1) on top of ξ. In either case therefore, x was not maximal.

Conversely, if the conditions hold and x < y in P_{I} then x is embedded as initial segment of y, so x_{i} = y_{i} ∩ x for i ≥ 1. If ξ ∈ y \ x, ξ ∈ y_{i} then (π(ξ), π(η)) ∈ I for all η ∈ x_{i} (and note that x_{i} ≠ ∅ since x has no maximal elements) so there is j > i and ζ ∈ x_{j} with (π(ζ), π(ξ)) ∉ I. But then ξ < ζ and x was not an initial segment of y; contradiction.

3 Independence relations and group actions on X^{ω}

In this section we see that the equivalence relation ∼_{I} on X^{ω}, defined in the proof of theorem 1.4, is induced by the action of a group on that set. We study certain graphs which can be associated with this action, and connect these to traces.

Definition 3.1 The group T of twists is generated by the natural numbers, and the following relations:

• i^{2} = id for i ∈ IN;

• i · j = j · i whenever |i − j| > 1;

• (i · (i + 1))^{6} = id.

Proposition 3.2 Every independence relation I on X induces a group action μ_{I} : T × X^{ω} → X^{ω} of T on X^{ω}, such that the orbits of the action are exactly the ∼_{I}-equivalence classes in the proof of 1.4.

Proof. We define μ_{I} (writing i · α for μ_{I}(i, α) on generators by:

i · α = \{ \begin{matrix}(α(0), …, α(i + 1), α(i), α(i + 2) …) & if (α(i), α(i + 1)) ∈ I \\ α & otherwise \end{matrix}

By symmetry of I, i · (i · α) = α, so the first relation in de definition of T is respected, and similarly, for |i − j| > 1, one easily sees that i · (j · α) = j · (i · α). As to the third relation, we distinguish cases. If all of {α(i), α(i+1), α(i+2)} are pairwise dependent or all are pairwise independent, then clearly (i·(i+1))^{3}·α = α, and this also holds if two of the possible three independences hold. If only one of them is true, say (α(i), α(i + 1)) ∈ I, then (i · (i + 1))^{2} · α = α. So the third relation is respected in all cases.

It is clear that the orbits of X^{ω} under the action μ_{I} are exactly the ∼_{I}- equivalence classes.

Now we picture the action μ_{I} as an irreflexive, undirected graph, with as vertices the elements of X^{ω}, and edges labelled by the generators of T for nontrivial action: there is an edge α ^{i} β if α and β are different and β = i · α (which entails α = i · β).

Let G(X) stand for the action graph corresponding to the largest independence relation, viz. X × X \ Δ. Here there is an edge α ^{i} i · α if and only if α(i) ≠ α(i + 1). It is clear that two vertices α, β are connected by a path in this graph if and only if there are a γ and finite strings s, t of the same length such that α = s ⋆ γ, β = t ⋆ γ and s and t are permutations of each other.

We consider certain subgraphs of G(X).

Definition 3.3 A subgraph G of G(X) is called good if it is connected, and for all configurations in G(X) of the form:

j_{i}  _{i}_{j}  (|i − j| > 1)  or  [figure: i+1; i; i; i+1; i; i+1]

if α and β are in G and are vertices of such a configuration, then any minimal path in the configuration joining α and β, belongs to G.

Example. The finite subgraph

α ^{i} i · α

is good, as is

α ^{i} i · α ^{i+1} (i + 1) · i · α

but

α ^{i} i · α ^{i+1} (i + 1) · i · α ^{i} i · (i + 1) · i · α

is not, because it should have contained also the other path in the hexagon.

Note, that any connected subgraph G of G(X) determines a subset P ⊂ X ×ω and (since all vertices of G are linear orders on P) a partial order on P which is locally finite and extends the order on X × ω, restricted to P, just as in theorem 1.4; we call this partial order ⋂ G.

Theorem 3.4 G is good if and only if G is a connected component of the full subgraph of G(X) on {α| α extends ⋂ G}.

Proof. For any poset (P, ≤) with P ⊂ X × ω etc., any connected component of {α| α extends (P, ≤)} is good; this is easy. Conversely suppose G is good, α ∈ G, β extends ⋂ G and there is a path from α to β in G(X). I show that this path lies in G. By induction on the length of the path, it suffices to show this for paths of length 1.

So suppose α ^{i} β = i · α in G(X). By the fact that α extends (P, ≤) = ⋂ G, let α(i) and α(i + 1) correspond to (x, n) and (y, m) respectively. Since β also extends (P, ≤) we have that (x, n) and (y, m) are incomparable in (P, ≤), so there is γ ∈ G which enumerates (y, m) before (x, n); and since G is connected there is a path σ in G joining α and γ. At some point along σ, the crucial swap takes place. The basic possibilities are:

(x⃗aα(i)α(i + 1) …) ^{N} (x⃗α(i)aα(i + 1) …) ^{N+1} (x⃗α(i)α(i + 1)a …)_{N} (x⃗α(i + 1)α(i)a …)

in which case, by goodness of G, we also had

(x⃗aα(i)α(i + 1) …) ^{N+1} (x⃗aα(i + 1)α(i) …)

in G; or,

(x⃗α(i)α(i + 1) …) ^{M} (x⃗′α(i)α(i + 1) …) ^{N} (x⃗′α(i + 1)α(i))

with |M − N| > 1, where, similarly, we also had

(x⃗α(i)α(i + 1) …) ^{N} (x⃗α(i + 1)α(i) …)

in G.

So unless σ was already the path α ^{i} i · α , we could move the crucial swap forward.

Furthermore it follows from the proof of theorem 3.4 that for two good graphs G and G′, if G′ ⊂ G then ⋂ G′ extends ⋂ G. So an inclusion of good subgraphs of G(X) corresponds to an order-reflecting map between partially ordered sets.

This will guide our reflections in the next section, where we consider the dynamics of independence structures and the connection with Winskel’s Event Structures.

4 Independence Structures, Event Structures and an Enveloping Category

In [WN94], a mathematical analysis of various models of concurrency is carried out in terms of specific adjunctions between categories: reflections and coreflections. In this section, the results are in the same line: a category LSP is defined into which both independence structures (being sets with an independence relation, and independence-preserving maps) and event structures embed as full reflective subcategories.

The category in question is a category of labelled systems of posets (LSP’s).

Definition 4.1 A labelled system of posets (LSP) is a triple (X, P, l) where X is a set, l : X → L is a labelling function and P a collection of poset structures on subsets of X, satisfying:

• if (P, ≤) ∈ P then for all x ∈ L, l^{−1}(x) ∩ P is a linearly ordered subset of P;

• every (P, ≤) ∈ P is locally finite;

• if (P, ≤) ∈ P and Q ⊂ P is a downwards closed subset, then (Q, ≤) ∈ P.

The set P is naturally ordered by: P ⪯ Q if P is an initial segment of Q (as partial orders; I write P instead of (P, ≤) whereever possible).

Definition 4.2 Let (X, P, l) and (Y, Q, m) be LSP’s with l : X → L and m : Y → M. A map from (X, P, l) to (Y, Q, m) is a triple (F, (f_{P})_{P ∈P}, κ) where κ : L → M is a function and F : P → Q a ⪯-preserving function, and (f_{P} : P → F (P)|P ∈ P) a system of order-reflecting bijective functions such that if p ∈ P ⪯ Q, then f_{P} (p) = f_{Q}(p) ∈ F (Q), and moreover m(f_{P} (p)) = κ(l(p)).

This defines a category LSP of labelled systems of posets.

Definition 4.3 Let (X, P, l) be an LSP. An event of (X, P, l) is an element of the colimit of P, viewed as a system of posets and embeddings as initial segments. Concretely, an event is an equivalence class of pairs (p, P) with p ∈ P ∈ P, under the equivalence relation which is generated by: (p, P) ∼ (q, Q) if there is R into which both P and Q embed as initial segments, and p = q.

Given two events e_{1}, e_{2} we say that e_{1}, e_{2} are consistent if they have representatives (p, P) and (q, Q) such that P and Q have an upper bound in P w.r.t. ⪯. We write e_{1}#e_{2} (and say e_{1} and e_{2} are in conflict) if they are inconsistent. We write e_{1} ≤ e_{2} if there is p ≤ q in P, such that (p, P) and (q, P) are representatives of respectively e_{1}, e_{2}. Since the labelling map l : X → L obviously also gives a map on the set of events, we have a structure (E, ≤, #, l) where E is the set of events of (X, P, l). We call this structure Ev(X, P, l).

Proposition 4.4 Ev(X, P, l) is a labelled event structure.

Let us recall that a labelled event structure is a tuple (E, ≤, #, l) where (E, ≤) is a poset, # is a binary conflict relation which is symmetric and irreflexive and satisfies e#e′ ≤ e′′ ⇒ e#e′′; and l : E → L is a labelling map. We require that if l(e) = l(e′) and ¬(e#e′), then e ≤ e′ or e′ ≤ e holds.

A map of event structures (E, ≤, #, l : E → L) → (E′, ≤′, #′, l′ : E′ → L′) is a pair (κ : L → L′, η : E → E′) such that κ ∘ l = l′ ∘ η and:

• e′ ≤′ η(d) ⇒ ∃d′ ≤ d.e′ = η(d′)

• if e_{1}, e_{2} are consistent (i.e. not in the conflict relation) and not equal, then so are η(e_{1}) and η(e_{2}).

We have a category LES of labelled event structures. The only difference between the definition here and the one by Winskel and Nielsen is that they take the maps η partial. This is not a fundamental difference: see remark at the end of this section.

Proposition 4.5 LES is a reflective subcategory of LSP.

Proof. Given a labelled event structure (E, ≤, #, l), its configurations are the downwards closed subsets of E that are conflict-free. By D(E) we denote the set of configurations of (E, ≤, #). D(E) is ordered by inclusion which is, by definition of configuration, inclusion as initial segment.

Every P ∈ D(E) is a locally finite poset and l^{−1}(x) ∩ P is linearly ordered in P by the requirement we put on labelled event structures, so (E, D(E), l) is an LSP.

Any map η : E → E′ of event structures (we suppress reference to labels wherever irrelevant) gives, for every P ∈ D(E), an order-reflecting bijection from P to η[P], so we have in fact a functor ψ : LES → LSP.

Conversely, there is a functor ϕ : LSP → LES. On objects, ϕ(X, P, l) is the event structure Ev(X, P, l) described before. From the definition of events of an LSP, it is clear that any map of LSP’s induces a map on events, which is readily seen to be a map of labelled event structures.

There is a natural 1-1 correspondence between maps (X, P, l) → ψ(E, ≤ , #, m) of LSP’s and maps ϕ(X, P, l) → (E, ≤, #, m) of labelled event structures: every function F : P → D(E) satisfying the requirements for a map of LSP’s, induces a unique function Ev(X, P, l) → E which is a map of event structures, and vice versa; so ϕ ⊣ ψ.

Furthermore, there is a bijection Ev(ψ(E, ≤, #, l)) → E, given by the counit of the adjunction. This is, by well-known category theory, to say that ψ is full and faithful (a fact which can also easily be seen directly).

Given the adjunction, it is easy to characterize the event structures among the LSP’s:

Proposition 4.6 An LSP (X, P, l) is a labelled event structure if and only if for every conflict-free subset A of Ev(X, P, l) there is a P ∈ P such that every e ∈ A has a representative (p, P) in P.

We now turn to independence structures. The category IS has as objects pairs (L, I) where L is a set and I an independence relation on L; maps (L, I) → (L′, I′) are functions f : L → L′ such that xIx′ implies f(x)I′f(x′) for x, x′ ∈ L. In other words, IS is a category of undirected, irreflexive graphs.

Proposition 4.7 IS is a full reflective subcategory of LSP.

Proof. The functor θ : IS → LSP is defined on objects by θ(L, I) = (L × ω, A_{I}, π : L × ω → L) where A_{I} is the set of poset structures on parts of L × ω which are initial segments of elements of P_{I}, P_{I} is as in theorem 1.4, the posets regarded as subsets of L × ω. Every map f : (L, I) → (L′, I′) of independence structures gives a map f^{ω} : L^{ω} → L^{′ω} such that whenever α and β are ≈_{I}- equivalent, f^{ω}(α) and f^{ω}(β) are ≈_{I′}-equivalent; therefore there is a map F : P_{I} → P_{I′}, continuous and therefore ⪯-preserving, which gives a map A_{I} → A_{I′}.

f^{ω} : L^{ω} → L^{′ω} gives also a homomorphism between the action graphs of the respective actions of T on L^{ω} and L^{′ω}, and this homomorphism is injective on connected components. This means that for any α, f gives an order-reflecting bijection from the poset represented by α to the one represented by f^{ω}(α). I.e. we have a map of LSP’s; and therefore a functor IS →^{θ} LSP.

In the other direction, we define ζ : LSP → IS by ζ(X, P, l : X → L) = (im(l), I) where the relation I is defined by xIy if for some P ∈ P and p, q ∈ P: l(p) = x, l(q) = y and p and q are incomparable in P. This is a symmetric and irreflexive relation (because l^{−1}(x) ∩ P is linearly ordered).

Given a map (F, (f_{P})_{P} , κ) : (X, P, l) → (Y, Q, m), its ζ-image is the factorization of κ ∘ l through im(l).

Since the projection L × ω → L is surjective, clearly ζθ(L, I) = (L, I). The rest of the proof is left to the reader. Again, θ is full and faithful because the counit is an isomorphism.

Now it follows directly from lemma 2.2 and its corollary that P_{I} has directed joins, that the image of every independence structure under the embedding in LSP, satisfies the condition in proposition 4.6; therefore:

Proposition 4.8 The embedding IS → LSP factors through the embedding LES → LSP; therefore, IS is a full reflective subcategory of LES.

Proof. Only the last statement needs verification; however it is a general fact for two full reflective subcategories that if one is contained in the other, it is reflective in the other.

We can also set up an adjunction between the category LSP and the category of Mazurkiewicz trace languages, as defined in [WN94], and establish that the latter is full reflective in the former. Again, the embedding factors through LES, and we obtain essentially the result of [WN94] that Mazurkiewicz trace languages are a full reflective subcategory of labelled event structures.

Remark about bisimulation. In [JNW], the authors observe that in many structures for concurrency, standard notions of bisimulation can be derived from so-called “open maps”. These in turn can be defined in terms of a suitable path lifting property. One has to define a suitable “path category” with respect to which one then can define the open maps, and subsequently bisimulation as a span of open maps (for definitions, the reader is referred to the mentioned text).

The category LSP also has a notion of bisimulation, which restricts to the notion of strong history-preserving bisimulation for labelled event structures. There is, in this case, a very simple definition for open maps in LSP: define (X, P, l) →^{(F,(f_{P})_{P} ,κ)} (Y, Q, m) to be open iff F : P → Q is an open map of posets. A monotone map φ : (P, ≤) → (Q, ≤′) is open if for q_{1} ≤′ φ(p) ≤′ q_{2} there are p_{1} ≤ p ≤ p_{2} with φ(p_{i}) = q_{i} for i = 1, 2. We have:

Proposition 4.9 If (X, P, l) →^{(F,(f_{P})_{P} ,κ)} (Y, Q, m) is an open map, then every f_{P} : P → F (P) is an isomorphism of labelled posets.

Proposition 4.10 The open maps of LSP’s restrict on event structures to the open maps of [JNW].

Remark about partiality. As remarked before, my definitions differ from those in [WN94] only in that they take (as maps of event structures and independence structures) partial functions. This is an inessential difference, in that the basic adjunctions also exist when the maps are partial. This is left to the reader.

References

[BT] Diekert & Rozenburg (eds), The Book of Traces, World Scientific (Singapore) 1994

[Joh] P.T. Johnstone, Stone Spaces, Cambridge University Press 1982

[JNW] A. Joyal, M. Nielsen & G. Winskel, Bislimulation from open maps, BRICS Report RS-94-7, Aarhus 1994

[Kwi] Marta Kwiatkowska, Defining Process Fairness for Non-Interleaving Concurrency, LNCS 472, 1991, and: On Topological characterization of behavioral properties, in: Reed & Roscoe (eds), Topology and Category Theory in Computer Science, Clarendon (Oxford), 1991

[WN94] G. Winskel & M. Nielsen, Models of Concurrency, BRICS Report RS-94-12, Aarhus 1994

Recent Publications in the BRICS Report Series

RS-95-57 Jaap van Oosten. Topological Aspects of Traces. November 1995. 16 pp.

RS-95-56 Luca Aceto, Wan J. Fokkink, Rob J. van Glabbeek, and Anna Ing� olfsd� ottir. Axiomatizing Pre�x Iteration with Silent Steps. November 1995. 25 pp.

RS-95-55 Mogens Nielsen and Kim Sunesen. Trace Equivalence - Partially Decidable! November 1995.

RS-95-54 Nils Klarlund, Mogens Nielsen, and Kim Sunesen. Using Monadic Second-Order Logic with Finite Domains for Speci�cation and Veri�cation. November 1995.

RS-95-53 Nils Klarlund, Mogens Nielsen, and Kim Sunesen. Automated Logical Veri�cation based on Trace Abstractions. November 1995.

RS-95-52 Anton��n Ku� cera. Deciding Regularity in Process Algebras. October 1995. 42 pp.

RS-95-51 Rowan Davies. A Temporal-Logic Approach to Binding-Time Analysis. October 1995. 11 pp.

RS-95-50 Dany Breslauer. On Competitive On-Line Paging with Lookahead. September 1995. 12 pp.

RS-95-49 Mayer Goldberg. Solving Equations in the λ-Calculus using Syntactic Encapsulation. September 1995. 13 pp.

RS-95-48 Devdatt P. Dubhashi. Simple Proofs of Occupancy Tail Bounds. September 1995. 7 pp. To appear in Random Structures and Algorithms.

RS-95-47 Dany Breslauer. The Suf�x Tree of a Tree and Minimizing Sequential Transducers. September 1995. 15 pp.

RS-95-46 Dany Breslauer, Livio Colussi, and Laura Toniolo. On the Comparison Complexity of the String Pre�x-Matching Problem. August 1995. 39 pp. Appears in Leeuwen, editor, Algorithms - ESA ’94: Second Annual European Symposium proceedings, LNCS 855, 1994, pages 483�494.