Connections between a Concrete and an Abstract Model of Concurrent Systems

Eugene W. Stark^{∗}

Department of Computer Science

State University of New York at Stony Brook

Stony Brook, NY 11794 USA

Abstract

We define a concrete operational model of concurrent systems, called trace automata. For such automata, there is a natural notion of permutation equivalence of computation sequences, which holds between two computation sequences precisely when they represent two interleaved views of the “same concurrent computation.” Alternatively, permutation equivalence can be characterized in terms of a residual operation on transitions of the automaton, and many interesting properties of concurrent computations can be expressed with the help of this operation. In particular, concurrent computations, ordered by “prefix,” form a Scott domain whose structure we characterize up to isomorphism.

By axiomatizing the properties of the residual operation, we obtain a more abstract formulation of automata, which we call concurrent transition systems (CTS’s). By exploiting a correspondence between concurrent alphabets and certain CTS’s, we are able to use the rich algebraic structure of CTS’s to obtain results in trace theory. Finally, we connect CTS’s and trace automata by obtaining a characterization of those CTS’s that correspond in a natural way to trace automata, and we show how the correspondence suggests an interesting notion of morphism of trace automata.

1 Introduction

Labeled transition systems (LTS’s) have been used frequently as an operational semantics of concurrent processes. In typical formulations, an LTS is a tuple A = (E, Q, T, ∗), where E is a set of events, Q is a set of states, ∗ ∈ Q is a distinguished start state, and T ⊆ Q × E × Q is a set of transitions, which represent potential computation steps. Although useful for many applications, LTS’s are not ideally suited as a model of concurrency, since they contain no mathematical structure with which concurrency can be represented and reasoned about directly. Instead, concurrency in computations must be represented somewhat artificially by interleaving, and reasoning about concurrency requires that we make use of auxiliary information (e.g. which pairs of transitions “commute”) not explicitly formalized in the LTS model.

∗Research supported in part by NSF Grant CCR-8702247.

In an effort to get explicit concurrency information into the definition of a transition system, we might introduce a symmetric, irreflexive concurrency relation ∥ on E, and require that the transitions respect this concurrency information in a suitable sense. Although there is some flexibility in the exact sense in which concurrency is to be respected by the transitions, the end result is essentially the class of trace automata which we define below. This kind of automaton, which arises naturally in the study of trace theory [1, 11], has been the subject of investigation by Bednarczyk [2], Kwiatkowska [8], and Shields [13], and has been used by the author to study nondeterministic dataflow networks [12, 17]. The familiar mapping that takes a finite computation sequence of an automaton to the string it generates is now replaced by a monotone mapping from the prefix-ordered set of finite computation sequences to the prefix-ordered set of traces, which are equivalence classes of strings modulo a congruence relation induced by the concurrency relation.

We can actually go a bit further than this. If we regard computation sequences having the same trace as “equivalent interleaved views” of a single concurrent computation, and we factor the poset of computation sequences by this equivalence, then the trace mapping becomes an isomorphism between the resulting poset of “finite concurrent computations” and the “trace language” generated by the automaton, where the latter is viewed as a subset of the prefix-ordered set of all traces. Ideal completion of the poset of finite concurrent computations results in a Scott domain containing both finite and infinite concurrent computations. The domain of concurrent computations is much more interesting than the poset of finite computation sequences, since concurrency is reflected in the former through the existence of nontrivial upper bounds. Since our goal is to make concurrency explicit, one might argue that concurrent computations, rather than computation sequences, ought to be the main focus of attention.

One of our main results is the following characterization of the structure of the domains of concurrent computations of trace automata:

The domain of concurrent computations of a trace automaton is isomorphic to a normal subdomain U of the domain Ē of traces generated by the event set E and concurrency relation ∥, where the inclusion of U in Ē preserves prime intervals. Conversely, if U is a normal subdomain of a domain Ē of traces, such that the inclusion of U in Ē preserves prime intervals, then U is isomorphic to the domain of concurrent computations of a trace automaton.

The proof of this characterization theorem uses in an essential way the observation that equivalence of computations can be described, independently of trace theory, using the concept of a “residual operation” on computation sequences. Intuitively, taking the residual of a computation sequence γ “after” a computation sequence δ corresponds to “cancelling from γ the greatest common prefix, up to concurrency, of γ and δ.” The computation sequences γ and δ are equivalent precisely when each is completely cancelled by the other. Residuals have previously been used by Lévy [9] in the study of the λ-calculus, to define the notion of strongly equivalent reductions. The same ideas can also be applied [3, 4, 7] to the study of recursive programs and left-linear term-rewriting systems without critical pairs. In that work, residuals are used to keep track of what happens to one redex in a term while other redexes are contracted. Our use here is analogous: the residual operation allows us to keep track of what happens to one enabled transition in a system while other concurrent transitions are executed. Boudol and Castellani [5] have also exploited the use of residuals and permutation equivalence in reasoning about concurrency.

By axiomatizing the properties of a residual operation necessary to obtain the equivalence relation on computation sequences, we arrive at the definition of concurrent transition systems (CTS’s) [15, 16]. The defining axioms generate a rich algebraic theory, which we have found to be of use in the study of concurrent systems [12, 15, 17]. A suitable definition of morphism makes the class of all CTS’s into a category CTS, which has small limits, small coproducts, small filtered colimits, and is cartesian closed. Moreover, many interesting constructions on automata have universal or couniversal characterizations either in CTS or in functor categories built from it. Included among these constructions are those that extract the computational behavior of a CTS.

In this paper, we give the details of the story outlined above. Our goal is to motivate explicitly the connection, between the concrete, easily understood trace automaton model, and the more abstract concurrent transition systems which the author has described elsewhere [15, 16]. To complete this connection between abstract and concrete, we exhibit properties that characterize up to isomorphism those CTS’s that are derived from “event automata.”

2 Trace Automata

In this paper, all sets whose cardinality is left unspecified are assumed to be at most countable.

A concurrent alphabet is a set E, equipped with a symmetric, irreflexive binary relation ∥_{E}, called the concurrency relation.

A trace automaton (henceforth simply “automaton”) is a tuple A = (E, Q, T), where

• E is a concurrent alphabet, whose elements are called events. We assume that E does not contain the special symbol ϵ, called the identity event.

• Q is a set of states.

• T ⊆ Q × (E ∪ {ϵ}) × Q is a set of transitions. We usually write t : q⟶^{a}r, or just q⟶^{a}r, to denote a transition t = (q, a, r) in T.

These data are required to satisfy the following conditions:

(Identity) q⟶^{ϵ}r iff q = r.

(Disambiguation) If q⟶^{a}r and q⟶^{a}r′, then r = r′.

(Commutativity) For all states q and events a, b, if a∥_{E}b, q⟶^{a}r, and q⟶^{b}s, then for some state p there exist transitions s⟶^{a}p and r⟶^{b}p.

A trace automaton with start state is a tuple (E, Q, T, ∗), where (E, Q, T) is a trace automaton, and ∗ ∈ Q is a distinguished state.

Intuitively, if a ∈ E, then a transition q⟶^{a}r represents a potential computation step of A in which event a occurs and the state changes from q to r. Identity transitions id_{q} = (q⟶^{ϵ}q) do not represent steps of A. Rather, these transitions play a purely technical role, which will become evident when we define the notion of a “residual operation” below. We say that event a ∈ E is enabled in state q if there exists a transition q⟶^{a}r. By the disambiguation condition, if q⟶^{a}r, then r is uniquely determined by q and a. If t : q⟶^{a}r, then q is called the domain dom(t) of t and r is called the codomain cod(t) of t. Transitions t and u are called coinitial if dom(t) = dom(u).

A finite computation sequence for an automaton is a finite sequence γ of nonidentity transitions of the form:

q_{0}⟶^{a_{1}}q_{1}⟶^{a_{2}} … ⟶^{a_{n}}q_{n}.

The number n is called the length |γ| of γ. By convention, we regard an identity transition id_{q}. as identical to the computation sequence of length zero from state q. An infinite computation sequence is an infinite sequence of non-identity transitions:

q_{0}⟶^{a_{1}}q_{1}⟶^{a_{2}} ….

We extend notation and terminology for transitions to computation sequences, so that if γ is a computation sequence, then the domain dom(γ) of γ is the state q_{0}, and if γ is finite, then the codomain cod(γ) of γ is the state q_{n}. We write γ : q → r to assert that γ is a finite computation sequence with domain q and codomain r. A computation sequence γ is initial if dom(γ) is the distinguished start state ∗. If γ : q → r and δ : q′ → r′ are finite computation sequences, then γ and δ are called composable if q′ = r, and we define their composition to be the finite computation sequence γδ : q → r′, obtained by concatenating γ and δ and identifying cod(γ) with dom(δ). The operation of composition of finite computation sequences is associative, and identity transitions (computation sequences of length 0) behave as units for it. A finite computation sequence γ is a prefix of a computation sequence δ, and we write γ ≤ δ, iff there exists a computation sequence ξ with γξ = δ.

Trace automata (with start state) are nearly identical to the “forward stable asynchronous systems” of Bednarczyk [2]; the difference being that we retain his forward stability axiom (our commutativity axiom), but we omit his axiom stating that if q⟶^{a}r, r⟶^{b}s, and a∥_{E}b, then for some state p there exist transitions q⟶^{b}p and p⟶^{a}s. Although Bednarczyk seems to treat this axiom as more fundamental than forward stability, it seems overly restrictive, and we shall see that much can be done without it.

Trace automata can be used as the basis for an operational model of nondeterministic dataflow networks, which consist of a collection of concurrently and asynchronously executing processes that communicate by passing “value tokens” over named “ports.” This is done by introducing additional structure to distinguish between “input events,” “output events,” and “internal events,” and then requiring that input and output events have a specific form that reflects the port structure. We give below some of the definitions to illustrate how this is done. The reader wishing further discussion is referred to [10, 12, 15, 17].

An input/output automaton is a triple (A, X, Y), where A = (E, Q, T, ∗) is a trace automaton with start state, and X, Y are disjoint subsets of E, called the sets of input events and output events, respectively. Elements of E \ (X ∪ Y) are called internal events. The following property is required to hold:

(Receptivity) For all states q and input events a, event a is enabled in state q.

A port automaton is an input/output automaton (A, X, Y) equipped with a set V of values, a set I of input ports, and a set O of output ports, such that X = I × V, Y = O × V, and such that whenever (p, v) and (p′, v′) are events in X ∪ Y, then (p, v)∥_{E}(p′, v′) iff p = p′.

Two particularly well-behaved classes of input/output automata are the “monotone” automata and the “determinate” automata. An input/output automaton is monotone if the following additional property holds:

(Monotonicity) a∥_{E}b whenever a ∈ X and b ∈ E \ X.

Intuitively, the monotonicity property states that the arrival of input cannot disable any enabled output or internal transitions, since if b is an output event enabled in state q, and if a is an arbitrary input event, then a∥_{E}b by monotonicity, q⟶^{a}r for some r by receptivity, hence b is enabled in state r by commutativity. An automaton is determinate if it satisfies the following condition:

(Determinacy) Suppose q⟶^{b}r and q⟶^{c}s, where b and c are distinct non-input events. Then b∥_{E}c.

It can be shown [15, 16] that determinate input/output automata have functional input/output behavior.

2.1 Concurrent Computations

A partially ordered set (D, ⊑) is consistently complete if each pair of elements of D that have an upper bound, have a least upper bound. A (Scott) domain is an ωalgebraic, consistently complete CPO D = (D, ⊑, ⊥). A domain D is finitary if for all finite (=isolated=compact) elements d ∈ D the set {d′ ∈ D : d′ ⊑ d} is finite. An atom of D is a minimal non-⊥ element of D. If D and E are domains, then a monotone map f : D → E is continuous if it preserves suprema of ω-chains, strict if f(⊥_{D}) = ⊥_{E}, and additive if whenever d, d′ are consistent elements of D, then f(d), f(d′) are consistent elements of E, and f(d ⊔ d′) = f(d) ⊔ f(d′). The map f reflects consistency if whenever f(d) and f(d′) are consistent elements of E, then d and d′ are consistent elements of D.

The set of all finite and infinite initial computation sequences of a trace automaton with start state A = (E, Q, T, ∗), forms a domain when equipped with the prefix ordering ≤. This domain is of limited utility, since it does not take into account any concurrency information. However, there is a natural notion of “permutation equivalence” of computations of A, which captures the idea of “equivalent interleaved views” of the same concurrent computation. By factoring the domain of initial computation sequences by permutation equivalence we obtain a more useful and interesting domain of “concurrent computations.”

Formally, define permutation equivalence to be the least congruence ∼, respecting concatenation, on the set of finite computation sequences of A such that:

• Computation sequences q⟶^{a}r⟶^{b}p and q⟶^{b}s⟶^{a}p are ∼-related if a∥_{E}b.

Closely related to permutation equivalence is the permutation preorder relation ⊏ ∼ on finite computation sequences of A, which is defined to be the transitive closure of (≤ ∪ ∼). It is not difficult to see that γ ∼ δ iff γ ⊏ ∼ δ and δ ⊏ ∼ γ.

Permutation preorder extends in a straightforward way to infinite computation sequences as well: if γ′ and δ′ are coinitial finite or infinite computation sequences, then define γ′ ⊏ ∼ δ′ to hold iff for every finite γ ≤ γ′ there exists a finite δ ≤ δ′, such that γ ⊏ ∼ δ. We may then extend permutation equivalence to infinite computation sequences by defining γ′ ∼ δ′ iff γ′ ⊏ ∼ δ′ and δ′ ⊏ ∼ γ′.

2.1.1 Permutation Preorder and Traces

Because the concurrency in a trace automaton is completely determined by the concurrency relation on events, we can describe permutation preorder as the preorder induced by a certain mapping from computation sequences to a domain of “traces.” To state this formally, we need some basic definitions from trace theory [1, 2, 11].

Suppose E is a concurrent alphabet. Let E^{∗} denote the free monoid generated by E, then there is a least congruence ∼_{E} on E^{∗} such that a∥_{E}b implies ab ∼_{E} ba for all a, b ∈ E. The quotient E^{∗} /∼_{E} is the free partially commutative monoid generated by E, and its elements are called traces. We use ϵ to denote the monoid identity, and if x ∈ E^{∗}, then we use [x] to denote the corresponding element of E^{∗} /∼_{E}. Define the relation ⊑ on the monoid E^{∗} /∼_{E} by: [x] ⊑ [y] iff ∃[z]([x][z] = [y]). It is not difficult to show that ⊑ is a partial order, with ϵ as a least element. Let Ē denote the ideal completion of this partial order, then Ē is an algebraic CPO whose finite elements are the principal ideals generated by elements of E^{∗} /∼_{E}. We call Ē the domain of traces generated by the concurrent alphabet E. (This terminology is justified by Lemma 2.3, which shows that Ē is consistently complete, hence a domain. For the moment, we only need the fact that Ē is an algebraic CPO.) Notice that since the finite elements of Ē are in bijective correspondence with the elements of E^{∗} /∼_{E}, they inherit the monoid operation of E^{∗} /∼_{E}, with the least element of Ē as the monoid identity. In the sequel, we identify elements of E^{∗} /∼ with the corresponding finite elements of Ē.

Now, suppose

γ = q_{0}⟶^{a_{1}}q_{1}⟶^{a_{2}} …

is a finite or infinite computation sequence of an automaton A = (E, Q, T). Define the trace of γ to be the element tr(γ) = ⨆_{k≥0}[a_{1}a_{2} … a_{k}] of the domain of traces Ē. Obvious consequences of this definition are: (1) tr(id_{q}) = ϵ, (2) if γ and δ are composable finite computation sequences, then tr(γδ) = tr(γ)tr(δ), and (3) the map tr is continuous, with respect to the prefix ordering ≤ on computation sequences and the ordering ⊑ on traces.

Theorem 1 Suppose γ and δ are coinitial computation sequences. Then γ ⊏ ∼ δ holds iff tr(γ) ⊑ tr(δ).

Proof – We first prove the result for the special case that γ and δ are finite. Suppose γ ⊏ ∼ δ. Then there exists a finite sequence

γ = ξ_{0}, ξ_{1},…, ξ_{n} = δ,

such that for each k with 0 ≤ k < n, one of the following two relationships holds:

1. ξ_{k} ≤ ξ_{k+1}.

2. ξ_{k+1} is obtained from ξ_{k} by replacing a subsequence of the form q⟶^{a}r⟶^{b}p, where a∥_{E}b, by a sequence q⟶^{b}s⟶^{a}p.

In case (1), tr(ξ_{k}) ⊑ tr(ξ_{k+1}), and in case (2), tr(ξ_{k}) = tr(ξ_{k+1}). Hence tr(γ) ⊑ tr(δ) by reflexivity and transitivity of ⊑.

Conversely, suppose tr(γ) ⊑ tr(δ). Let x and y be the sequences of events appearing in γ and δ, respectively. Then [x] = tr(γ) ⊑ tr(δ) = [y], so by definition of ⊑ there exists z such that xz ∼ y. It follows that the string y can be transformed into the string xz by a finite sequence of steps in which adjacent pairs of concurrent symbols are permuted. By performing the same sequence of permutation steps starting with δ, we obtain a proof that δ ∼_{E} γξ for some computation sequence ξ.

We now extend the result to include infinite computation sequences. Suppose γ′ ⊏ ∼ δ′, where γ′ and δ′ are arbitrary. Given any finite [x] ⊑ tr(γ′), by the continuity of the map tr with respect to the prefix ordering ≤, there exists a finite γ ≤ γ′ such that [x] ⊑ tr(γ). Choose a finite δ ≤ δ′ such that γ ⊏ ∼ δ, then tr(γ) ⊑ tr(δ) by the finite case of the theorem. Thus, for each finite [x] ⊑ tr(γ′) there exists a finite [y] ⊑ tr(δ′) such that [x] ⊑ [y]. By the fact that the CPO Ē is algebraic, it follows that tr(γ′) ⊑ tr(δ′).

Conversely, suppose tr(γ′) ⊑ tr(δ′). Given a finite γ ≤ γ′, let [x] = tr(γ). Then [x] ⊑ tr(γ′) so by algebraicity of Ē we may choose a finite [y] ⊑ tr(δ′) such that [x] ⊑ [y]. By continuity of tr with respect to the prefix ordering ≤ on computation sequences, there exists a finite δ ≤ δ′ such that [y] ⊑ tr(δ). But then γ ⊏ ∼ δ by the finite case of the theorem.

2.1.2 Permutation Preorder and Residuals

The permutation preorder can also be characterized in a much different, and ultimately more useful way, using the notion of the “residual” of one finite computation sequence “after” another. Residuals, previously used for the λ-calculus and termrewriting systems [3, 4, 7, 9], have been shown in [12, 15, 16] to be extremely useful in reasoning about concurrent systems. Here, we formalize the notion of residual as a partial binary operation ↑ on finite computation sequences, such that γ ↑ δ (read γ “after” δ) is defined, and γ and δ are said to be consistent, exactly when γ and δ are coinitial finite computation sequences that could both be part of the “same concurrent computation.” In general, δ will then contain some transitions that “overlap” with γ and some transitions that are “concurrent” with γ, and the residual γ ↑ δ is defined to be what is left of γ after the part of δ that overlaps with it has been “cancelled.” The residual γ ↑ δ is undefined when γ contains some nondeterministic choice that is incompatible with a choice made in δ. In this case we say that γ and δ conflict. Observe that we distinguish between two types of choice that may be represented in an automaton: concurrent choice, in which events a, b with a∥b are both enabled in the same state q, and nondeterministic choice, in which a and b are both enabled in state q but we do not have a∥b.

We first define the residual operation for coinitial computation sequences γ : q → r and δ : q → s of length ≤ 1. There are three cases:

1. If γ = id_{q}, then γ ↑ δ = id_{s} and δ ↑ γ = δ.

2. If γ is a non-identity transition q⟶^{a}r, and δ is a non-identity transition q⟶^{a}s, then r = s by the disambiguation condition. Define γ ↑ δ = id_{s} = id_{r} = δ ↑ γ.

3. If γ is a non-identity transition q⟶^{a}r, and δ is a non-identity transition q⟶^{b}s, where a ≠ b, then γ ↑ δ and δ ↑ γ are defined iff a∥_{E}b. In this case, the commutativity property implies there must exist transitions s⟶^{a}p and r⟶^{b}p, which we take as γ ↑ δ and δ ↑ γ, respectively.

Lemma 2.1 The operation ↑ has the following properties, where γ, δ, and ξ denote computation sequences of length ≤ 1.

1. If γ ↑ δ is defined, then so is δ ↑ γ, and we have dom(γ ↑ δ) = cod(δ), dom(δ ↑ γ) = cod(γ), and cod(γ ↑ δ) = cod(δ ↑ γ).

2. For all γ : q → r, (a) id_{q} ↑ γ = id_{r}; (b) γ ↑ id_{q} = γ; and (c) γ ↑ γ = id_{r}.

3. For all coinitial γ, δ, ξ, (ξ ↑ γ) ↑ (δ ↑ γ) = (ξ ↑ δ) ↑ (γ ↑ δ), whenever either side is defined.

4. For all coinitial γ : q → r and δ : q → s, if γ ↑ δ = id_{s} and δ ↑ γ = id_{r}, then γ = δ.

Moreover, ↑ extends uniquely to an operation on finite computation sequences, in such a way that properties (1)-(3) are preserved and such that the following additional identities hold whenever either side is defined:

5. \begin{aligned}γ ↑ δξ & = & (γ ↑ δ) ↑ ξ \\ δξ ↑ γ & = & (δ ↑ γ)(ξ ↑ (γ ↑ δ)). \end{aligned}

Proof – (1), (2), and (4) are obvious from the definitions. (3) is proved by a straightforward case analysis on γ, δ, and ξ (see [12]).

The extension of ↑ to finite computation sequences is done using (5) as a recursive definition. Verification that the resulting extension has properties (1), (2), and (3) is then done by induction on the lengths of the computation sequences involved. Property (4) does not necessarily hold for the extension; for example, because if

γ = q⟶^{a}r⟶^{b}p and δ = q⟶^{b}s⟶^{a}p with a∥_{E}b, then γ ↑ δ = id_{p} = δ ↑ γ, but γ ≠ δ.

We now derive the connection between residuals and permutation preorder. If γ and δ are coinitial, then define γ ≺ ∼ δ iff γ ↑ δ is an identity.

Lemma 2.2 The relation ≺ ∼ is a preorder.

Proof – Reflexivity holds because γ ↑ γ = id_{q}, where q = cod(γ). To show transitivity, suppose γ ≺ ∼ δ and δ ≺ ∼ ξ. Then γ ↑ δ is an identity, so (γ ↑ δ) ↑ (ξ ↑ δ) is an identity. Since (γ ↑ δ) ↑ (ξ ↑ δ) = (γ ↑ ξ) ↑ (δ ↑ ξ), it follows that (γ ↑ ξ) ↑ (δ ↑ ξ) is an identity. But δ ↑ ξ is an identity because δ ≺ ∼ ξ, hence γ ↑ ξ is an identity.

Theorem 2 Suppose γ and δ are coinitial finite computation sequences. Then γ ⊏ ∼ δ iff γ ≺ ∼ δ.

Proof – Suppose γ ⊏ ∼ δ. Then there exists a finite sequence

γ = ξ_{0}, ξ_{1},…, ξ_{n} = δ,

such that for each k with 0 ≤ k < n, one of the following two relationships holds:

1. ξ_{k} ≤ ξ_{k+1}.

2. ξ_{k+1} is obtained from ξ_{k} by replacing a subsequence of the form q⟶^{a}r⟶^{b}p, where a∥_{E}b, by a sequence q⟶^{b}s⟶^{a}p.

In case (1), ξ_{k+1} = ξ_{k}ζ for some ζ, so by Lemma 2.1, ξ_{k} ↑ ξ_{k+1} = (ξ_{k} ↑ ξ_{k}) ↑ ζ, which is an identity, hence ξ_{k} ≺ ∼ ξ_{k+1}. In case (2), ξ_{k} = ζtu′ζ′ and ξ_{k+1} = ζut′ζ′, where t is the transition q⟶^{a}r, u is the transition q⟶^{b}s, t′ = t ↑ u, and u′ = u ↑ t. From this, a straightforward calculation using Lemma 2.1 shows that ξ_{k} ↑ ξ_{k+1} is an identity, so ξ_{k} ≺ ∼ ξ_{k+1}. Since ξ_{k} ≺ ∼ ξ_{k+1} both in case (1) and in case (2), the result γ ≺ ∼ δ follows by the reflexivity and transitivity of ≺ ∼.

Conversely, suppose γ ≺ ∼ δ. Let ξ = δ ↑ γ, then γ, δ, and ξ are related as depicted in Figure 1, where the sides of each small diamond are single transitions, and the apex of each small diamond is obtained by applying the residual operation to the transitions forming its base. From this diagram, we may read off a proof that γξ ∼ δ. This is done by starting with the computation sequence γξ represented by the path around the left-hand side of the large diamond, and, beginning with the

[figure: a_{1}; a_{2}; a_{n}; a′_{n}; b′′_{1}; b′_{1}; b_{1}; b_{2}; b_{m}; δ; γ; ξ = δ ↑ γ; id = γ ↑ δ]

Figure 1: Residuals and Permutation Preorder

leftmost small diamond in the diagram, successively replacing the pairs of transitions forming the left-hand sides of the small diamonds by the pairs of transitions forming the right-hand sides. For example, in the first step we would replace a_{n}b′′_{1} by b′_{1}a′_{n}. Eventually, these replacement steps transform the sequence γξ into the computation sequence represented by the path around the right-hand side of the large diamond; that is, into δ.

Having characterized permutation preorder in terms of residuals, we may now obtain a great deal of information about the structure of the set of computation sequences, under the permutation preorder. The main result is Theorem 4 below. I do not know how to prove such a strong result without using residuals.

Lemma 2.3 Suppose γ and δ are coinitial finite computation sequences. Then γ and δ have an upper bound with respect to ⊏ ∼ iff γ ↑ δ is defined. Moreover, if γ ↑ δ is defined, then γ and δ have a supremum with respect to ⊏ ∼, given by γ(δ ↑ γ) or δ(γ ↑ δ), which are permutation equivalent.

Proof – If γ and δ have an upper bound ξ with respect to ⊏ ∼, then γ ↑ ξ and (γ ↑ ξ) ↑ (δ ↑ ξ) are identities. But (γ ↑ ξ) ↑ (δ ↑ ξ) = (γ ↑ δ) ↑ (ξ ↑ δ), hence γ ↑ δ is defined.

Conversely, if γ ↑ δ is defined, then since γ ↑ γ(δ ↑ γ) = (γ ↑ γ) ↑ (δ ↑ γ) and δ ↑ γ(δ ↑ γ) = (δ ↑ γ) ↑ (δ ↑ γ), both of which are identities, it is clear that γ(δ ↑ γ) is a ⊏ ∼-upper bound of γ and δ. Suppose ξ is any ⊏ ∼-upper bound of γ and δ. Then

γ(δ ↑ γ) ↑ ξ = (γ ↑ ξ)((δ ↑ γ) ↑ (ξ ↑ γ)) = (γ ↑ ξ)((δ ↑ ξ) ↑ (γ ↑ ξ)),

which is an identity, so γ(δ ↑ γ) ⊏ ∼ ξ.

Theorem 3 Suppose A = (E, Q, T) is a trace automaton, and q ∈ Q. Then the set of permutation equivalence classes of computation sequences from state q, equipped with the partial order induced by ⊏ ∼, is a domain, whose finite elements are exactly the equivalence classes of finite computation sequences.

Proof – The set of finite computation sequences from state q is countable, and from Lemma 2.3 we know that whenever γ and δ have an upper bound with respect to ⊏ ∼, then they have a supremum with respect to ⊏ ∼. Then the ideal completion I of the preorder ⊏ ∼ is a domain whose finite elements are exactly the principal ideals. Let h be the map that takes each ⊏ ∼-equivalence class [γ] to the set h([γ]) = {δ : δ finite, δ ⊏ ∼ γ}. The set h([γ]) is obviously nonempty and downward-closed. It is also directed, because if δ ∈ h([γ]) and δ′ ∈ h([γ]), then δ and δ′ have a ⊏ ∼-supremum, which must also be in h([γ]). Thus, h([γ]) is an ideal of ⊏ ∼.

We claim that the map h is an order-isomorphism, from the partially ordered set of permutation equivalence classes of computation sequences from state q, to I. Since h takes each equivalence class [γ] with γ finite to the principal ideal generated by γ, we will then have the desired result. Obviously h satisfies h([γ]) ⊆ h([δ]) iff γ ⊏ ∼ δ. Note that h is injective, because if [γ] ≠ [δ] then either γ has a finite prefix γ′ such that γ′ ∉ h([δ]), or else δ has a finite prefix δ′ such that δ′ ∉ h([γ]). To complete the proof, we must show that h is also surjective; that is, every ⊏ ∼-ideal Γ of the set of finite computation sequences is h([γ]) for some computation sequence γ.

Suppose Γ ∈ I. We first observe that Γ is at most countable (because the set of all finite computation sequences is countable), hence has an enumeration (perhaps with repetition) δ_{0}, δ_{1},. . .. Next, we inductively construct a sequence γ_{0} ≤ γ_{1} ≤ … of elements of Γ, forming a chain under the prefix ordering, such that δ_{k} ⊏ ∼ γ_{k+1} for all k ≥ 0. For the basis step, let γ_{0} = id_{q}, which is in Γ because Γ is an ideal. For the induction step, suppose γ_{k} ∈ Γ has been defined for some k ≥ 0. Since δ_{k}, γ_{k} ∈ Γ, and Γ is directed, it follows by Lemma 2.3 that δ_{k} and γ_{k} are consistent. Define γ_{k+1} = γ_{k}(δ_{k} ↑ γ_{k}). Clearly, γ_{k} is a prefix of γ_{k+1}. Since γ_{k+1} is a ⊏ ∼-supremum of {γ_{k}, δ_{k}} ⊆ Γ, and since the ideal Γ is closed under suprema of finite subsets, it follows that γ_{k+1} ∈ Γ. Also, δ_{k} ⊏ ∼ γ_{k+1}, since δ_{k} ↑ γ_{k+1} = (δ_{k} ↑ γ_{k}) ↑ (δ_{k} ↑ γ_{k}) = id.

Let γ be the supremum of the chain γ_{0} ≤ γ_{1} ≤ … with respect to the prefix ordering. We claim that h([γ]) = Γ. Clearly, if δ ∈ Γ, then δ = δ_{k} for some k ≥ 0, hence δ ⊏ ∼ γ_{k+1}. This shows Γ ⊆ h([γ]). Conversely, if δ is a finite computation sequence with δ ⊏ ∼ γ, then δ ⊏ ∼ ξ for some finite prefix ξ of γ. But this means δ ⊏ ∼ γ_{k} for some k ≥ 0, hence h([γ]) ⊆ Γ because γ_{k} ∈ Γ and Γ is an ideal.

To proceed further, we need some additional information about the structure of the domain of traces Ē generated by a concurrent alphabet E. Define a trace domain to be a structure (D, ⊑, ⊥, ·), where (D, ⊑, ⊥) is a finitary domain with least element ⊥, and if D^{o} denotes the set of finite elements of D, then (D^{o}, ·, ⊥) is a monoid. In addition, the following are required to hold:

1. For all x, y ∈ D^{o}, we have x ⊑ y iff there exists z ∈ D^{o} with xz = y.

2. For all x, y, z ∈ D^{o}, if xy = xz then y = z.

3. For all distinct atoms a, b ∈ D, we have a, b consistent iff ab = ba, and then a ⊔ b = ab = ba.

On any trace domain D, we may define a partial binary operation \ on D^{o}, such that x \ y is defined iff x and y are consistent, and if so, then x \ y is the unique z such that yz = x ⊔ y. Obviously the domain of definition of \ is symmetric, and x = y iff x \ y = ϵ = y \ x.

Lemma 2.4 Suppose (D, ⊑, ⊥, ·) is a trace domain. Then the following identities hold for finite x, y, z, whenever either side is defined:

1. x(y ⊔ z) = xy ⊔ xz.

2. z \ xy = (z \ x) \ y.

3. xy \ z = (x \ z)(y \ (z \ x)).

Proof – Omitted.

We will prove the following lemma in Section 3.5 below.

Lemma 2.5 Suppose E is a concurrent alphabet. Then (Ē, ⊑, ϵ, ·) is a trace domain. Conversely, a structure (D, ⊑, ⊥, ·) is a trace domain iff it is isomorphic to (Ē, ⊑, ϵ, ·) for some concurrent alphabet E.

Lemma 2.6 Suppose γ and δ are coinitial finite computation sequences of a trace automaton. Then γ and δ are consistent iff tr(γ) and tr(δ) are consistent, in which case tr(γ ↑ δ) = tr(γ) \ tr(δ).

Proof – The proof is by induction on the pair of lengths (|γ|, |δ|). For the special cases: |γ| = 0 or |δ| = 0, the result is trivial. For the basis case of |γ| = |δ| = 1 we have that γ is a single transition t : q⟶^{a}r and δ is a single transition u : q⟶^{b}s, so tr(γ) = [a] and tr(δ) = [b]. Then γ and δ are consistent iff one of the following cases occurs:

1. a = b.

2. a ≠ b and a∥_{E}b.

By Lemma 2.5, traces [a] and [b] are consistent iff one of these two cases occurs. In case (1), traces [a] and [b] are equal, and tr(γ ↑ δ) = ϵ = tr(γ) \ tr(δ). In case (2),

[a] \ [b] = [a], hence tr(γ ↑ δ) = [a] = tr(γ) \ tr(δ).

For the induction step, suppose |γ| > 1 and |δ| ≥ 1. (We omit the case |γ| ≥ 1 and |δ| > 1, which is symmetric.) Then γ = ξζ, where |ξ| ≥ 1 and |ζ| ≥ 1. Suppose tr(ξ) = [x], tr(ζ) = [y], and tr(δ) = [z]. By Lemma 2.1, γ and δ are consistent iff ξ and δ are consistent and also δ ↑ ξ and ζ are consistent. If γ and δ are consistent, then

γ ↑ δ = (ξ ↑ δ)(ζ ↑ (δ ↑ ξ))
δ ↑ γ = (δ ↑ ξ) ↑ ζ.

Applying the induction hypothesis and Lemma 2.4, we see that

tr(γ ↑ δ) = (tr(ξ) ↑ tr(δ))(tr(ζ) ↑ (tr(δ) ↑ tr(ξ))) = [x][y] \ [z] = tr(γ) \ tr(δ)
tr(δ ↑ γ) = (tr(δ) ↑ tr(ξ)) ↑ tr(ζ) = [z] \ [x][y] = tr(δ) \ tr(γ).

Conversely, suppose tr(γ) and tr(δ) are consistent. Since then tr(ξ) and tr(δ) are consistent, by the induction hypothesis we know that ξ and δ are consistent, tr(δ ↑ ξ) = tr(δ) \ tr(ξ), and tr(ξ ↑ δ) = tr(ξ) \ tr(δ). Now, since tr(γ) and tr(δ) are consistent, and tr(ξ) ⊑ tr(γ), it follows that tr(γ) and tr(ξ) ⊔ tr(δ) are consistent. Moreover, tr(γ) = tr(ξ)tr(ζ) and tr(δ) ⊔ tr(ξ) = tr(ξ)(tr(δ) \ tr(ξ)), so it follows that tr(ζ) and tr(δ) \ tr(ξ) are consistent. Applying the induction hypothesis once again shows that ζ and δ \ ξ are consistent. Since ξ and δ are consistent, and δ ↑ ξ and ζ are consistent, it follows that γ and δ are consistent, as was to be shown.

A subdomain of a domain D is a subset U of D, which is a domain under the restriction of the ordering on D, and is such that the inclusion of U in D is strict and continuous. A subdomain U of D is normal if for all d ∈ D, the set {e ∈ U : e ⊑ d} is directed.

Lemma 2.7 Domain D′ is isomorphic to a normal subdomain of D iff there exists a strict, additive, continuous injection f : D′ → D that also reflects consistency.

Proof – Omitted.

An interval in a domain D is a pair (d, d′) of elements of D, with d ⊑ d′. A prime interval is an interval (d, d′) such that d ⊏ d′, and there exists no d′′ ∈ D with d ⊏ d′′ ⊏ d′.

Theorem 4 Suppose D is the domain of permutation equivalence classes of initial computation sequences of a trace automaton with start state A = (E, Q, T, ∗). Then D is isomorphic to a normal subdomain U of Ē, such that the inclusion of U in Ē preserves prime intervals. Conversely, if U is a normal subdomain of Ē, such that the inclusion of U in Ē preserves prime intervals, then U is isomorphic to the domain of permutation equivalence classes of initial computation sequences of a trace automaton with start state.

Proof – Suppose domain D is the domain of permutation equivalence classes [γ] of initial computation sequences γ of a trace automaton with start state A = (E, Q, T, ∗). Each computation sequence γ of A determines a trace tr(γ) ∈ Ē. By Lemma 2.6, if γ ⊏ ∼ δ, then tr(γ) \ tr(δ) = ϵ, so tr(γ) ⊑ tr(δ). It follows that the mapping tr from computation sequences to traces induces a monotone injection (which we also denote by tr) from D to Ē. Clearly, the map tr is strict. It also preserves prime intervals, because an interval ([γ], [δ]) in D is prime iff δ ∼ γt for some nonidentity transition t, and an interval ([x], [y]) in Ē is prime iff y ∼ xe for some e ∈ E.

To see that tr is continuous, it suffices to show that it preserves suprema of ⊏ ∼- chains. Suppose γ_{0} ⊏ ∼ γ_{1} ⊏ ∼ … is a chain with supremum γ. By a dovetailing argument using ω-algebraicity and consistent completeness, we may construct a prefix-ordered chain of finite computation sequences δ_{0} ≤ δ_{1} ≤ … with the following properties:

1. For all j ≥ 0, there exists k ≥ 0 such that δ_{j} ⊏ ∼ γ_{k}.

2. For all k ≥ 0, and all finite ξ ⊏ ∼ γ_{k}, there exists j ≥ 0 such that ξ ⊏ ∼ δ_{j}.

It follows that ⨆_{k} tr(δ_{k}) = ⨆_{k} tr(γ_{k}), and if δ is the ≤-supremum of δ_{0} ≤ δ_{1} ≤ …, then δ ∼ γ. Since it is obvious from the definition that tr is continuous with respect to the prefix ordering ≤, we may then conclude that tr(γ) = tr(δ) = ⨆_{k} tr(δ_{k}) = ⨆_{k} tr(γ_{k}).

To see that tr is additive, suppose γ and δ are consistent finite computation sequences. Then ξ = γ(δ ↑ γ) is a ⊏ ∼-supremum of γ and δ. Moreover, tr(ξ) = tr(γ)(tr(δ) \ tr(γ)) = tr(γ) ⊔ tr(δ) by Lemmas 2.4 and 2.5. Finally, if tr(γ) and tr(δ) are consistent, then γ and δ are consistent by Lemma 2.6, so tr reflects consistency. Since the map tr is a strict, additive, continuous injection that reflects consistency, it is a isomorphism from D to a normal subdomain of Ē by Lemma 2.7.

Conversely, suppose U is a normal subdomain of Ē for some concurrent alphabet E, such that the inclusion of U in Ē preserves prime intervals. Let A = (E, U^{o}, T, ϵ), where U^{o} is the set of finite elements of U, and where T contains id_{ϵ} all identity transitions id_{[x]} with [x] ∈ U^{o}, and all transitions [x]⟶^{a}[xa] where both [x] and [xa] ∈ U^{o}. It is easy to check that A satisfies the conditions for an automaton. If γ is an initial computation sequence of A, then tr(δ) is a finite element of U for each finite prefix δ of γ, so tr(γ) ∈ U by continuity of tr. Conversely, if [x] ∈ U, then we may choose a chain [x_{0}] ⊑ [x_{1}] ⊑ … of finite elements of U such that ⨆_{k}[x_{k}] = [x]. Since the inclusion of U in Ē preserves prime intervals, and the domain Ē is finitary, we may assume without loss of generality that for each k ≥ 0, either x_{k+1} = x_{k} or else x_{k+1} = x_{k}a for some a ∈ E. It is then a simple matter to construct a corresponding initial computation sequence γ of A, such that tr(γ) = [x].

It can be shown (see [14]), that a domain D is isomorphic to a normal subdomain U of a domain of traces Ē, where the inclusion of U in Ē preserves prime intervals, if and only if D is an event domain [6, 18]. Event domains, in turn, are those that are isomorphic to the domains of “configurations” of an “event structure” determined by an enabling relation and a binary conflict relation. Thus, trace automata generate the same class of domains as event structures.

3 Concurrent Transition Systems

The notion of the residual of one computation sequence after another was crucial in the results of the previous section. The properties of the residual operation that were used in the proofs can be axiomatized, and the result is concurrent transition systems [15, 16]. As we have shown in these papers and in [12, 17], many interesting properties of automata can be established from these axioms. An advantage of the more abstract, axiomatic formulation is that there is an obvious way in which concurrent transition systems can be made into a category, which we call CTS. The category CTS has a surprisingly rich structure, and categorical constructions in it and related functor categories correspond directly to many natural constructions we wish to perform on automata, including the extraction of their computational behavior. After investigating the properties of CTS, we shall see that a certain mapping from trace automata to CTS suggests an interesting way to make trace automata into a category.

An abstract automaton is a structure A = (Q, T, dom, cod, id), where

• Q is a set of states.

• T is a set of transitions.

• dom, cod : T → Q are functions that map each transition to its domain and codomain, respectively.

• id : Q → T maps each state q in Q to a distinguished identity transition id_{q} ∈ T, such that dom(id_{q}) = cod(id_{q}) = q.

Let Coin(A) denote the set of all coinitial pairs of transitions of A. A residual operation on an automaton A = (Q, T, dom, cod, id) is a partial function ↑: Coin(A) → T, such that the following conditions hold (we write t ↑ u instead of ↑ (t, u), and we read it as “t after u”):

1. If t ↑ u is defined, then so is u ↑ t, and then dom(t ↑ u) = cod(u), dom(u ↑ t) = cod(t), and cod(t ↑ u) = cod(u ↑ t).

2. For all t : q → r in T, (a) id_{q} ↑ t = id_{r}; (b) t ↑ id_{q} = t; and (c) t ↑ t = id_{r}.

3. For all coinitial t, u, v ∈ T, (v ↑ t) ↑ (u ↑ t) = (v ↑ u) ↑ (t ↑ u), whenever either side is defined.

A residual operation is extensional if it satisfies the additional condition:

4. For all coinitial transitions t, u, if t ↑ u and u ↑ t are both identities, then t = u.

A concurrent transition system (CTS) is a pair C = (A, ↑), where A is an abstract automaton and ↑ is an extensional residual operation on A. If ↑ is a residual operation, but not necessarily extensional, then C is called a pre-CTS. Coinitial transitions t, u of a pre-CTS are called consistent if t ↑ u is defined (equivalently, if u ↑ t is defined), otherwise they are called conflicting. We think of consistent transitions as representing actions that might arise in a single concurrent computation, and of conflicting transitions as representing incompatible nondeterministic choices. If t and u are consistent, then we think of t ↑ u as what remains of the transition t after the transition u has occurred.

The results of the previous section allow us to associate with each trace automaton A = (E, Q, T) a CTS C_{A} whose states, transitions, and identities are those of A, and whose residual operation is defined as in Section 2.1.2. It is also interesting to observe that a concurrent alphabet E can be viewed as the set of nonidentity transitions of a one-state CTS, such that a, b ∈ E are consistent exactly when either a = b or a∥_{E}b, and in the latter case a ↑ b = a and b ↑ a = b. We shall put this observation to good use in Section 3.5.

Suppose A = (Q, T, dom, cod, id) and A′ = (Q′, T′, dom′, cod′, id′) are automata. Then a morphism from A to A′ is a pair of maps ρ = (ρ_{o}, ρ_{a}), where ρ_{o} : Q → Q′ and ρ_{a} : T → T′, such that dom′∘ρ_{a} = ρ_{o}∘dom, cod′∘ρ_{a} = ρ_{o}∘cod, and id′∘ρ_{o} = ρ_{a}∘id. In the sequel, we will drop the notational distinction between ρ_{o} and ρ_{a}, writing simply ρ in both cases. Let Auto denote the category of automata and their morphisms.

A morphism from a pre-CTS B = (A, ↑) to a pre-CTS B′ = (A′, ↑′) is a morphism ρ : A → A′ of the underlying automata, with the following additional property:

• If t, u are consistent transitions of B, then ρ(t) and ρ(u) are consistent transitions of B′, and ρ(t ↑ u) = ρ(t) ↑′ ρ(u).

The class of all pre-CTS’s forms a category PCTS, when equipped with the CTSmorphisms as arrows. Let CTS denote the full subcategory of PCTS whose objects are the CTS’s.

The following result shows that there is a universal way to obtain a CTS from a pre-CTS.

Lemma 3.1 Suppose B is a pre-CTS. Then there exists a CTS B^{♭}, and a morphism ♭_{B} : B → B^{♭}, with the following property: if C is any CTS equipped with a morphism ρ : B → C, then there exists a unique morphism ρ^{♭} : B^{♭} → C with ρ = ρ^{♭} ∘ ♭_{B}.

Proof – Suppose B = (A, ↑). Define a binary relation ∼ on transitions of B by: t ∼ u iff t ↑ u = id and u ↑ t = id. Let A^{♭} be the automaton whose states are those of A, but whose transitions are ∼-equivalence classes [t] of transitions of A, with domain, codomain, and identities defined in the obvious way. Define ↑^{♭} by:

[t] ↑^{♭} [u] = [t ↑ u], and let B^{♭} = (A^{♭}, ↑^{♭}). Define ♭_{B} : B → B^{♭} to take each transition t of A to the corresponding ∼-equivalence class [t], which is a transition of A^{♭}. One may now verify that B^{♭} and ♭_{B} are well-defined and have the required properties.

Corollary 3.1 CTS is a reflective subcategory of PCTS.

Proof – Lemma 3.1 shows that the inclusion of CTS in PCTS has a left adjoint, whose object map takes B to B^{♭}.

There is also a universal way to lift an automaton to a CTS.

Lemma 3.2 Suppose A is an automaton. Then there exists a CTS A^{♯} = (A, ↑) with the following property: Given a CTS C′ = (A′, ↑′), every morphism ρ : A → A′ in Auto is also a morphism ρ : A^{♯} → C′ in CTS.

Proof – Given an automaton A, let t ↑ u be defined for coinitial transitions t, u of A iff either t = u or else either t or u is an identity. If t = u or t = id, then t ↑ u = id, and if u is an identity, then t ↑ u = t. Let A^{♯} = (A, ↑), then it is easy to see that A^{♯} has the required property.

Corollary 3.2 Auto is isomorphic to a coreflective subcategory of CTS.

Proof – Lemma 3.2 shows that the forgetful functor Auto : CTS → Auto has a left adjoint, whose object map takes A to A^{♯}, and which is full and faithful.

3.1 Basic Consequences of the CTS Axioms

Define a relation ⪯ on the transitions of a CTS by: t ⪯ u iff t, u are coinitial and t ↑ u = id. We say that a transition v is a join of the coinitial transitions t, u if t ⪯ v, u ⪯ v, v ↑ t = u ↑ t, and v ↑ u = t ↑ u. If t and u are composable, then we say that a transition v is a composite of t, u if t ↑ v = id and v ↑ t = u.

The following results are proved in [16]. The reader may enjoy working out the proofs, since they are good examples of how to work with residuals.

Lemma 3.3 Suppose C is a CTS.

1. The relation ⪯ is a partial order.

2. If a composite of t and u exists, then it is unique. (We denote it by tu.)

3. Suppose t and v are coinitial, and the composite tu of t and u exists.

(a) v ↑ tu = (v ↑ t) ↑ u.

(b) tu ↑ v = (t ↑ v)(u ↑ (v ↑ t)).

4. Composition obeys the following laws:

(a) For all t, t = id t = t id.

(b) i. If tu and (tu)v exist, then uv and t(uv) exist, and (tu)v = t(uv). ii. If tu, uv, and t(uv) exist, then (tu)v exists and (tu)v = t(uv).

(c) If tu and tv exist, and tu = tv, then u = v.

5. A transition v is a join of t and u iff v = t(u ↑ t). Hence a join of t and u, if it exists, is unique. (We denote it by t ∨ u.) Moreover, if t ∨ u exists, then it is the least upper bound of t and u under ⪯.

Lemma 3.4 Suppose ρ : C → C′ is a morphism. Then

1. ρ(tu) = ρ(t)ρ(u) whenever tu exists.

2. ρ(t ∨ u) = ρ(t) ∨ ρ(u) whenever t ∨ u exists.

3.2 Completion of a CTS

A CTS is called complete if every composable pair of transitions has a composite. Complete CTS’s play a fundamental role in the process of extracting the computational behavior of a CTS. In particular, each CTS C freely generates a completion C^{∗}, whose states are the same as those of C, and whose transitions are certain equivalence classes of finite sequences of transitions of C. In case C is the CTS C_{A} corresponding to a trace automaton A, then the transitions of C_{A}^{∗} are precisely the permutation equivalence classes of finite computation sequences of A.

Lemma 3.5 Suppose C is a CTS. Then there exists a complete CTS C^{∗}, and a morphism ♮_{C} : C → C^{∗}, with the following property: if C′ is any complete CTS equipped with a morphism ρ : C → C′, then there exists a unique morphism ρ^{∗} : C^{∗} → C′ such that ρ = ρ^{∗} ∘ ♮_{C}.

Proof – Suppose C = (A, ↑) is a CTS. Let A^{∗} be the automaton whose states are those of A, and whose transitions are the finite computation sequences of A, with the computation sequences of length 0 as the identity transitions. If we identify each nonidentity transition of A with the corresponding computation sequence of length 1, then the residual operation ↑ on A extends uniquely to a residual operation ↑^{∗} on A^{∗}, such that the following hold whenever either side is defined:

ξ ↑^{∗} γδ = (ξ ↑^{∗} γ) ↑^{∗} δ, γδ ↑^{∗} ξ = (γ ↑^{∗} ξ)(δ ↑^{∗} (ξ ↑^{∗} γ)).

Then B = (A^{∗}, ↑^{∗}) is a pre-CTS. Moreover, the map μ : C → B that takes each state of C to the same state of B and each nonidentity transition of C to the corresponding computation sequence of length 1, is a morphism. Define C^{∗} = B^{♭} and define ♮_{C} : C → C^{∗} by: ♮_{C} = ♭_{B} ∘ μ. One may now verify that C^{∗} and ♮_{C} have the stated properties.

Let CCTS denote the full subcategory of CTS having the complete CTS’s as objects.

Corollary 3.3 CCTS is a reflective subcategory of CTS.

Proof – Lemma 3.5 shows that the inclusion of CCTS in CTS has a left adjoint, whose object map takes C to C^{∗}.

Theorem 5 If C_{A} is the CTS associated with a trace automaton A, then up to isomorphism, C_{A}^{∗} is the CTS whose states are the states of A and whose transitions are the permutation equivalence classes of finite computation sequences of A, with residual given by Lemma 2.1.

Proof – By the construction in Lemma 3.5, C_{A}^{∗} has as states the states of A and as transitions the ∼-equivalence classes of finite computation sequences of A, where γ ∼ δ holds iff γ ↑^{∗} δ = id and δ ↑^{∗} γ = id. By Theorem 2, ∼ is nothing more than permutation equivalence.

In later sections, we need a characterization of the complete CTS’s that was proved in [16]. Define a computation category to be a small category C with the following properties:

1. Every arrow is an epimorphism.

2. The only isomorphisms are identities.

3. C has bounded pushouts: whenever t, u are coinitial arrows of C such that tv = uw for some arrows v, w, then t and u have a pushout.

For the statement of the next result, we observe that a category is nothing more than a pair (A, ·), where A is an automaton and · is an associative composition on the transitions of A, having the identities of A as units.

Lemma 3.6 Suppose C = (A, ↑) is a complete CTS, and let · denote the composition operation of C. Then C′ = (A, ·) is a computation category. Conversely, suppose C′ = (A, ·) is a computation category. For coinitial arrows t, u of A, let t ↑ u be defined iff tv = uw for some arrows v, w, in which case let t ↑ u be the side opposite t in a pushout square with t, u as its base. Then C = (A, ↑) is a complete CTS, whose composition operation coincides with that of C.

Proof – Omitted.

3.3 Computation Diagrams

In this section we generalize to CTS’s the notions of “computation tree” and “computation” for ordinary transition systems. Given a CTS C, the set of all transitions of its completion C^{∗} from a designated state ∗, forms the set of states of another complete CTS D, which we call the complete computation diagram of C with respect to ∗. Transitions of D represent prefix relationships between concurrent computations; accordingly, there is at most one transition between any two states of D.

Formally, a pointed CTS is a pair (C, ∗), where C is a CTS, and ∗ is a distinguished state of C, called the start state. Let CTS_{∗} (resp. CCTS_{∗}) denote the category of pointed CTS’s (resp. pointed, complete CTS’s) and morphisms that preserve the start state.

A complete computation diagram is a pointed CTS (D, ⊥), such that D is complete, and for each state q of D, there is a unique transition 0_{q} : ⊥ → q in D. The ⪯ partial order on transitions of D determines a corresponding ordering ⪯ on states of D, defined by: q ⪯ r iff 0_{q} ⪯ 0_{r}. Then the set of states of D, partially ordered by ⪯, has ⊥ as a least element, and by Lemma 3.6 has the property that any pair of states with an upper bound, has a least upper bound.

There is a universal way to obtain a complete computation diagram from a pointed, complete CTS.

Lemma 3.7 Suppose (C, ∗) is a pointed, complete CTS. Then there exists a complete computation diagram CDiag(C, ∗) = (D, ⊥), and a CTS_{∗}-morphism

ε : CDiag(C, ∗) → (C, ∗),

with the following property: if (D′, ⊥′) is any other complete computation diagram, equipped with a morphism ρ : (D′, ⊥′) → (C, ∗), then there exists a unique CTS_{∗}- morphism ρ† : (D′, ⊥′) → CDiag(C, ∗) such that ρ = ε ∘ ρ†.

Proof – Given (C, ∗), let D be the complete CTS whose states are all transitions t of C such that dom(t) = ∗, and in which there is a unique transition from t to u iff t ⪯ u. Let ⊥ = id_{∗}. Let ε : (D, ⊥) → (C, ∗) take each state t of D to the state cod(t) of C, and each transition from t to u in D to the transition u ↑ t in C. One may now easily check that (D, ⊥) and ε have the required properties.

Let CDiag denote the full subcategory of CTS_{∗} whose objects are the complete computation diagrams.

Theorem 6 CDiag is coreflective in CCTS_{∗}.

Proof – Lemma 3.7 shows that the inclusion of CDiag in CCTS_{∗} has a right adjoint, whose object map takes (C, ∗) to CDiag(C, ∗).

Theorem 7 Suppose (C_{A}, ∗) is the pointed CTS determined by a trace automaton A with start state, and let (D, ⊥) = CDiag(C_{A}, ∗) be its complete computation diagram. Then up to isomorphism, D is the poset of finite initial concurrent computations of A.

Proof – Obvious from Theorem 5 and the construction of CDiag(C_{A}, ∗) given in the proof of Lemma 3.7.

Noting that the domain of all computations of A may be obtained by ideal completion of the poset of finite computations, we make the following general definition:

• A computation of a pointed CTS (C, ∗) is an ideal of its complete computation diagram. A computation is finite if it is a principal ideal, otherwise it is infinite.

3.4 The Category CTS

The category CTS has a great deal of structure making it suitable for use in constructing models of concurrent systems.

Theorem 8 The category CTS:

1. has equalizers and small products, hence all small limits.

2. has small coproducts.

3. is cartesian closed.

4. has small filtered colimits.

Proof – The proofs of (1) and (2) use the obvious constructions. Assertion (3) is proved in [16].

To show (4), let D be a small filtered category, and let L : D → CTS be a functor. Our objective is to construct a colimit of L. Let V denote the set of objects of D, and let E denote the set of its arrows. For each i ∈ V, let C_{i} = (A_{i}, ↑_{i}) denote the CTS Li, where A_{i} = (Q_{i}, T_{i}, dom_{i}, cod_{i}, id_{i}). Define T to be the disjoint union ∐_{i∈V} T_{i}. Let the relation ∼ on T be defined as follows: t ∼ u iff there exist arrows f : i → k and g : j → k in D such that t ∈ T_{i}, u ∈ T_{j}, and Lf(t) = Lg(u). One may now show that ∼ is an equivalence relation, and then construct a CTS C having the equivalence classes of ∼ as its transitions. The CTS C is the base of a colimiting cone over L.

3.5 Application to Trace Theory

In this section, we show how the theory of CTS’s can be used to obtain results in trace theory. Typically, proofs in trace theory make use of the representation of traces by their “dependency graphs” [1, 11]. In contrast, proofs using CTS theory involve residuals. One of our goals is to prove Lemma 2.5, which we have already used in the proof of Theorem 4.

We first establish a correspondence between concurrent alphabets and certain CTS’s. This correspondence extends to yield a correspondence between free partially commutative monoids and certain complete CTS’s.

Lemma 3.8 Suppose E is a concurrent alphabet. Then E is the set of nonidentity transitions of a one-state CTS C_{E}, in which a ↑ b is defined for a, b ∈ E precisely when a∥_{E}b, and in that case a ↑ b = a. Conversely, suppose C is a one-state CTS in which a ↑ b = a whenever a and b are consistent, distinct, nonidentity transitions. Let E_{C} be the concurrent alphabet whose elements are the nonidentity transitions of C, with a∥_{E_{C}}b defined to hold iff a and b are consistent and distinct. Then E_{C_{E}} = E and C_{E_{C}} ≃ C.

Proof – Straightforward.

Lemma 3.9 Suppose C is a one-state complete CTS. Then x ↑ y is defined iff x and y have an upper bound with respect to the ordering ⪯. Moreover, the transitions of C, equipped with the identity and composition of C, form a monoid Mon(C) with the following properties:

1. For all x, y, z ∈ Mon(C), if xy = xz then y = z.

2. Define x ⊑ y iff ∃z(xz = y). Then ⊑ is a consistently complete partial order with the identity transition of C as a least element.

Proof – Immediate from Lemma 3.6.

From Lemma 3.9, it follows that the residual operation on C can be recovered from the monoid Mon(C), because x ↑ y is defined iff x and y have an upper bound with respect to ⊑ (which is the same relation as ⪯), in which case x ↑ y is the unique z such that yz = x ⊔ y.

Lemma 3.10 Suppose E is a concurrent alphabet. Then Mon(C_{E}) ≃ E^{∗} /∼.

Proof – The transitions of C_{E}^{∗} are permutation equivalence classes [γ] of finite computation sequences γ of C_{E}. Define a map μ from Mon(C_{E}^{∗}) to E^{∗} /∼ by: μ([γ]) = tr(γ). Note that γ is well-defined, because if [γ] = [δ], then tr(γ) = tr(δ) by Theorem 1. Also, μ is a monoid homomorphism, because μ(id) = ϵ and μ([γ][δ]) = μ([γδ]) = tr(γδ) = tr(γ)tr(δ) = μ([γ])μ([δ]). The map μ is injective, because if μ([γ]) = μ([δ]), then tr(γ) = tr(δ) hence [γ] = [δ] by Theorem 1. Finally, μ is surjective, because if [x] ∈ E^{∗} /∼, then we may construct a computation sequence γ of C_{E}, such that the sequence of events appearing in γ is x, hence such that tr(γ) = [x]. Since μ is a bijective monoid homomorphism, it is an isomorphism.

We are now equipped to prove Lemma 2.5. Proof of Lemma 2.5 – (⇒) Suppose E is a concurrent alphabet. By definition of Ē, the set Ē^{o} of finite elements of Ē is the set of elements of a monoid isomorphic to the free partially commutative monoid (E^{∗} /∼_{E}, ·, ϵ). By Lemma 3.10, this monoid is isomorphic to the monoid Mon(C_{E}^{∗}). Since the residual operation of C_{E}^{∗} can be recovered from Mon(C_{E}^{∗}) it makes sense to use this operation to reason about Mon(C_{E}^{∗}), hence about E^{∗} /∼.

Now, by Lemma 3.9, the relation ⊑ on Mon(C_{E}^{∗}) is a consistently complete partial order with ϵ as a least element. Since the ideal completion of a consistently complete partial order with a least element is a domain, it follows that Ē is a domain. We observe that Ē is finitary, because if [x] is a finite element of Ē, then |{[y] : [y] ⊑ [x]}| is bounded by the number of prefixes of permutations of x, which is finite.

Property (1) of a trace domain holds for Ē by definition of ⊑. Property (2) of a trace domain is immediate from Lemma 3.9. It remains to verify property (3) of a trace domain. The atoms of E^{∗} /∼ are precisely the ∼-equivalence classes [a] of elements a of E. Suppose [a] and [b] are distinct atoms. By Lemma 3.9, [a] and [b] are consistent iff [a] ↑ [b] is defined. But by definition of C_{E}, [a] ↑ [b] is defined for distinct [a], [b] iff a∥_{E}b, hence iff [a][b] = [b][a]. In that case, [a] ⊔ [b] = [a]([b] ↑ [a]) = [a][b] = [b][a], by definition of ↑ on C_{E}.

(⇐) Conversely, suppose (D, ⊑, ·, ⊥) is a trace domain. Define a concurrent alphabet E whose elements are the atoms of D, and which has a∥_{E}b iff a ≠ b and [a][b] = [b][a]. By property (3) of a trace domain, the monoid homomorphism that takes each element [a_{1} … a_{n}] of E^{∗} (with a_{1},…, a_{n} ∈ E) to the corresponding finite element a_{1} … a_{n} of D respects ∼, thus induces a monoid homomorphism from (E^{∗} /∼) → D^{o}, and this monoid homomorphism extends uniquely to a continuous map μ : Ē → D. Property (1) of a trace domain, together with the fact that D is finitary, implies that every element of D^{o} factors via · into a finite sequence of atoms. Thus, μ is surjective.

It remains to be shown that μ is injective. It suffices to show that μ is injective when restricted to E^{∗} /∼, since then the injectiveness of μ on all of Ē will follow by algebraicity. It is easy to see that μ(x) = ⊥ iff x = ϵ. A straightforward argument by induction on the length of a factorization into atoms shows that [x] \ [y] is defined in Ē iff μ([x]) \ μ([y]) is defined in D, and then μ([x] \ [y]) = μ([x]) \ μ([y]). Hence, μ([x]) = μ([y]) iff μ([x]) \ μ([y]) = ⊥ = μ([y]) \ μ([x]), which holds iff μ([x] \ [y]) = ϵ = μ([y] \ [x]), that is, iff [x] \ [y] = ϵ = [y] \ [x]. Thus, μ is injective, hence is an isomorphism.

The correspondence between concurrent alphabets and one-state CTS’s suggests a way to make the class of concurrent alphabets into a category. Formally, if E and F are concurrent alphabets, then define a strong morphism from E to F to be an ϵ-preserving map μ : (E ∪ {ϵ}) → (F ∪ {ϵ}), such that a∥_{E}b implies μ(a) ≠ μ(b). Let SAlph denote the category of concurrent alphabets and strong morphisms.

Lemma 3.11 The map that takes a concurrent alphabet E to the CTS C_{E} extends to an equivalence of SAlph to the full subcategory of CTS whose objects are the one-state CTS’s C such that a ↑ b = a whenever a and b are distinct consistent nonidentity transitions of C.

Proof – Omitted.

The category SAlph is not particularly interesting. However, there is another way to map concurrent alphabets to one-state CTS’s. This mapping leads to an alternative notion of “weak morphism” of concurrent alphabets. The resulting category Alph of concurrent alphabets and weak morphisms is also equivalent to a full subcategory of CTS, and is much more interesting than SAlph.

Formally, if E is a concurrent alphabet, then call a subset U of E commuting if a∥_{E}b whenever a and b are distinct elements of E. Let Com(E) denote the set of all finite commuting subsets of E. A weak morphism from E to F is a function μ : Com(E) → Com(F) such that

1. μ(∅) = ∅.

2. If U ∪ V ∈ Com(E), then μ(U) ∪ μ(V) ∈ Com(F), and μ(U \ V) = μ(U) \ μ(V).

Here the symbol \ denotes set difference. Let Alph denote the category of concurrent alphabets and weak morphisms.

A CTS C is called join-complete if every consistent coinitial pair of transitions of C has a join. The join-completion C is the sub-CTS Ĉ of C^{∗} whose transitions are precisely those transitions of C^{∗} that can be expressed as a finite join t_{1} ∨ … ∨ t_{n}, where t_{1},…, t_{n} are transitions of C.

Theorem 9 The map that takes a concurrent alphabet E to the CTS Ĉ_{E} extends to an equivalence of Alph to the full subcategory of CTS whose objects are the one-state, join-complete CTS’s C with the following properties:

1. t ↑ u = t whenever t and u are distinct, consistent, ⪯-minimal nonidentity transitions.

2. Every nonidentity transition t of C can be expressed as a join t_{1} ∨… ∨ t_{n} of a nonempty set of ⪯-minimal nonidentity transitions.

Proof – Omitted.

We do not have space here to develop in detail the features of the category Alph. We merely note that it can be shown that Alph has binary products and coproducts, which correspond to intuitively appealing notions of “concurrent product” and “nondeterministic sum,” respectively.

3.6 Characterization of Trace CTS’s

Notably absent from the CTS definition are any sort of “concreteness” axioms that would have as a consequence, for example, a theorem stating that every transition factors into a finite sequence of ⪯-minimal transitions. Part of the reason we have not included such axioms is that we can often do without them, using instead a principle of “computational induction” that arises out of the fact that C^{∗} is freely generated by C. However, another reason we have not given any concreteness axioms is that we are still looking for attractive axioms that are satisfied by the CTS’s in some subcategory of CTS with sufficient completeness properties. The axioms we have been able to discover are either too weak in the sense that the CTS’s satisfying them are not very concrete, or else they are too strong in the sense that the resulting subcategory does not admit countable products.

As an example of what we are able to do, we obtain properties that characterize the CTS’s obtained from trace automata. The result is patterned after Winskel’s characterization of the domains of configurations of event structures defined by an enabling relation and a binary conflict relation [6, 18].

Define a CTS C to be atomic if the following holds:

• t ↑ v = u ↑ v implies either t = u, t = v, or u = v, whenever t, u, and v are transitions of C, with t, v consistent and u, v consistent.

This is a very strong concreteness axiom which ensures that no nontrivial ⪯-relationships hold between transitions.

Lemma 3.12 Suppose C is an atomic CTS. If t and u are coinitial transitions of C such that t ⪯ u, then either t = u or else t = id.

Proof – If t ⪯ u, then t ↑ u = id, so t ↑ u = id ↑ u. By the atomicity property, either t = id, u = id, or t = u. But u = id implies t = u = id, so either t = id or t = u.

If C is an atomic CTS, then we may define ≡ to be the least equivalence relation on transitions of C such that t ≡ t ↑ u holds whenever t is an arbitrary transition and transition u ≠ t is a nonidentity transition consistent with t.

Theorem 10 A CTS C is isomorphic to the CTS C_{A} associated with a trace automaton A iff the following conditions hold:

1. C is atomic.

2. For all transitions t, t′ of C, if t ≡ t′ and dom(t) = dom(t′), then t = t′.

3. For all transitions t ≡ t′ and u ≡ u′, if the transitions t, u are consistent, and the transitions t′, u′ are coinitial, then t′, u′ are consistent as well.

Proof – If C_{A} is the CTS associated with a trace automaton A, then it is a straightforward application of the definition of the residual operation on A to see that C_{A} has properties (1)-(3).

Conversely, suppose C is a CTS with the stated properties. Define the events of C to be the ≡-equivalence classes [t] of nonidentity transitions t of C. Let E be the set of all events of C, with concurrency relation ∥_{E} defined as follows: [t]∥_{E}[u] iff there exist t′ ≡ t and u′ ≡ u such that t′, u′ are consistent and t′ ≠ u′. Clearly, the relation ∥_{E} is symmetric, and hypothesis (2) implies that it is irreflexive.

Define A = (E, Q, T), where T contains all transitions q⟶^{ϵ}q and all transitions q⟶^{[t]}r such that t : q → r is a nonidentity transition of C. One may now verify that A is an automaton, with A ≃ C_{A}.

The equivalence, discussed in Section 3.5, from the category Alph of concurrent alphabets and weak morphisms to a full subcategory of CTS, suggests an interesting way to make the class of trace automata into a category TrAuto.

Formally, suppose A = (E, Q, T) and A′ = (E′, Q′, T′) are trace automata. Define a morphism from A to A′ to be a pair (ρ_{e}, ρ_{s}), where ρ_{e} : E → E′ is a weak morphism of concurrent alphabets, and ρ_{s} : Q → Q′ is a function, such that the following holds:

• Suppose q⟶^{e}r ∈ T, with e ≠ ϵ. Then for every enumeration {e′_{1},…, e′_{n}} of ρ_{e}({e}), there exists a (necessarily unique) finite computation sequence

ρ_{s}(q) = r′_{0}⟶^{e′_{1}}r′_{1}⟶^{e′_{2}} … ⟶^{e′_{n}}r′_{n} = ρ_{s}(r)

of A′.

Let TrAuto denote the category of trace automata and their morphisms.

The map that takes a trace automaton A to the CTS Ĉ_{A} extends to a functor AuCts : TrAuto → CTS. This functor does not yield an equivalence with a full subcategory of CTS, because AuCts(A) does not contain sufficient information to recover the concurrent alphabet of A up to isomorphism. Nevertheless, the category TrAuto seems quite interesting, and further study of it and its relationship to CTS seems worthwhile.

4 Conclusion

We have seen that by using the notion of a concurrent alphabet to introduce concurrency information into ordinary nondeterministic transition systems, we obtain a model of concurrent computation having a great deal of algebraic structure. The essential features of this structure can be expressed nicely with the help of the notion of the residual of one transition after another. The resulting algebra of residuals can be used to obtain useful insights into the capabilities and limitations of concurrency. In particular, the characterization of the domain of concurrent computations given by Theorem 4 leads at once to interesting characterizations (see [17]) of the input/output relations that are computable by various classes of concurrent automata.

References

[1] I. J. Aalbersberg and G. Rozenberg. Theory of traces. Theoretical Computer Science, 60(1):1–82, 1988.

[2] M. Bednarczyk. Categories of Asynchronous Systems. PhD thesis, University of Sussex, October 1987.

[3] G. Berry and J.-J. Lévy. Minimal and optimal computations of recursive programs. Journal of the ACM, 26(1):148–175, January 1979.

[4] G. Boudol. Computational semantics of term rewriting systems. In M. Nivat and J. Reynolds, editors, Algebraic Methods in Semantics, pages 169–236, Cambridge University Press. 1985.

[5] G. Boudol and I. Castellani. A non-interleaving semantics for CCS based on proved transitions. Fundamenta Informaticae, XI:433–452, 1988.

[6] P.-L. Curien. Categorical Combinators, Sequential Algorithms, and Functional Programming. Research Notes in Theoretical Computer Science, Pitman, London, 1986.

[7] G. Huet. Formal structures for computation and deduction (first edition). May 1986. Unpublished manuscript. INRIA, France.

[8] M. Kwiatkowska. Categories of Asynchronous Systems. PhD thesis, University of Leicester, May 1989.

[9] J.-J. Lévy. Réductions Correctes et Optimales dans le Lambda Calcul. PhD thesis, Université Paris VII, 1978.

[10] N. A. Lynch and E. W. Stark. A proof of the Kahn principle for input/output automata. Information and Computation, 82(1):81–92, July 1989.

[11] A. Mazurkiewicz. Trace theory. In Advanced Course on Petri Nets, GMD, Bad Honnef, September 1986.

[12] P. Panangaden and E. W. Stark. Computations, residuals, and the power of indeterminacy. In Automata, Languages, and Programming, pages 439–454, Springer-Verlag. Volume 317 of Lecture Notes in Computer Science, 1988.

[13] M. W. Shields. Deterministic asynchronous automata. In Formal Methods in Programming, North-Holland. 1985.

[14] E. W. Stark. Compositional relational semantics for indeterminate dataflow networks. In Category Theory and Computer Science, pages 52–74, Springer-Verlag. Volume 389 of Lecture Notes in Computer Science, Manchester, U. K., 1989.

[15] E. W. Stark. Concurrent transition system semantics of process networks. In Fourteenth ACM Symposium on Principles of Programming Languages, pages 199–210, January 1987.

[16] E. W. Stark. Concurrent transition systems. Theoretical Computer Science, 64:221–269, 1989.

[17] E. W. Stark. On the relations computed by a class of concurrent automata. In Seventeenth Annual ACM Symposium on Principles of Programming Languages, January 1990.

[18] G. Winskel. Events in Computation. PhD thesis, University of Edinburgh, 1980.