Concurrent Transition Systems^{∗}

Eugene W. Stark State University of New York at Stony Brook Stony Brook, NY 11794

July 24, 1987

Abstract: Concurrent transition systems (CTS’s), are ordinary nondeterministic transition systems that have been equipped with additional concurrency information, specified in terms of a binary residual operation on transitions. Each CTS C freely generates a complete CTS or computation category C^{∗}, whose arrows are equivalence classes of finite computation sequences, modulo a congruence induced by the concurrency information. The categorical composition on C^{∗} induces a “prefix” partial order on its arrows, and the computations of C are conveniently defined to be the ideals of this partial order. The definition of computations as ideals has some pleasant properties, one of which is that the notion of a maximal ideal in certain circumstances can serve as a replacement for the more troublesome notion of a fair computation sequence.

To illustrate the utility of CTS’s, we use them to define and investigate a dataflow-like model of concurrent computation. The model consists of machines, which generalize the sequential machines of classical automata theory, and various operations (parallel product, input and output relabeling, and feedback) on machines that correspond to ways of combining machines into networks. Using our definition of computations as ideals, we define a natural notion of observable equivalence of machines, and show that it is the largest congruence, respecting parallel product and feedback, that does not relate two machines with distinct input/output relations. In an attempt to obtain information about the algebra of observable equivalence classes, we investigate a series of abstractions of the machine model, show that these abstractions respect the feedback operation, and characterize the homomorphic image of this operation in each case. A byproduct of our analysis is a simple characterization of a large class of processes with functional input/output behavior, and a proof that the feedback operation on such processes obeys Kahn’s fixed-point principle.

1 Introduction

Labeled transition systems have been used as an operational semantics of concurrent processes. In typical formulations [9, 8], a labeled transition system is defined to be a tuple M = (Q, q_{0}, Σ, Δ), where Q is a set of states, q_{0} is a distinguished start state, Σ is a set of events, not containing the distinguished symbol ϵ, and Δ ⊆ Q × (Σ ∪ ϵ) × Q is called the transition relation. Given such a transition system M, one can define a computation sequence of M to be a sequence of the form

q_{0}⟶^{σ_{1}}q_{1}⟶^{σ_{2}} … ⟶^{σ_{n}}q_{n},

∗This paper is a revised and expanded version of [35], which it supersedes. Some of the results presented here were reported, in an abbreviated form, in [36].

where each q_{k} is in Q, each σ_{k} is in Σ ∪ {ϵ}, and (q_{k}, σ_{k+1}, q_{k+1}) ∈ Δ for each k. The string σ_{1}σ_{2} … σ_{n} is called the trace of the computation. Here we regard the set Σ as embedded in the free monoid Σ^{∗} in the obvious way, and regard ϵ as the identity element of this monoid; thus ϵ does not appear in a trace.

Formulations of labeled transition systems similar to the preceding have been used with some success in the study of concurrent programming languages such as CCS [27] and CSP [14], especially in the case where only finite computations are of interest. However, in the study of concurrency it is desirable to consider infinite computations as well, since processes in a concurrent system (e.g. an operating system) often are intended to run forever. Interesting properties of concurrent systems (such as guaranteed service of requests) cannot be properly expressed unless infinite computations are included in the underlying semantic model.

When one attempts to extend the use of transition systems to encompass the description of processes that run forever, things no longer work as smoothly as in the finite case. If we wish to define an operation of parallel composition, for example, which takes two transition systems and yields a new transition system that corresponds to the two original transition systems running in parallel, the linear nature of computation sequences forces us to use an “interleaved step” model of concurrency. Such an approach leads immediately to the so-called “fairness problem” [31]—a distinction must be drawn between “fair” computations, in which each process takes infinitely many steps, and “unfair” computations, in which one process performs only finitely many steps while the other enjoys infinitely many steps. Unfair computations can be screened out by applying some sort of fairness predicate to computations, or some sort of scheduling mechanism can be introduced to ensure that only fair computations are generated in the first place. Both approaches are mathematically inconvenient, since they involve the use of auxiliary notions (scheduling functions or predicates) not part of the basic transition system model, and these auxiliary notions tend to be ill-behaved (e.g. non-continuous).

For some time, the author has been interested in the possibility that by somehow viewing a transition system as being or generating a category, we might eliminate some of the difficulties associated with infinite computations. The basic idea would be to try to use the notion of “commuting paths” in a category to model the the various interleaved representations of a concurrent computation. It is clear that transition systems define categories in a natural way. Given a transition system G = (Q, q_{0}, Σ, Δ), we can define a “computation category” G^{∗} whose object set is Q and which has as arrows from q to r all finite computation sequences of G that begin in state q and end in state r, with composition corresponding to concatenation of computation sequences. Infinite computation sequences with initial state q can be regarded as ideals (nonempty, downwardclosed, directed subsets) of the set G^{∗}(q, - ) of all arrows of G^{∗} with domain q, partially ordered by prefix. Now, the categories G^{∗} that result by this construction are free categories having no nontrivial commuting paths; thus we have apparently obtained little more than an insignificant restatement of the definition of computation sequence. However, from the new point of view it is interesting to ask whether some generalization of the usual notion of transition system might result in computation categories in which there are nontrivial commuting paths.

In this paper, we provide an affirmative answer to this question. We define the notion of a “concurrent transition system” (CTS), which consists of a (directed, multi-)graph, whose objects (nodes) are states and whose arrows (arcs) are transitions, which has been equipped with some additional concurrency information. Although not categories themselves, each CTS C freely generates a “complete CTS” or “computation category,” C^{∗} whose states (objects) are the same as those of C, and whose arrows (transitions) are equivalence classes of finite computation sequences of C. Each equivalence class can be thought of as the set of all interleaved views of a single underlying concurrent computation. The “prefix” relation induced by the categorical composition partially orders the set of arrows of the computation category. We define the “computations” of C, from start state q_{0}, to be the ideals of the set C^{∗}(q_{0},-) of all arrows of C^{∗} with domain q_{0}, partially ordered by prefix. It follows from the ideal construction that the set of all computations from initial state q is an algebraic directed-complete partial order.

The main body of this paper is organized as follows: In Section 2, we define concurrent transition systems, give some examples, and derive some basic properties of CTS’s and the category CTS in which they live. We establish the existence of the computation categories discussed above, and also of related structures called “computation diagrams,” which generalize the familiar notion of “computation tree” for ordinary nondeterministic transition systems.

In Section 3, the theory developed in Section 2 is used to define a dataflow-like model of concurrent computation. The basic objects of the model are “machines,” which are a CTS generalization of the sequential machines of classical automata theory. We define some operations (parallel product, input and output relabeling, and feedback) on machines that correspond to various ways of composing machines into networks. We define a natural notion of “observable equivalence” of machines, and show that it is the largest congruence on machines, respecting parallel product and feedback, that does not relate machines having distinct input/output relations. The “full abstraction problem” is defined as the problem of characterizing the structure of the quotient algebra of machines, modulo observable equivalence.

In Section 4, we perform a rather extensive analysis of the feedback operation, with the dual aims, of showing that our model is a reasonable one, and of attempting to make progress on the full abstraction problem. We define a sequence of abstraction mappings that starts with machines and ends with input/output relations. For each mapping, we prove a theorem that shows that the mapping is homomorphic with respect to the feedback operation. (The mapping to input/output relations is homomorphic only for the subclass of “Kahn” machines, which have continuous functions as their input/output behaviors.) Since some of the structures at the intermediate stages between machines and input/output relations are similar to models of concurrent processes that have been proposed in the literature, our analysis yields useful information about the relationships between these models.

In Section 5 we summarize what we have accomplished, discuss how our work is related to that of other authors, and mention possibilities for future research.

We assume that the reader is familiar with the basic notions of category theory. The necessary background can be found in [23, 2, 13]. We also assume some familiarity with the theory of algebraic directed-complete partial orders, as used in denotational semantics. Reference [11] provides background on this topic.

2 Concurrent Transition Systems

In this section, we define concurrent transition systems and derive some of their basic properties.

A graph is a tuple G = (O, A, dom, cod), where O is a set of objects, A is a set of arrows, and dom, cod are functions from A to O, which map each arrow to its domain and codomain, respectively. Arrows t, u of G are called composable if cod(t) = dom(u) and coinitial if dom(t) = dom(u). Let Coin(G) denote the set of all coinitial pairs of arrows of G.

If G = (O, A, dom, cod) is a graph, then define the augmented graph G^{♯} = (O^{♯}, A^{♯}, dom^{♯}, cod^{♯}) to be the extension of G defined by: O^{♯} = O ∪ {Ω}, A^{♯} = A ∪ {ω_{q} : q ∈ O^{♯}}, dom^{♯}(ω_{q}) = q, and cod^{♯}(ω_{q}) = Ω, where Ω is a new object not in O, and for each q ∈ O^{♯}, ω_{q} is a distinct new arrow not in A.

A concurrent transition system (CTS) is a structure (G, id, ↑), where

• G = (O, A, dom, cod) is a graph, called the underlying graph. The elements of O^{♯} (resp. O) are called (resp. proper) states and the elements of A^{♯} (resp. A) are called (resp. proper) transitions.

• id : O^{♯} → A^{♯} maps each q ∈ O^{♯} to a distinguished identity transition id_{q}.

• ↑: Coin(G^{♯}) → A^{♯} is a function, called the residual operation. We write t ↑ u (read t “after” u) for ↑ (t, u).

These data are required to have the following properties:

1. For all q ∈ O^{♯}, and all coinitial t, u ∈ A^{♯},

(a) dom^{♯}(id_{q}) = cod^{♯}(id_{q}) = q;

(b) dom^{♯}(t ↑ u) = cod^{♯}(u), and

(c) cod^{♯}(t ↑ u) = cod^{♯}(u ↑ t).

2. For all t : q → r in A^{♯},

(a) id_{q} ↑ t = id_{r};

(b) t ↑ id_{q} = t; and

(c) t ↑ t = id_{r}.

3. For all coinitial t, u ∈ A^{♯}, if t ↑ u and u ↑ t are both identities, then t = u.

4. For all coinitial t, u, v ∈ A^{♯}, (v ↑ t) ↑ (u ↑ t) = (v ↑ u) ↑ (t ↑ u).

Axiom (4) can be visualized as shown in Figure 1.

In the sequel, we will drop the ♯ from dom^{♯} and cod^{♯}. Note that it automatically follows from the definition of a CTS that ω_{q} ↑ t = ω_{r} and t ↑ ω_{q} = ω_{Ω} = id_{Ω} for all transitions t : q → r, since for each q, the transition ω_{q} is the only transition with domain q and codomain Ω. Note also that states are actually not logically necessary in the definition of CTS, since they are in bijective correspondence with the set of identity transitions. We shall occasionally take advantage of this fact to give concise specifications of particular CTS’s.

Coinitial transitions t, u of a CTS are called consistent if t ↑ u is a proper transition (equivalently, if u ↑ t is proper), otherwise they are called conflicting. A coinitial set of transitions is called consistent if it is pairwise consistent. In defining the operation ↑ for a CTS, we need only specify which coinitial pairs of proper transitions are consistent, and to give the definition of ↑ for such pairs, since the remaining cases are fixed by the CTS axioms.

A CTS is called determinate if every coinitial pair of proper transitions is consistent. A CTS is called complete if to every composable pair t, u of transitions there corresponds a transition v, called a composite of t and u, such that t ↑ v = id_{cod(v)} and v ↑ t = u.

[figure: u; v; t; u ↑ t; v ↑ u; t ↑ u; v ↑ t; (v ↑ t) ↑ (u ↑ t); = (v ↑ u) ↑ (t ↑ u)]

Figure 1: CTS Axiom (4)

Example 1 – CTS’s From Graphs

Every graph G lifts to a CTS Cts(G) in a “minimally consistent” way. More precisely, suppose G = (O, A, dom, cod). Let G′ = (O, A′, dom′, cod′) be defined so that A′ = A ⊎ {id_{q} : q ∈ O}, and dom′(id_{q}) = cod′(id_{q}) = q for all q ∈ O. Let ↑ be defined as follows:

t ↑ u = \{ \begin{matrix}t, & if u = id_{dom(t)} \\ id_{cod(u)}, & if t = u or t = id_{dom(t)} \\ ω_{cod(u)}, & otherwise. \end{matrix}

It is easily verified that C = (G′, id, ↑) is a CTS. Moreover, assuming an appropriate definition (provided in Section 2.2) of “CTS-morphism,” it can be shown that the map Cts is the object map of a functor, left-adjoint to the forgetful functor taking each CTS to its underlying graph.

Example 2 – Trace Algebras A trace algebra is a monoid X such that:

1. For all t, u, v ∈ X, if tu = tv, then u = v.

2. If ⪯ is the prefix relation induced by the monoid operation (i.e. t ⪯ u iff ∃v(tv = u)), then ⪯ is a partial order with respect to which each pair t, u with an upper bound has a least upper bound t ∨ u.

The elements of a trace algebra are called traces.

One class of examples of trace algebras are those obtained from “concurrent alphabets” [26]. Formally, a concurrent alphabet is a pair (Σ, ∥), where Σ is a set and ∥ is an irreflexive, symmetric relation on Σ, called a concurrency relation. The concurrency relation induces a congruence ∼ on the free monoid Σ^{∗}, such that two strings are congruent iff one can be transformed into the other by a finite sequence of steps in which pairs of adjacent concurrent symbols are permuted. The monoid Σ^{∗}/ ∼ is a trace algebra.

From a trace algebra X, we can construct a CTS C with one proper state, having the elements of X as its proper transitions, and in which the monoid identity ϵ is regarded as the single proper identity transition. If t, u is a pair of proper transitions of C (i.e. elements of X), then we define t and u to be consistent if they have a least upper bound t ∨ u as elements of X. For such a pair, we define t ↑ u to be the unique element of X with the property u(t ↑ u) = t ∨ u. It is straightforward to check that the CTS axioms are satisfied by these definitions. Moreover, the CTS C is complete, since the monoid operation yields, for each pair t, u of transitions, a transition tu with the properties t ↑ tu = ϵ and tu ↑ t = u.

Example 3 - CTS’s From Petri Nets

In [38] a “net” is defined to be a bipartite directed graph N = (B, E; F), where the set of nodes B ∪ E is partitioned into a set E of events and a set B of conditions, and the relation F ⊆ (B ×E)∪(E ×B), is called the flow relation. A case of N is a set of conditions. For each event e ∈ E, the set pre(e) of preconditions of e is the set of all b ∈ B such that (b, e) ∈ F, and the set post(e) of postconditions of e is the set of all b ∈ B such that (e, b) ∈ F. A set u of events is called independent if for each pair e_{1}, e_{2} of elements of u, the sets pre(e_{1}) ∪ post(e_{1}) and pre(e_{2}) ∪ post(e_{2}) are disjoint.

The transition relation of N is the set of all triples (c, u, c′), where c and c′ are cases of N, and u is an independent set of events of N such that:

1. For all e ∈ u, pre(e) ⊆ c.

2. For all e ∈ u, post(e) ∩ c = ∅.

3. The case c′ is obtained from c by removing all preconditions of events in u, and then adding all postconditions of events in u.

We now obtain a CTS from N as follows: Take as states the cases of N. Take as proper transitions the elements of the transition relation of N, defining dom(c, u, c′) = c and cod(c, u, c′) = c′, and regarding the transitions (c, ∅, c) as identities. Define coinitial pairs (c, u, d) and (c, v, d′) of proper transitions to be consistent iff u ∪ v is independent. For such pairs, define

(c, u, d) ↑ (c, v, d′) = (d′, u\v, e),

where e is obtained from d′ by removing all preconditions of events in u\v and then adding all postconditions of events in u\v. That these definitions satisfy the CTS axioms is easily checked.

Example 4 - CTS’s From λ-Calculus

Let Λ be the set of terms of the pure λ-calculus [4], and let → denote reduction with respect to rule (β). If C is a set of redexes in a term q, then a derivation relative to C is a derivation q = q_{0} → q_{1} → … → q_{n}, in which the redex contracted at each step is either in C or is a residual (in Church’s original sense) of a redex in C. A derivation relative to C is complete if the set of residuals of C in q_{n} is empty. Given a set C of redexes in a term q, it can be shown that there is a fixed upper bound on the length of a derivation from q relative to C, and that all complete derivations from q relative to C result in the same term. It therefore makes sense to write q⟶^{C}r, if C is a set of redexes in q and any complete derivation relative to C results in r. Let us call such triples q⟶^{C}r transitions. Suppose t is a transition q⟶^{C}r and u is a transition q⟶^{D}s. It can be shown that the same set C/d of residuals of redexes in C is obtained for all complete derivations

[figure: v; t; u; t ↑ v; v ↑ t; u ↑ (v ↑ t); (v ↑ t) ↑ u] Figure 2:

d relative to D. Let C/D denote this set. It therefore makes sense to define the residual t/u of

transition t with respect to u to be the transition s⟶^{C/D}p, where p is the unique result of a complete derivation from s relative to C/D.

We now define a CTS whose state set is Λ, and whose transitions are all transitions t as defined above. The domain dom(t) of a transition t : q⟶^{C}r is the term q and the codomain cod(t) of t is the term r. The identity transitions are those of the form q⟶^{∅}q, all coinitial pairs of proper transitions are consistent, and we define and we define t ↑ u = t/u.

That the above definitions satisfy the CTS axioms follows from results of Lèvy [22, 5]. A similar construction can be used to obtain CTS’s from left-linear term-rewriting systems without critical pairs [15].

2.1 Consequences of the Axioms

Define a relation ⪯ on the transitions of a CTS by: t ⪯ u iff t, u are coinitial and t ↑ u = id_{cod(u)}. We call ⪯ the prefix relation.

Lemma 2.1.1 The prefix relation is a partial order.

Proof – Reflexivity holds because t ↑ t = id_{cod(t)} by axiom (2c).

To show transitivity, suppose t ⪯ u and u ⪯ v. Then t ↑ u is an identity, so (t ↑ u) ↑ (v ↑ u) is an identity by axiom (2a). Since (t ↑ u) ↑ (v ↑ u) = (t ↑ v) ↑ (u ↑ v) by axiom (4), it follows that (t ↑ v) ↑ (u ↑ v) is an identity. But (u ↑ v) is an identity because u ⪯ v, hence t ↑ v is an identity by axiom (2b).

Finally, ⪯ is antisymmetric because if t ⪯ u and u ⪯ t, then t ↑ u and u ↑ t are identities, hence t = u by axiom (3).

Lemma 2.1.2 If a composite of t and u exists, then it is unique.

Proof – Suppose v and v′ are composites of t and u. Then t ↑ v′ is an identity, so v ↑ v′ = (v ↑ v′) ↑ (t ↑ v′) by axiom (2b). By axiom (4), this is equal to (v ↑ t) ↑ (v′ ↑ t) = u ↑ u, which is an identity by axiom (2c). A symmetric argument shows that v′ ↑ v is an identity, so v = v′ by axiom (3).

We use tu to denote the composite of t and u, when it exists.

Lemma 2.1.3 Suppose t and v are coinitial, and the composite tu of t and u exists. Then

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

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

Proof – (See Figure 2.)

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

(2) Since (t ↑ v) ↑ (tu ↑ v) = (t ↑ tu) ↑ (v ↑ tu), which is an identity, and (tu ↑ v) ↑ (t ↑ v) = (tu ↑ t) ↑ (v ↑ t) = u ↑ (v ↑ t), the result follows.

Lemma 2.1.4 Composition obeys the following laws:

1. For all t, t = id_{dom(t)}t = t id_{cod(t)}.

2. (a) If tu and (tu)v exist, then uv and t(uv) exist, and (tu)v = t(uv).

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

3. If tu and tv exist, and tu = tv, then u = v.

Proof – (1) follows directly from the definition of composite.

To show (2a), suppose tu and (tu)v exist. Then by Lemma 2.1.3, (tu)v ↑ t = (tu ↑ t)(v ↑ (t ↑ tu)). But tu ↑ t = u and t ↑ tu is an identity, so (tu)v ↑ t = uv. Since by Lemma 2.1.3, t ↑ (tu)v = (t ↑ tu) ↑ v, which is an identity, it follows that (tu)v = t(uv).

To show (2b), suppose tu, uv and t(uv) exist. By Lemma 2.1.3,

t(uv) ↑ tu = (t ↑ tu)(uv ↑ (tu ↑ t)),

which is just v. Also,

tu ↑ t(uv) = (t ↑ t(uv))(u ↑ (t(uv) ↑ t)),

which is an identity, so t(uv) = (tu)v.

For (3), suppose tu = tv, so that tu ↑ tv and tv ↑ tu are identities. Then u ↑ v = (tu ↑ t) ↑ (tv ↑ t) = (tu ↑ tv) ↑ (t ↑ tv), which is an identity. Similarly, v ↑ u is an identity, so u = v.

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.

Lemma 2.1.5 A transition v is a join of t and u iff v = t(u ↑ t).

Proof – If v is a join of t and u, then t ↑ v is an identity and v ↑ t = u ↑ t, so v = t(u ↑ t). Conversely, if v = t(u ↑ t), then t ⪯ v, v ↑ t = u ↑ t, u ↑ v = (u ↑ t) ↑ (u ↑ t), which is an identity, so u ⪯ v, and v ↑ u = (t ↑ u)((u ↑ t) ↑ (u ↑ t)) = (t ↑ u). Hence v is a join of t and u.

It follows from the preceding lemma and the uniqueness of composites that a join of t and u, when it exists, is unique, and we denote it by t ∨ u. Moreover, if t ∨ u exists, then we have the equality t(u ↑ t) = t ∨ u = u(t ↑ u).

Lemma 2.1.6 Suppose t ∨ u exists. Then t ∨ u is the least upper bound of t and u under ⪯.

Proof – By definition, t ∨ u is an upper bound of t and u under ⪯. Suppose l is any upper bound of t and u. Let v = l ↑ t and w = l ↑ u, so that tv = l = uw. Now, (u ↑ t) ↑ v = (u ↑ t) ↑ (tv ↑ t) = (u ↑ tv) ↑ (t ↑ tv) = (u ↑ uw) ↑ (t ↑ tv), which is an identity, so u ↑ t ⪯ v. Let m = v ↑ (u ↑ t), so that v = (u ↑ t)m. It then follows that l = tv = t(u ↑ t)m = (t ∨ u)m, so that (t ∨ u) ⪯ l.

2.2 The Category CTS

If G = (O, A, dom, cod) and G′ = (O′, A′, dom′, cod′) are graphs, then a graph morphism from G to G′ is a pair of maps ρ = (ρ_{o}, ρ_{a}), where ρ_{o} : O → O′ and ρ_{a} : A → A′, such that dom′ ∘ρ_{a} = ρ_{o} ∘dom and cod′ ∘ ρ_{a} = ρ_{o} ∘ cod. In the sequel, we will drop the notational distinction between ρ_{o} and ρ_{a}, writing simply ρ in both cases.

A CTS-morphism from a CTS C = (G, id, ↑) to a CTS C′ = (G′, id′, ↑′) is a graph morphism ρ : G → G′, with the following properties:

1. For all proper states q of C, ρ(id_{q}) = id′_{ρ(q)}.

2. If t, u are consistent proper transitions of C, then ρ(t ↑ u) = ρ(t) ↑′ ρ(u).

It will be useful to think of a morphism ρ : C → C′ as extended to all states and transitions of C (not just the proper ones), according to the definitions ρ(Ω) = Ω, and ρ(ω_{q}) = ω_{ρ(q)}. The set of all CTS’s forms a category CTS, when equipped with the CTS-morphisms as arrows.

In the sequel, the term “morphism” will mean “CTS-morphism,” unless otherwise specified.

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

1. ρ(tu) = ρ(t)ρ(u) whenever tu exists and is a proper transition.

2. ρ(t ∨ u) = ρ(t) ∨ ρ(u) whenever t ∨ u exists and is a proper transition.

Proof – (1) Since t and tu are consistent, ρ(t) ↑ ρ(tu) = ρ(t ↑ tu), which is an identity. Also, ρ(tu) ↑ ρ(t) = ρ(tu ↑ t) = ρ(u), so ρ(tu) = ρ(t)ρ(u).

(2) If t ∨ u exists and is a proper transition, then t and u are consistent, hence t and t ∨ u are consistent. Thus, ρ(t ∨ u) ↑ ρ(t) = ρ((t ∨ u) ↑ t) = ρ(u ↑ t) = ρ(u) ↑ ρ(t). Also, ρ(t) ↑ ρ(t ∨ u) = ρ(t ↑ (t ∨ u)), which is an identity. Symmetric reasoning shows that ρ(t ∨ u) ↑ ρ(u) = ρ(t) ↑ ρ(u) and ρ(u) ↑ ρ(t ∨ u) is an identity. It follows that ρ(t ∨ u) = ρ(t) ∨ ρ(u).

Lemma 2.2.2 The forgetful functor from CTS to Graph that takes each CTS C to its underlying graph has a left adjoint, whose object map takes each graph G to the corresponding “minimally consistent” CTS Cts(G).

Proof – Straightforward.

Note that since the forgetful functor from CTS to Graph is a right adjoint, and hence preserves limits, from the previous lemma we know that any limits existing in CTS must be lifted from corresponding limits in Graph. In fact, we have:

Theorem 2.1 The following constructions in Graph lift to CTS:

1. Small limits.

2. Small coproducts.

Proof – (1) It suffices to show that small products and equalizers of pairs of morphisms lift from Graph to CTS, since a standard category-theoretic result (see, e.g. [23], p. 109) states that the existence of small products and equalizers of pairs of morphisms implies the existence of all small limits. The obvious constructions work in each case.

(2) The obvious construction works.

We do not know whether coequalizers of all pairs of morphisms exist in CTS. However, we can prove a somewhat weaker result, and the quotient construction it requires will be of use in Section 2.3.

Suppose C is a CTS. A strong congruence on C is an equivalence relation ∼ on the set of proper transitions of C, such that

1. For all transitions t, t′, u, u′ of C, if t ∼ t′, u ∼ u′, and t, u are consistent, then t′, u′ are consistent, and t ↑ u ∼ t′ ↑ u′.

2. For all coinitial transitions t, u of C, if t ↑ u and u ↑ t are both ∼-related to identities, then t ∼ u.

Since the defining properties of a strong congruence are evidently closure properties, it follows that every binary relation on the transitions of a CTS C is contained in a least strong congruence on C.

If ∼ is a strong congruence on C, then we may form the quotient CTS C/ ∼ as follows:

• Take the proper states of C as the proper states of C/ ∼.

• Define the proper transitions of C/ ∼ to be the ∼-equivalence classes. We write [t] for the equivalence class of t, and we define the identities of C/ ∼ to be the equivalence classes of identities of C. Define dom([t]) = dom(t) and cod([t]) = cod(t).

• Define [t], [u] to be consistent iff t, u are consistent, in which case we define [t] ↑ [u] = [t ↑ u].

It is easily shown, using the properties of a strong congruence, these definitions are independent of the choice of t and u. It is also straightforward to check that C/ ∼ satisfies the CTS axioms.

A strong morphism is a morphism ρ : C → D such that for all transitions t, t′, u of C, if t, u are consistent and ρ(t) = ρ(t′), then t′, u are consistent. The quotient map from C to C/ ∼ is the function η that takes each transition t of C to its ∼-equivalence class [t]. It is clear that η is a strong morphism.

Theorem 2.2 Suppose C is a CTS, and R is a binary relation on the transitions of C. Let ∼ be the least strong congruence on C that contains R, and let η : C → C/ ∼ be the quotient map. Then for each strong morphism ρ : C → D, with the property that tRu implies ρ(t) = ρ(u) for all transitions t, u of C, there exists a unique morphism σ : (C/ ∼) → D, such that ρ = σ ∘ η.

Proof – Straightforward.

A CTS with start state is a pair (C, ι), where C is a CTS, and ι : 1 → C is a morphism, called the start state map, from the terminal object 1 of CTS to C. The start state of (C, ι) is the image under ι of the single proper state of 1. If (C, ι) and (C′, ι′) are CTS’s with start state, then a morphism from (C, ι) to (C′, ι′) is a morphism ρ : C → C′ such that ρ ∘ ι = ι′. Let CTS_{ι} denote the category of CTS’s with start state, and their morphisms. It is a straightforward consequence of the results for CTS that the category CTS_{ι} has all small limits. It can also be shown that CTS_{ι} has all small coproducts.

2.3 Computation Categories

Define a computation category to be a small category C with the following properties:

1. C has a terminal object.

2. Every arrow of C is an epimorphism.

3. Every isomorphism of C is an identity.

4. C has a pushout for every coinitial pair of arrows.

Theorem 2.3 Suppose C = (G, id, ↑) is a complete CTS, and let · denote the composition operation of C. Then C′ = (G^{♯}, id, ·) is a computation category. Conversely, suppose C′ = (G′, id, ·) is a computation category. Since the terminal object of C′ is unique by property (3), we may regard G′ as an augmented graph G^{♯}. For coinitial arrows t, u, let t ↑ u denote the arrow opposite t in the pushout square determined by t and u. Then C = (G, id, ↑) is a complete CTS.

Proof – (⇐) If a small category C′ is given with properties (1)-(4), then standard categorytheoretic arguments suffice to show that (G, id, ↑) satisfies the axioms for a complete CTS.

(⇒) Conversely, given a complete CTS C, it follows from completeness and Lemma 2.1.4 that C′ is a category in which every arrow is an epimorphism. The state Ω is clearly a terminal object of C′. If v is an isomorphism of C′, with inverse v′, then v ⪯ vv′ = id_{dom(v)} and id_{dom(v)} ⪯ v, so v = id_{dom(v)} = v′ by Lemma 2.1.1. The completeness of C implies that every coinitial pair of arrows t, u has a join t ∨ u, which is a least upper bound of t and u by Lemma 2.1.6. Thus, every upper bound of t and u factors through t ∨ u. The uniqueness of such factorizations follows from the fact that every arrow is an epimorphism. Since t(u ↑ t) = t ∨ u = u(t ↑ u), it is now immediate that t, u, (u ↑ t), and (t ↑ u) form a pushout square in C′.

We now show that every CTS C freely generates a complete CTS C^{∗}, which has the same states as C and whose transitions are equivalence classes of finite composable sequences of transitions of C. The construction generalizes the construction of the free category G^{∗} generated by a graph G. The construction was discovered by Lévy [22] in the setting of the λ-calculus, and adapted in [5, 15] to the cases of recursive programs and left-linear term-rewriting systems without critical

[figure: a_{1}; a_{2}; a_{n}; b_{1}; b_{2}; b_{m}; u; t; u ↑^{∗} t; t ↑^{∗} u]

Figure 3: Extension of ↑ to ↑^{∗}

pairs. Consideration of problems in the theory of concurrency led to its independent rediscovery by the author in the present axiomatic setting.

Suppose C = (G, id, ↑) is a CTS. Let G^{∗} denote the free category (objects=objects of G, arrows=finite composable sequences of arrows of G) generated by G. If t = q_{0}⟶^{a_{1}}q_{1}⟶^{a_{2}} … ⟶^{a_{n}}q_{n} is an arrow of G^{∗}, then let |t| denote the length n of t. For k > 0, let id_{q}^{k} denote the arrow of G^{∗} which is the sequence consisting of k copies of id_{q}. By convention, we define id_{q}^{0} to be the identity for state q in G^{∗}.

Let ↑^{∗} be the extension to (G^{∗})^{♯} of the operation ↑ on G^{♯}, defined recursively by the following properties (see Figure 3):

1. id_{q}^{0} ↑^{∗} t = id_{r}^{0} and t ↑^{∗} id_{q}^{0} = t for all t : q → r in G^{∗}.

2. For all t in G^{∗} and all a, b ∈ G, with a, b coinitial and a, t composable,

at ↑^{∗} b = \{ \begin{matrix}(a ↑ b)(t ↑^{∗} (b ↑ a)), & if a, b and t, b ↑ a are consistent \\ ω_{cod(b)}, & otherwise. \end{matrix}

3. For all t, u in G^{∗} with |u| > 0, and all b ∈ G, with b, t coinitial and b, u composable,

t ↑^{∗} bu = (t ↑^{∗} b) ↑^{∗} u

4. ω_{q} ↑^{∗} t = ω_{r} and t ↑^{∗} ω_{q} = ω_{Ω} for all t : q → r in (G^{∗})^{♯}.

Lemma 2.3.1

1. For all objects q of (G^{∗})^{♯}, all coinitial arrows t, u of (G^{∗})^{♯}, and all k ≥ 0,

(a) dom(id_{q}^{k}) = cod(id_{q}^{k}) = q; (b) dom(t ↑^{∗} u) = cod(u); and

(c) cod(t ↑^{∗} u) = cod(u ↑^{∗} t).

2. For all arrows t : q → r of (G^{∗})^{♯}, and all k ≥ 0,

(a) id_{q}^{k} ↑^{∗} t = id_{r}^{k};

(b) t ↑^{∗} id_{q}^{k} = t;

(c) t ↑^{∗} t = id_{r}^{|t|};

3. For all coinitial arrows t, u, v of (G^{∗})^{♯}, (v ↑^{∗} t) ↑^{∗} (u ↑^{∗} t) = (v ↑^{∗} u) ↑^{∗} (t ↑^{∗} u).

Proof – Straightforward induction arguments using the properties of ↑ and the definition of ↑^{∗}.

Let Cts(G^{∗}) denote the “minimally consistent” CTS with G^{∗} as its underlying graph, as defined in Section 2, Example 1.

Let ∼ be the binary relation on the arrows of G^{∗} defined by: t ∼ u iff t ↑^{∗} u = id_{r}^{|t|} and u ↑^{∗} t = id_{r}^{|u|}.

Lemma 2.3.2 The relation ∼ is a strong congruence on Cts(G^{∗}).

Proof – It is clear that ∼ is symmetric. It is reflexive because t ↑^{∗} t = id_{r}^{|t|} by Lemma 2.3.1(2c). Transitivity follows from Lemma 2.3.1(3), as in the proof of Lemma 2.1.1.

(1) Suppose transitions t, t′, u, u′ of Cts(G^{∗}) are such that t ∼ t′, u ∼ u′, and t, u are consistent. We show that t′, u are consistent and t ↑^{∗} u ∼ t′ ↑^{∗} u; a similar argument (which we omit) then shows that t′, u′ are consistent and t′ ↑^{∗} u ∼ t′ ↑^{∗} u′. By Lemma 2.3.1(3), (t′ ↑^{∗} u) ↑^{∗} (t ↑^{∗} u) = (t′ ↑^{∗} t) ↑^{∗} (u ↑^{∗} t), which equals id_{t}^{|t′|} by Lemma 2.3.1(2a) and the assumption that t ∼ t′. Similarly, (t ↑^{∗} u) ↑^{∗} (t′ ↑^{∗} u) = (t ↑^{∗} t′) ↑^{∗} (u ↑^{∗} t′) = id_{t}^{|t|}, hence t ↑^{∗} u ∼ t′ ↑^{∗} u. Since t and u are consistent by assumption, it follows that t′ and u are consistent.

(2) First note that it is immediate from Lemma 2.3.1(2a,b) that t ∼ id_{q}^{0} holds for a transition of Cts(G^{∗}) iff t = id_{q}^{|t|}. Now, suppose t ↑ u and u ↑ t are both ∼-related to identities. Then we must have t ↑ u = id_{cod(u)}^{|t|} and u ↑ t = id_{cod(t)}^{|u|}. But this states exactly that t ∼ u.

Define the completion C^{∗} of C to be the quotient Cts(G^{∗})/ ∼. That C^{∗} is a complete CTS is immediate from the completeness of Cts(G^{∗}) and Lemma 2.2.1.

Theorem 2.4 The map taking a CTS C to its completion C^{∗} is the object map of a functor from CTS to the full subcategory CCTS of CTS whose objects are the complete CTS’s, and this functor is left-adjoint to the inclusion of CCTS in CTS.

Proof – Let μ_{C} : C → C^{∗} take each transition t of C to its equivalence class [t]; then μ_{C} is obviously a morphism. To prove the theorem, it suffices to show that to each morphism ρ from C to a complete CTS D, there is a unique morphism ρ^{∗} : C^{∗} → D satisfying ρ^{∗} ∘ μ_{C} = ρ.

We first note that a straightforward induction using Lemma 2.3.1 establishes the following fact: If

a_{1}a_{2} … a_{n} ↑^{∗} b_{1}b_{2} … b_{m} = c_{1}c_{2} … c_{n},

then

ρ(a_{1})ρ(a_{2}) … ρ(a_{n}) ↑ ρ(b_{1})ρ(b_{2}) … ρ(b_{m}) = ρ(c_{1})ρ(c_{2}) … ρ(c_{n}).

Now, every proper transition of C^{∗} is either an identity or of the form [a_{1}a_{2} … a_{n}], where n > 0 and each a_{i} is a proper transition of C. By Lemma 2.2.1, any morphism ρ^{∗} : C^{∗} → D must satisfy ρ^{∗}([a_{1}a_{2} … a_{n}]) = ρ^{∗}([a_{1}])ρ^{∗}([a_{2}]) … ρ^{∗}([a_{n}]). The condition ρ^{∗} ∘ μ_{C} = ρ implies in addition that ρ^{∗}([a_{i}]) = ρ(a_{i}), hence ρ^{∗}([a_{1}a_{2} … a_{n}]) = ρ(a_{1})ρ(a_{2}) … ρ(a_{n}). Thus, there can be at most one morphism ρ^{∗} : C^{∗} → D satisfying ρ^{∗} ∘ μ_{C} = ρ.

To show that ρ^{∗} exists, it suffices to show that for all proper transitions a_{1}, a_{2},…, a_{n} and b_{1}, b_{2},…, b_{m} of C, if [a_{1}a_{2} … a_{n}] = [b_{1}b_{2} … b_{m}], then ρ(a_{1})ρ(a_{2}) … ρ(a_{n}) = ρ(b_{1})ρ(b_{2}) … ρ(b_{m}). But if [a_{1}a_{2} … a_{n}] = [b_{1}b_{2} … b_{m}], then a_{1}a_{2} … a_{n} ↑^{∗} b_{1}b_{2} … b_{m} = id_{cod(b_{m})}^{n} and b_{1}b_{2} … b_{m} ↑^{∗} a_{1}a_{2} … a_{n} = id_{cod(a_{n})}^{m}. Applying the fact noted above, we see that

ρ(a_{1})ρ(a_{2}) … ρ(a_{n}) ↑ ρ(b_{1})ρ(b_{2}) … ρ(b_{m}) and ρ(b_{1})ρ(b_{2}) … ρ(b_{m}) ↑ ρ(a_{1})ρ(a_{2}) … ρ(a_{n})

are identities, showing ρ(a_{1})ρ(a_{2}) … ρ(a_{n}) = ρ(b_{1})ρ(b_{2}) … ρ(b_{m}).

Finally, to show that the function ρ^{∗} is a morphism, we must show that it preserves identities and translation. Each identity of C^{∗} is of the form [id_{q}^{n}], where id_{q} is an identity of C, and we must have ρ^{∗}([id_{q}^{n}]) = ρ(id_{q})^{n} = id_{ρ(q)}. Moreover, if [a_{1}a_{2} … a_{n}] and [b_{1}b_{2} … b_{m}] are consistent, then using the fact noted above shows that

ρ^{∗}([a_{1}a_{2} … a_{n}] ↑ [b_{1}b_{2} … b_{m}]) = ρ^{∗}([a_{1}a_{2} … a_{n} ↑^{∗} b_{1}b_{2} … b_{m}])
= ρ(a_{1})ρ(a_{2}) … ρ(a_{n}) ↑ ρ(b_{1})ρ(b_{2}) … ρ(b_{m})
= ρ^{∗}([a_{1}a_{2} … a_{n}]) ↑ ρ^{∗}([b_{1}b_{2} … b_{m}]),

as required.

2.4 Computation Diagrams

In this section we generalize to CTS’s the notions of “computation tree” and “computation” for ordinary transition systems.

A computation diagram is a CTS D, whose completion D^{∗} is a poset category having an initial (least) object. We regard the class of all computation diagrams as a full subcategory Diag of CTS_{ι}, by identifying a computation D with the corresponding CTS with start state (D, ι), whose start state is the initial object of D.

Define the elements of a computation diagram D to be the proper initial arrows of D^{∗}. Note that the elements of D are in bijective correspondence with the states of D. Define the successor relation ≺_{1} on the elements of D by t ≺_{1} u iff u ↑ t is a transition of D. The successor relation is easily seen to be an irreflexive relation, whose reflexive, transitive closure is the prefix relation ⪯ on the set of elements of D.

Given a CTS with start state (C, ι), let C^{∗} be the completion of C. Define the CTS Diag(C, ι) to have as proper states all transitions t of C^{∗} whose domain is the start state of (C, ι), and as transitions pairs (t, u) of states of Diag(C, ι), such that t ⪯ u and u ↑ t is a transition of C. Define dom(t, u) = t and cod(t, u) = u. Let (t, u) and (t, v) be consistent in Diag(C, ι) iff u and v are consistent in C, in which case define (t, u) ↑ (t, v) = (v, u ∨ v). It is easily verified that Diag(C, ι) is a computation diagram, and we call it the computation diagram of (C, ι).

Theorem 2.5 The map, taking a CTS with start state (C, ι) to its computation diagram Diag(C, ι), is the object map of a functor Diag : CTS_{ι} → Diag, which is right-adjoint to the inclusion of Diag in CTS_{ι}.

Proof – Let π_{C} : Diag(C, ι) → (C, ι) take each transition (t, u) of Diag(C, ι) to the corresponding transition u ↑ t of C. It is straightforward to check that π_{C} is a CTS_{ι}-morphism, and that every morphism ρ from a computation diagram D to (C, ι) factors uniquely through π_{C}.

Recall that an ideal of a partially ordered set (K, ⪯) is a subset J of K that is:

1. (Nonempty): J ≠ ∅.

2. (Downward-closed): If t ∈ J and u ∈ K are such that u ⪯ t, then u ∈ J.

3. (Directed): If t ∈ J and u ∈ J, then there exists v ∈ J such that t ⪯ v and u ⪯ v.

An ideal J of K is principal if it is the set of all elements below some element t of K.

We define a computation of a CTS with start state (C, ι) to be an ideal of the set of elements of its computation diagram Diag(C, ι), under the ordering ⪯. A computation of C is called finite if it is a principal ideal, otherwise it is called infinite. Note that the computations of (C, ι) are in natural bijective correspondence with the determinate subdiagrams of Diag(C, ι). Although we could have defined the computations of (C, ι) to be the determinate subdiagrams of Diag(C, ι), it will be convenient later on to think of a computation of (C, ι) as a set of transitions of C^{∗}, rather than as a subdiagram of Diag(C, ι).

A set J of computations of a CTS with start state (C, ι) is called chain-complete if whenever I is a subset of J that is linearly ordered with respect to inclusion, then ⋃ I is an element of J.

Lemma 2.4.1

1. The set of computations of a CTS with start state (C, ι) is an algebraic directed-complete poset under inclusion order, whose compact elements are exactly the finite computations.

2. Every consistent set of elements of Diag(C, ι) is included in a unique least computation of (C, ι).

3. If J is a nonempty, chain-complete set of computations of (C, ι), then every element of J is included in a maximal element of J.

Proof – (1) That the set of computations of (C, ι) is an algebraic directed-complete poset, with the finite computations as isolated elements, is a standard property of the “completion by ideals” of a partially ordered set (see e.g. [11]).

(2) is obvious from the fact that ideals are defined by closure properties.

(3) is just Zorn’s Lemma applied to sets of computations.

We conclude this section with a result that shows that our generalized definition of computations as ideals does not depart too radically from the more conventional notion of computation sequences.

A computation sequence for a CTS with start state (C, ι) is a sequence ⊥ = t_{0} ≺_{1} t_{1} ≺_{1} … ≺_{1} t_{n} of elements of Diag(C, ι). The element t_{n} is called the result of the computation sequence. Since every element of Diag(C, ι) is the result of some computation sequence for (C, ι) (by the initiality of ⊥), we may prove properties of finite computations by induction on the length of a computation sequence. A generalized computation sequence for (C, ι) is a sequence ⊥ = t_{0} ⪯ t_{1} ⪯ t_{2} ⪯ … of elements of Diag(C, ι), such that for each k ≥ 0, either t_{k} ≺_{1} t_{k+1} or t_{k} = t_{k+1}. The ideal ⋁_{k=0}^{∞} t_{k} is called the computation generated by the sequence t_{0} ⪯ t_{1} ⪯ t_{2} . . ..

A coinitial set of transitions T of a CTS C is called independent if it is consistent, and for all t ∈ T and all finite sets T′ ⊆ T, if t ⪯ ⋁ T′, then t ∈ T′. The CTS C is said to have finite concurrency if there are no infinite independent sets of transitions in C.

Theorem 2.6 Suppose (C, ι) is a CTS with start state, where C has finite concurrency. Then every computation of (C, ι) is generated by some generalized computation sequence of (C, ι).

Proof – Straightforward.

3 CTS Semantics of Process Networks

In this section, we show how concurrent transition systems can be used as the basis for a dataflowlike model of concurrent computation. The kind of model we consider is similar to those of [16, 17, 6, 10, 24, 34], and concerns a system of processes with internal state that communicate by transmitting messages through named ports. Each port is shared by at most two processes, one of which (called the “receiver”) always inputs messages from the port, and the other of which (called the “sender”) always outputs messages to the port. Typically, ports are regarded as buffers that transmit messages in FIFO order. However, for our purposes, it will be convenient to take a slightly more abstract point of view in which we think of the state of a port as part of the internal state of the reader of that port. This permits us to regard the transmission of a message by a sender and the arrival of that message at the input port of a receiver as synchronized, simultaneous occurrences. It will also be convenient to adopt a slightly more abstract point of view than usual, regarding the number and type of the ports used by a process. That is, rather than assume that a process has a specific number of input and output ports, each of which is capable of handling values from a certain set, we merely assume that each process has a “type” (X, Y), where X and Y are trace algebras whose elements represent possible message histories for the input and output ports of that process, respectively. The example at the end of Section 3.1 will clarify this point.

Since we will be making frequent use of trace algebras (see Section 2, Example 2), some additional notation will be convenient. If X is a trace algebra, then we denote the identity of X by ϵ_{X}, or just ϵ, when X is clear from the context. We denote the prefix ordering by ⪯_{X}, or just ⪯, and the join by ∨_{X}, or just ∨. We identify a trace algebra X with the corresponding one-proper-state CTS, so that trace algebras form a full subcategory of CTS. If X and Y are trace algebras, then their product X × Y in CTS is also a trace algebra. We use π_{X} and π_{Y} to denote the projections from X × Y to X and Y, respectively. We use the notation x; y to denote the element of X × Y with π_{X}(x; y) = x and π_{Y} (x; y) = y. If λ : C → X × Y is a morphism, then we often write λ_{X} or λ_{Y} as an abbreviation for π_{X} ∘ λ and π_{Y} ∘ λ. The ideal space of X is the set \overline{X} of ideals of X, which is an algebraic directed-complete poset with respect to inclusion. It will be convenient to regard X as included in \overline{X}, by identifying each x ∈ X with the corresponding principal ideal. We can then view the inclusion order on \overline{X} as an extension of the prefix ordering ⪯ on X, and we use the same symbol ⪯ in both cases. The elements of X ⊆ \overline{X} are called the finite elements of \overline{X}, and all other elements of \overline{X} are called infinite. A morphism ρ : X → Y extends uniquely to a continuous function \overline{ρ} : \overline{X} → \overline{Y}. We will generally identify \overline{X × Y} and \overline{X} × \overline{Y}, exploiting the obvious natural isomorphism.

3.1 Machines

Suppose C is a CTS. An endomorphism μ : C → C is orthogonal if,

• For all transitions t of C, if μ(t) is an identity, then t is an identity.

• For all coinitial pairs t, u of transitions of C, if μ(t) and μ(u) are consistent, then so are t and u.

An action of a trace algebra X on C is a monoid homomorphism δ : X → CTS(C, C), such that for each x ∈ X, the morphism δ(x) is orthogonal. We usually write δ_{x}, instead of δ(x), for the application of an action δ to argument x ∈ X.

Suppose X and Y are trace algebras. An (X, Y)-machine is a four-tuple M = (C, ι, λ, δ), where:

• C is a CTS, called the underlying CTS of M;

• ι : 1 → C is a morphism, called the start state map of M.

• λ : C → Y is a morphism, called the output map of M;

• δ : X → CTS(C, C) is an action of X on C, called the input map of M;

such that λ ∘ δ_{x} = λ for all x ∈ X.

If M = (C, ι, λ, δ) and M′ = (C′, ι′, λ′, δ′) are (X, Y)-machines, then a morphism from M to M′ is a morphism μ : C → C′ of the underlying CTS’s, such that

1. ι′ = μ ∘ ι.

2. λ = λ′ ∘ μ.

3. δ′_{x} ∘ μ = μ ∘ δ_{x} for all x ∈ X.

Let Mach_{X,Y} denote the category of (X, Y)-machines and their morphisms.

A machine is called a Kahn machine if its underlying CTS is determinate.

In the special case that X = 1 (the terminal object in CTS), an (X, Y)-machine will be called a Y -automaton. Note that a Y -automaton is completely specified by giving its underlying CTS C, its start state map ι, and its output map λ : C → Y, since there is only one possible input map δ : 1 → CTS(C, C). Let Auto_{Y} denote the category of Y -automata.

To illustrate the expressive power of the (X, Y)-machine model, we show how the axioms are satisfied by a kind of process that communicates with its environment by reading sequences of values from input ports and writing sequences of values to output ports.

Formally, suppose V is a set of values, and m, n are natural numbers. Then a sequential dataflow process (SDP) with m input ports and n output ports is a triple (Q, ι, A), where

• Q is a set of states, with ι ∈ Q a distinguished start state.

• A ⊆ (Q × (V^{∗})^{m}) × (V^{∗})^{n} × (Q × (V^{∗})^{m}) is a set of transitions. such that

1. For all q ∈ Q, the set A contains a transition ((q, ϵ), ϵ, (q, ϵ)).

2. If the set A contains a transition ((q, x), y, (q′, x′)), then A also contains a transition ((q, xx_{0}), y, (q′, x′x_{0})) for each x_{0} ∈ X.

Each transition ((q, x), y, (q′, x′)) in A represents a possible process step, in which a vector x of value sequences on the input ports of the process is replaced by a new vector x′ (if x = x′′x′, then we may think of the prefix x′′ of x as being consumed in the step), a vector y of value sequences is transmitted to the output ports of the process, and the internal state of the process is changed from q to q′. We think of input values arriving at the input port of a process as getting concatenated with the current sequence of values in the port. Condition (2) above thus states that arrival of new input values can never cause transitions enabled for a process to become disabled, only new transitions to become enabled.

Any program expressed in a nondeterministic sequential programming language with primitives for reading values from input ports and writing values to output ports, but not for testing for the absence of values on input ports, can be regarded as defining an SDP. For m ≥ 0, let (V^{∗})^{m} be the trace algebra whose elements are m-vectors of elements of the free monoid V^{∗}, with composition and identity defined componentwise. Assuming a suitable definition of the “input/output relation” computed by a process (we shall provide such a definition in the sections to follow), it can be shown that every continuous function from (\overline{V^{∗}})^{m} to (\overline{V^{∗}})^{n} is computed by an SDP. An example of a non-functional process also representable as an SDP is “unfair merge,” which has two input ports and one output port, and executes a loop in which input is nondeterministically chosen from one of the input ports and output on the output port. This merge is “unfair” because we do not make any assumption about how often in a computation one enabled branch of a nondeterministic choice may be rejected in favor of another (although we do introduce a kind of fairness assumption with respect to choices between consistent transitions).

An SDP (Q, ι, A) may be regarded as an (X, Y)-machine M = (C, ι, λ, δ) as follows:

• Let X be the trace algebra (V^{∗})^{m} and Y the trace algebra (V^{∗})^{n}.

• Let the CTS C have as proper states the elements of Q, and as proper transitions the elements of A. Define

dom((q, x), y, (q′, x′)) = q
cod((q, x), y, (q′, x′)) = q′.

Let the identities of C be the transitions ((q, ϵ), ϵ, (q, ϵ)), and let ↑ be defined so that two coinitial transitions are consistent iff they are equal, or one is an identity.

• Let λ : C → Y take ((q, x), y, (q′, x′)) to y.

• Let δ : X → CTS_{ι}(C, C) be defined so that δ_{x_{0}} takes a transition ((q, x), y, (q′, x′)) ∈ A to the transition ((q, xx_{0}), y, (q′, x′x_{0})) ∈ A, which exists by condition (2) in the definition of an SDP above.

It is straightforward to check that these definitions satisfy the requirements for an (X, Y)-machine.

[figure: M; M; M′; M; M; ρ; ρ; X; Y; Y′; X′; Z; Z; X; Y; X; Y; Z; X; Y; Z; X; X′; Y; Y′; X; Y; Y; X; Parallel Product; Output Relabeling; Input Relabeling; Feedback]

Figure 4: Operations on Machines

3.2 An Algebra of Machines

We are interested in the properties of an algebra of machines, with respect to operations that correspond to ways of building more complex machines from simpler components. Although many such operations can be defined, in this paper we restrict our attention to parallel product, input and output relabeling, and feedback. The effect of these operations is depicted schematically in Figure 4.

3.2.1 Parallel Product

Suppose M = (C, ι, λ, δ) is an (X, Y)-machine and M′ = (C′, ι′, λ′, δ′) is an (X′, Y′)-machine. Define the parallel product of M and M′ to be the (X × X′, Y′ × Y)-machine

M × M′ = (C × C′, (ι, ι′), λ′′, δ′′),

where λ′′ takes each transition (t, t′) of M × M′ to the trace λ′(t′); λ(t) ∈ Y′ × Y, and δ′′_{x;x′}(t, t′) = (δ_{x}(t), δ′_{x}(t′)) for each x; x′ ∈ X × X′ and transition (t, t′) of C × C′.

Parallel product is easily seen to be the object map of a functor from Mach_{X,Y} × Mach_{X′,Y′} to Mach_{X×X′,Y′×Y}.

3.2.2 Output Relabeling

Suppose M = (C, ι, λ, δ) is an (X, Y)-machine, and ρ : Y → Z is a morphism. Define the output relabeling of M by ρ to be the (X, Z)-machine

M ρ = (C, ι, ρ ∘ λ, δ).

Output relabeling is the object map of a functor from Mach_{X,Y} to Mach_{X,Z}.

3.2.3 Input Relabeling

Suppose M = (C, ι, λ, δ) is an (X, Y)-machine, and ρ : Z → X is a morphism. Define the input relabeling of M by ρ to be the (Z, Y)-machine

ρ M = (C, ι, λ, δ ∘ ρ).

Input relabeling is the object map of a functor from Mach_{X,Y} to Mach_{Z,Y}.

3.2.4 Feedback

Suppose M = (C, ι, λ, δ) is a (Z × X, Y × Z)-machine. Define the feedback {M}_{Z} of M with respect to Z to be the (X, Y × Z)-machine

{M}_{Z} = (C′, ι, λ′, δ′),

where

• C′ is a CTS whose states and transitions are the same as those of C, but whose domain and codomain functions are defined as follows:

dom′(t) = dom(t)
cod′(t) = δ_{λ_{Z}(t);ϵ_{X}} (cod(t))

The identities of C′ are the same as those of C. For coinitial t, u, define

t ↑′ u = δ_{λ_{Z}(u);ϵ_{X}} (t ↑ u).

• λ′ : C′ → Y is defined by λ′(t) = λ(t).

• δ′ : X → CTS(C′, C′) is defined by δ′_{x}(t) = δ_{ϵ_{Z};x}(t).

It is straightforward to verify that {M}_{Z} is, in fact, an (X, Y × Z)-machine. The assumption that δ_{z;x} is orthogonal for all z; x ∈ Z × X is used in the verification of CTS axioms (3) and (4).

Intuitively, the machine {M}_{Z} represents the machine M with its Z-output “fed back” to its Z-input. Thus, each transition t of {M}_{Z} is a transition of M that has been “composed” with the effect, given by δ_{λ_{Z}(t);ϵ_{X}}, of the feedback input generated by t.

The feedback operation can be shown to be the object map of a functor from Mach_{Z×X,Y ×Z} to Mach_{X,Y ×Z}.

3.3 Observable Equivalence

Define the pairing of an (X, Y) machine M and a (Y, X)-machine N to be the (X × Y)-automaton

⟨M, N ⟩ = {M × N }_{X×Y} .

Intuitively, the automaton ⟨M, N ⟩ represents a closed system consisting of machines M and N executing in parallel, with the output of M feeding the input of N and the output of N feeding the input of N.

Lemma 3.3.1

1. Suppose M is an (X, Y)-machine, N is a (Y, X)-machine, and π : X × Y → Y × X takes

x; y to y; x. Then

⟨M, N ⟩ ≃ ⟨N , M⟩ π.

2. Suppose M is an (X, Y)-machine, N is a (Z, X)-machine, and ρ : Y → Z. Then

⟨M ρ , N ⟩ ≃ ⟨M, ρ N ⟩ (π_{X} × (ρ ∘ π_{Y})).

3. Suppose M is an (X, Y)-machine, N is a (Z, W)-machine, and P is a (W × Y, X × Z)-

machine. Then

⟨M × N , P⟩ ≃ ⟨M, {N × P}_{Z×W} ⟩.

Proof – Straightforward.

Although a result exactly analogous to (2) and (3) above does not hold for the feedback operation, we can obtain a useful weaker result (Lemma 3.3.2 below). To state it, we need to define the output set of an automaton. Output sets of automata are a special cases of input/output relations of machines, which we will define and investigate in more detail in Section 4.

Suppose A = (C, ι, λ) is a Y -automaton. The computations of A are the computations of the CTS with start state (C, ι). A computation J of A is maximal if it is not a proper subset of any other computation of A. Now, if π_{C} : Diag(C, ι) → (C, ι) denotes the universal morphism associated with the right adjoint Diag, then λ ∘ π_{C} : Diag(C, ι) → Y extends uniquely to a continuous map \overline{λ} from the cpo of computations of (C, ι) to the ideal space \overline{Y} of Y. Thus, each computation J of A determines an ideal \overline{λ}(J) ∈ \overline{Y}, which we call the complete output trace of J. The output set Out(A) of A is the set of all complete output traces determined by maximal computations of A.

We also need a (Z, Z)-machine I_{Z} that simply passes its input through unchanged to its output. Lemma 4.6.2 provides such a machine, and we anticipate this result here, rather than restating a special case.

Lemma 3.3.2 Suppose M is a (Z × X, Y × Z)-machine, and N is a (Y × Z, X)-machine. Let ρ : Y ×Z → Y ×Z×Z be the morphism that takes y; z to y; z; z, and let π : Z×X×Y ×Z → X×Y ×Z be the morphism that takes z′; x; y; z to x; y; z. Then

Out⟨{M}_{Z} , N ⟩ = Out(⟨M, ρ (N × I_{Z}) ⟩ π).

Proof – Suppose ⟨{M}_{Z} , N ⟩ = (C, ι, λ) and ⟨M, ρ (N × I_{Z}) ⟩ π = (C′, ι′, λ′). Let (D, λ) = Diag(C, ι) and (D′, λ′) = Diag(C′, ι′). We can construct morphisms ρ : D^{∗} → (D′)^{∗} and ρ′ : (D′)^{∗} → D^{∗}, preserving the initial state, and such that (λ′)^{∗} = λ^{∗} ∘ ρ, ρ′ ∘ ρ = id_{Diag(C,ι)}, and t′ ⪯ ρ(ρ′(t′)) for all elements t′ of Diag(C′, ι). From this, it follows that the output sets of the two automata are identical. We omit the details.

We say that (X, Y)-machines M and M′ are observably equivalent, and we write M ∼ M′, if we have

Out⟨M, N ⟩ = Out⟨M′, N ⟩

for all (Y, X)-machines N. Here we use the idea of defining process equivalences based on indistinguishability with respect to tests performed by “observers” or “environments,” which is discussed in [12].

Theorem 3.1 Observable equivalence is a congruence with respect to parallel product, output relabeling, and feedback. It is also a congruence with respect to input relabeling by left-invertible morphisms. That is,

1. Suppose M and M′ are (X, Y)-machines, and M ∼ M′. Then

(a) M × N ∼ M′ × N, for all machines N.

(b) M ρ ∼ M′ ρ for all morphisms ρ : Y → Z.

(c) ρ M ∼ ρ M′ for all morphisms ρ : Z → X for which there exists a morphism ρ′ : X → Z with ρ′ ∘ ρ = id_{Z}.

2. Suppose M and M′ are (Z × X, Y × Z)-machines. If M ∼ M′, then {M}_{Z} ∼ {M′}_{Z} .

Moreover, ∼ is the largest congruence on machines, respecting parallel product and feedback, that does not relate automata with distinct output sets.

Proof – (1a) Let P be an arbitrary (W × Y, X × Z)-machine, and let π be as in Lemma 3.3.1(3). Using that lemma and the equivalence of M and M′, we have:

Out⟨M × N , P⟩ = Out⟨M, {N × P}_{Z×W} ⟩
= Out⟨M′, {N × P}_{Z×W} ⟩
= Out⟨M′ × N , P⟩.

(1b) Similar to (1a), but using Lemma 3.3.1(2).

(1c) Similar to (1b), but using the isomorphism

⟨ρ M , N ⟩ ≃ ⟨M, N ρ ⟩ ((ρ′ ∘ π_{X}) × π_{Y}),

obtained from Lemma 3.3.1(1, 2), plus the assumption that ρ′ ∘ ρ = id_{Z}.

(2) Similar to the above, but using Lemma 3.3.2.

To show that ∼ is the largest congruence that respects parallel product and feedback, but does not relate automata with distinct output sets, suppose ≈ is a congruence on machines that relates two (X, Y)-machines M and M′ that are not related by ∼. By definition of ∼, there exists a (Y, X)-machine N such that

Out⟨M, N ⟩ ≠ Out⟨M′, N ⟩.

But we must have ⟨M, N ⟩ ≈ ⟨M′, N ⟩ by the assumption that ≈ is a congruence with respect to parallel product and feedback. Hence ≈ relates two automata with distinct output sets.

The full abstraction problem for machines is the problem of characterizing the structure of the quotient algebra of machines modulo observable equivalence. The difficulty of this problem has become apparent since it was first pointed out by Keller [18] and more conclusively by Brock and Ackerman [7] (the so-called “Brock-Ackerman anomaly”) that the mapping taking machines to their input/output relations is not homomorphic with respect to feedback. Since then, a number of researchers [31, 32, 3, 19, 34, 20] have proposed process models that incorporate somewhat more information than just input/output relations. Abramsky [1], has shown the full abstractness of a powerdomain model, with respect to a notion of observable equivalence based on finite computations. To the author’s knowledge, though, none of these models has been shown both consistent with (i.e. a homomorphic image of) an operational semantics as well as fully abstract (i.e. observably equivalent processes have identical images), when both infinite and finite computations are considered.

4 An Analysis of Feedback

It would seem that a deep understanding of the feedback operation is prerequisite to solving the full abstraction problem. Whereas the parallel product operation is readily seen to be respected by the mapping from machines to input/output relations, the same does not hold for the feedback operation. The input/output relation of a (Z × X, Y × Z)-machine M simply does not contain enough information, in general, to determine the input/output relation of {M}_{Z} .

In an attempt to make progress on the full abstraction problem, in this section we investigate how the feedback operation behaves under a sequence of mappings that starts with machines and ends with input/output relations. The idea is to try to delete more and more information, getting successively more abstract representations of the behavior of machines, until we cannot see how to delete any more information and still preserve the machine operations. Some of the representations at intermediate stages between machines and input/output relations are similar to various models that have been proposed for concurrent processes. Thus, as a byproduct of our analysis, we obtain an improved understanding of the relationship between these models.

Our first mapping takes an (X, Y)-machine to a corresponding (X × Y)-automaton. Whereas machines can be thought of as a CTS generalization of the sequential machines of classical automata theory, automata can be thought of as a CTS generalization of classical nondeterministic automata, or the labeled transition systems used, e.g. in [9, 8]. Our second mapping “unwinds” automata to obtain their “synchronization diagrams,” which are a generalization of “synchronization trees” [42]. We then show how each synchronization diagram determines a set of “behaviors,” which represent “fair” or “completed” computations. Abstracting further from sets of behaviors, we obtain sets of “histories,” which are related to the “pomset” model of [32, 33]. We then map sets of histories to sets of “scenarios”, where a scenario represents information about causal relationships between input and output in a single computation. Our scenarios are similar in spirit, although not formally identical to, the scenarios originally defined by Brock and Ackerman [7, 6]. Finally, we show how scenario sets determine input/output relations.

For each of the mappings, we prove a theorem showing a sense in which the mapping is homomorphic with respect to the feedback operation on machines. All of the mappings except the one to input/output relations are homomorphic with respect to the full algebra of machines. The mapping from to input/output relations is homomorphic only on the subalgebra of Kahn machines. (Its failure to be homomorphic for unrestricted machines is the Brock-Ackerman anomaly already mentioned.) We show that the input/output relation of an (X, Y)-Kahn machine is the graph of a continuous function from \overline{X} to \overline{Y}, and that the map from Kahn machines to continuous functions transforms feedback into a certain least-fixed-point construction. This least-fixed-point characterization of feedback was first noted by Kahn [16], and has been called the “Kahn Principle.” Although the Kahn Principle has been proved before [10], our proof applies to a more general, axiomatically defined class of processes.

4.1 Automata

Given \overline{x} ∈ \overline{X}, let X̂ denote the (Y, X)-machine (X, ι, id_{X}, δ), where ι is the unique proper state of X and δ_{y} : X → X is id_{X} for each y ∈ Y. Intuitively, X̂ is a machine that ignores its input, and is capable of outputting an arbitrary element of X at any time. Each (X, Y)-machine M determines a corresponding (X × Y)-automaton Auto(M), under the definition

Auto(M) = ⟨M, X̂⟩.

Define an (X × Y)-automaton A to be an (X, Y)-input/output automaton (resp. (X, Y)-Kahn automaton) if A ≃ Auto(M) for some (X, Y)-machine (resp. (X, Y)-Kahn machine) M.

We now characterize the structure of input/output automata. To state this result, some additional terminology will be convenient. Suppose C is a CTS, and ρ : C → X is a morphism. We say that a proper transition t of A is canonical w.r.t. ρ, if for any other proper transition t′ of C, with dom(t) = dom(t′) and ρ(t′) = ρ(t), we have t ⪯ t′. Note that canonical transitions, when they exist, are uniquely determined by their domain and their image under ρ.

Theorem 4.1 An (X × Y)-automaton A = (C, ι, λ) is an (X, Y)-input/output automaton iff A has the following properties:

1. For each proper state q of A, and each x ∈ X, there exists a transition x_{q} of C, with dom(x_{q}) = q and λ_{X}(x_{q}) = x, such that x_{q} is canonical w.r.t. λ_{X}.

2. Each proper transition t : q → r of A, has a decomposition t = x_{q} ∨ u, where x = λ_{X}(t).

3. For each proper transition t : q → r of A, and each x ∈ X, we have x_{q} ↑ t = (x ↑ λ(t))_{r}.

4. For each proper transition t : q → r of A, and each x ∈ X, if x and λ(t) are consistent, then x_{q} and t are consistent, and x_{q} ∨ t exists in A.

5. For each proper transition t : q → r of A, and each x ∈ X, if λ_{X}(t) = ϵ and t ↑ x_{q} = id_{r}, then t = id_{q}.

Moreover, A is a Kahn automaton iff it has the additional property:

6. For each coinitial pair t, u of proper transitions of A, if λ_{X}(t) and λ_{X}(u) are consistent, then t and u are consistent.

Proof – We show: (⇒) If A ≃ Auto(M) for some M, then A has properties (1)-(5), and also property (6) in case M is a Kahn machine. (⇐) If A has properties (1)-(5), then A ≃ Auto(M) for some M, and if A has property (6), then M can be chosen to be a Kahn machine.

(⇒) Suppose A ≃ Auto(M). Since properties (1)-(5) are preserved under isomorphism, we may suppose without loss of generality that A = Auto(M). Then the state set of A is (in bijective correspondence with) the state set of M, and the transitions of A are pairs (t, x), where t is a transition of M and x ∈ X. It is easily shown that the transitions x_{q} = (id_{q}, x) are the canonical transitions required by property (1). The remaining properties then follow by straightforward calculations, which we omit.

(⇐) Suppose A = (C, ι, λ) has properties (1)-(5). We show how to construct M so that A ≃ Auto(M). It is easily verified that the states of C, equipped with all transitions t of C such that λ_{X}(t) = ϵ, define a sub-automaton A′ = (C′, ι, λ′) of A. Let δ : X → CTS(C′, C′) be defined by δ_{x}(t) = t ↑ x_{dom(q)}. Straightforward calculations, which we omit, from the definitions and properties (1)-(5) suffice to verify that M = (C′, ι, λ′_{Y} , δ) is an (X, Y)-machine. It is also easily verified that if A has property (6), then M is a Kahn machine.

We claim that A ≃ Auto(M). The required isomorphism μ : Auto(M) → A is obtained as the morphism that takes each transition (u, x) : dom(u) → δ_{x}(cod(u)) of Auto(M) to the join x_{q} ∨ u in A, which exists by property (4). The morphism μ is surjective on transitions because by property (2), every proper transition t of A has a decomposition t = x_{q} ∨ u, where x = λ_{X}(t). To show that it is injective on transitions, it suffices to show the uniqueness of such decompositions in A. If x_{q} ∨ u and x_{q} ∨ u′ are two decompositions of t, then (x_{q} ∨ u) ↑ (x_{q} ∨ u′) is an identity transition. Since (x_{q} ∨ u) ↑ (x_{q} ∨ u′) = [x_{q} ↑ (x_{q} ∨ u′)] ∨ [u ↑ (x_{q} ∨ u′)], it follows that u ↑ (x_{q} ∨ u′) is an identity transition. However, u ↑ (x_{q} ∨ u′) = (u ↑ u′) ↑ (x_{q} ↑ u′), and x_{q} ↑ u′ = x_{cod(u′)} by property (3). Hence u ↑ u′ is an identity transition by property (5). Similar reasoning shows that u′ ↑ u is an identity transition, thus u = u′.

In case A = (C, ι, λ) is an (X, Y)-input/output automaton, we will refer to the canonical transitions x_{q} of A as pure-input transitions, and to decompositions t = x_{q} ∨ v, with x = λ_{X}(t), as pure-input/output decompositions. It will also sometimes be convenient to use λ^{in} and λ^{out} as alternate notations for λ_{X} and λ_{Y}, respectively.

We now determine how the feedback operation on machines is transformed by the map from machines to automata. The relabeling functor

- (π_{Z} × id_{W ×Z}) : Auto_{W ×Z} → Auto_{Z×W ×Z}

has a right adjoint

{-}_{=Z} : Auto_{Z×W ×Z} → Auto_{W ×Z},

whose object map takes each Z × W × Z-automaton A = (C, ι, λ) to the (W × Z)-automaton {A}_{=Z} = (C′, ι, λ′), where C′ is the sub-CTS of C consisting of all transitions t of C for which the two Z components of λ(t) are equal, and λ′ takes each t in C′ to λ_{W ×Z}(t).

Theorem 4.2 Suppose M is a (Z × X, Y × Z)-machine. Then

Auto({M}_{Z} ) ≃ {Auto(M)}_{=Z}

Proof – If M = (C, ι, λ, δ), then the required isomorphism maps a transition (t, x) of Auto({M}_{Z} ) to the corresponding transition (t, λ_{Z}(t); x) of {Auto(M)}_{=Z}. The details are straightforward, and are omitted.

4.2 Synchronization Diagrams

If W is a trace algebra, then a W -synchronization diagram is a W -automaton D = (D, ⊥, λ), whose underlying CTS D is a computation diagram with initial state ⊥. Since ⊥ can be determined from the structure of D, it is redundant information for synchronization diagrams, and we henceforth omit mention of it. Let Diag_{W} denote the full subcategory of Auto_{W}, whose objects are the W -synchronization diagrams.

Suppose A = (C, ι, λ) is a W -automaton. Define the diagram of A to be the synchronization diagram Diag(A) = (Diag(C, ι), λ ∘ π_{C}), where π_{C} : Diag(C, ι) → (C, ι) is the universal morphism associated with the right adjoint Diag.

An (X × Y)-synchronization diagram is called an (X, Y)-input/output diagram (resp. (X, Y)- Kahn diagram) if it is isomorphic to Diag(A) for some (X, Y)-input/output automaton (resp. (X, Y)- Kahn automaton) A.

Lemma 4.2.1 An (X × Y)-synchronization diagram is an (X, Y)-input/output diagram (resp. (X, Y)-Kahn diagram) iff it is an (X, Y)-input/output automaton (resp. (X, Y)-Kahn automaton).

Proof – The result is easily established by noting that the properties of Theorem 4.1 are preserved under the “unwinding construction” by which Diag(A) is obtained from A.

Lemma 4.2.2 Suppose D = (D, λ) is an (X, Y)-input/output diagram.

1. For all x ∈ X, there exists an element t_{x} of D such that λ_{X}(t_{x}) = x, and such that if u is any element of D with λ_{X}(u) = λ_{X}(t_{x}), then t_{x} ⪯ u.

2. If u is an element of D, and x ∈ X is consistent with λ_{X}(u), then t_{x} and u are consistent.

3. Suppose D is a Kahn diagram. If t and u are two elements of D such that λ_{X}(t) and λ_{X}(u) are consistent, then t and u are consistent.

Proof – Straightforward from Lemma 4.2.1.

The elements t_{x} in (1) above are called the pure-input elements of D.

We now determine the form taken by the feedback operation on synchronization diagrams. Suppose D = (D, λ) is a (Z ×W ×Z)-synchronization diagram. Let λ_{Z_{1}} and λ_{Z_{2}} be the projections of λ on the first and second Z components, respectively. Define a feedback computation sequence for D to be a computation sequence t_{0} ≺_{1} t_{1} ≺_{1} … ≺_{1} t_{n} for D, such that λ_{Z_{1}}(t_{k}) = λ_{Z_{2}}(t_{k}) for 1 ≤ k ≤ n. An element of D is called feedback-reachable if it is the result of some feedback computation sequence for D, and a state of D is called feedback-reachable if it is the codomain of some feedback-reachable element of D. The feedback-reachable subdiagram of D is the full subdiagram D′ of D whose states are all the feedback-reachable states of D. Define {D}_{._{=}Z} = (D′, λ′), where D′ is the feedback-reachable subdiagram of D, and λ′(t) = λ_{W ×Z}(t).

Theorem 4.3 Suppose A is a (Z × W × Z)-automaton. Then

Diag({A}_{=Z}) ≃ {Diag(A)}_{._{=}Z}.

Proof – Straightforward from the observation that both functors

Diag({-}_{=Z}) : Auto_{Z×W ×Z} → Diag_{W ×Z}

and

{Diag(-)}_{._{=}Z} : Auto_{Z×W ×Z} → Diag_{W ×Z}

are right-adjoint to the composition of the output-relabeling functor

- (π_{Z} × id_{W ×Z}) : Auto_{W ×Z} → Auto_{Z×W ×Z}

with the inclusion of Diag_{W ×Z} in Auto_{W ×Z}. Since two right adjoints to the same functor are naturally isomorphic, the result follows.

4.3 Behaviors

If D = (D, λ) is a W -synchronization diagram, then each consistent set J of elements of D determines a consistent subset λ(J) of W, which we call the history of J with respect to λ. The set λ(J) extends to a least ideal \overline{λ}(J) ∈ \overline{W}, which we call the complete trace of J with respect to λ. If D is an (X, Y)-input/output diagram, and \overline{λ}(J) = \overline{x}; \overline{y}, then we call \overline{x} the complete input trace, and \overline{y} the complete output trace, of J. A behavior of D is a computation J of D that is maximal among all computations of D with the same complete input trace as J.

Lemma 4.3.1 Suppose D = (D, λ) is an (X, Y)-input/output diagram. Then

1. Each consistent set J of elements of D extends to a behavior of D having the same complete input trace as J. In particular, for each \overline{x} ∈ \overline{X} there is a behavior of D with \overline{x} as its complete input trace. Moreover, if D is a Kahn diagram, then its behaviors are uniquely determined by their complete input traces.

2. If J is a behavior of D with complete input trace \overline{x}, and \overline{x} ⪯ \overline{x}′, then J extends to a behavior J′ of D with complete input trace \overline{x}′.

3. If {J_{i} : i ∈ I} is any directed collection of behaviors of D, then ⋁{J_{i} : i ∈ I} is also a behavior of D.

Proof – (1) Suppose J is a consistent set of elements of D. Then the class of all consistent sets of elements of D with the same complete input trace as J is nonempty, and is easily seen to be chain-complete. Hence by Lemma 2.4.1 this class has a maximal element, which is a behavior of D with the same complete input trace as J. In the special case that the given set J is the set of all pure-input elements of D whose input traces are prefixes of \overline{x}, this construction yields a behavior of D with complete input trace \overline{x}. Moreover, the existence of two distinct behaviors of D with the same complete input trace implies the existence of two inconsistent elements of D with consistent input traces. Since by Lemma 4.2.2, this cannot happen when D is a Kahn diagram, we conclude that behaviors of Kahn diagrams are uniquely determined by their input traces.

(2) Given a behavior J of D with complete input trace \overline{x}, and given \overline{x}′ with \overline{x} ⪯ \overline{x}′, let K be the set of all pure-input elements of D whose input traces are prefixes of \overline{x}′. Then the set J ∪ K is consistent by Lemma 4.2.2, and has complete input trace \overline{x}′, hence it extends to a behavior J′ of D that has complete input trace \overline{x}′.

(3) Suppose the set J = ⋁{J_{i} : i ∈ I} were not a behavior of D. Then there would exist some element t of D whose input trace is a prefix of the complete input trace of J, but such that t ∉ J. But some J_{i} must have a complete input trace with that of t as a prefix, hence t ∈ J_{i} because J_{i} is a behavior of D. Since this contradicts the assumption t ∉ J, we conclude that t cannot exist.

If (K, ⪯) is a partially ordered set, and J ⊆ K, then J is called cofinal in K if for every element t of K there exists an element u of J with t ⪯ u.

Lemma 4.3.2 Suppose D = (D, λ) is a (Z × W × Z)-synchronization diagram, and K is a computation of D. Let J be the set of feedback-reachable elements of K. Then J is cofinal in K iff J and K have the same complete trace.

Proof – If J is cofinal in K then it is obvious that J and K have the same complete trace. Conversely, suppose K has complete trace \overline{z}; \overline{w}; \overline{z}. Let t ∈ K be given; then we can choose u ∈ J such that λ(t) ⪯ λ(u). Since K is determinate, t and u must be consistent, and hence λ(t ↑ u) = ϵ. Since u ∈ J, hence is feedback-reachable in K, it then follows easily that t ∨ u = u(t ↑ u) is feedback-reachable in K, hence is in J. Thus, t ∨ u ∈ J is such that t ⪯ t ∨ u, as required.

Theorem 4.4 Suppose D = (D, λ) is a (Z × X, Y × Z)-input/output diagram. Then a set J of elements of D is a behavior of {D}_{._{=}Z} iff there exists a behavior K of D, such that J is the set of feedback-reachable elements of K, and J is cofinal in K.

Proof – (⇒) Suppose J is a behavior of \{D\}_{._{=}Z}, with \overline{λ}(J) = \overline{z}; \overline{x}; \overline{y}; \overline{z}. By Lemma 4.3.1, J extends to a behavior K of D, with complete input trace \overline{z}; \overline{x}. Let J′ denote the feedback-reachable subdiagram of K. Then J ⊆ J′, because every element of J is the result of a computation sequence in J, and J ⊆ K means that every computation sequence in J is a feedback computation sequence in K. Also, J′ ⊆ J, because each element of a feedback computation sequence in K is consistent with J, and has input trace a prefix of \overline{x}, hence is in J because J is a behavior of \{D\}_{._{=}Z}. Thus J = J′.

We claim that J is cofinal in K. To establish this, we show by induction on n, that if t is a element of K, and t is the result t_{n} of a computation sequence t_{0} ≺_{1} t_{1} ≺_{1} … ≺_{1} t_{n} for K, then there exists an element u_{n} of J with t_{n} ⪯ u_{n}.

In the basis case, we have t_{0} = ⊥, so we may take u_{0} = ⊥.

For the induction step, suppose we have established the result for n, and consider the case of n + 1. Then t is the result t_{n+1} of a computation sequence t_{0} ≺_{1} t_{1} ≺_{1} … ≺_{1} t_{n+1} of K. Applying the induction hypothesis to the computation sequence t_{0} ≺_{1} t_{1} ≺_{1} … ≺_{1} t_{n}, we obtain an element u_{n} of J with t_{n} ⪯ u_{n}. Let v = t_{n+1} ↑ t_{n}, then v is a transition of D by definition of a computation sequence. (See Figure 5.) Now, λ_{Z}^{in}(t_{n+1}) ⪯ \overline{z}, because t_{n+1} ∈ K and \overline{λ}_{Z}^{in}(K) = \overline{z}. Since we also have \overline{λ}_{Z}^{in}(J) = \overline{z}, and u_{n} is an element of J, there must exist an element u′_{n} of J, with u_{n} ⪯ u′_{n} and λ_{Z}^{in}(t_{n+1}) ⪯ λ_{Z}^{in}(u′_{n}). Let v′ = v ↑ (u′_{n} ↑ t_{n}); then λ_{Z}^{in}(v′) = ϵ. Moreover, v′ is a transition of D because v is. Let v′′ be the pure-input transition of D with dom(v′′) = dom(v′) and λ^{in}(v′′) = λ_{Z}^{out}(v′); ϵ_{X}. Let w = v′ ∨ v′′, which exists by Theorem 4.1. Let u_{n+1} = u′_{n}w, then u_{n+1} is feedback-reachable, and t_{n+1} ⪯ u_{n+1}.

[figure: u_{n}; u′_{n}; u_{n+1}; v′′; v′; w; t_{n}; t_{n+1}; v]

Figure 5: Proof of Theorem 4.4

To complete the induction step, it remains to be shown that u_{n+1} ∈ J. It suffices, since J is a behavior of \{D\}_{._{=}Z}, to show that λ_{X}(u_{n+1}) ⪯ \overline{x} and that u_{n+1} is consistent with J. That u_{n+1} is consistent with J is clear, since u_{n+1} = t_{n+1} ∨ u′_{n}v′′, and both t_{n+1} and u′_{n}v′′ are consistent with J. Also, λ_{X}(u_{n+1}) ⪯ \overline{x} holds, since λ_{X}(u_{n+1}) = λ_{X}(t_{n+1} ∨ u′_{n}v′′) = λ_{X}(t_{n+1}) ∨ λ_{X}(u′_{n}), and both t_{n+1} and u′_{n} are in K.

(⇐) Suppose K is a behavior of D. Let J be the set of feedback-reachable elements of K, and suppose J is cofinal in K. Then J and K have the same complete input trace, say \overline{z}; \overline{x}, with respect to λ. We claim that J is a behavior of {D}_{._{=}Z}; that is, J is maximal among all computations J′ of \{D\}_{._{=}Z} with \overline{λ}_{X}(J′) = \overline{x}. To show this, we show that if t is a feedback-reachable element of D, consistent with J, and such that λ_{X}(t) ⪯ \overline{x}, then t ∈ K. It then follows that t ∈ J because J is the feedback-reachable subdiagram of K.

We proceed by induction on the length n of a feedback computation sequence t_{0} ≺_{1} t_{1} ≺_{1} … ≺_{1} t_{n} for D, with result t.

In the basis case, we have t = t_{0} = ⊥, hence t ∈ K.

For the induction step, suppose we have shown the result for n, and consider the case of n + 1. Then t is the result t_{n+1} of a feedback computation sequence t_{0} ≺_{1} t_{1} ≺_{1} … ≺_{1} t_{n+1}, and t is consistent with J. By the induction hypothesis, t_{n} ∈ K. Let u = t_{n+1} ↑ t_{n}, then u is a transition of D and we have λ_{Z}^{in}(t_{n+1}) = λ_{Z}^{out}(t_{n+1}), by definition of a feedback computation sequence.

Now, u has a decomposition u = v ∨w, where v is the pure-input transition of D with dom(v) = dom(u) and λ^{in}(v) = λ_{Z}^{in}(u); ϵ_{X}. Then t_{n}w is an element of D that is consistent with J, and has the property λ_{Z}^{in}(t_{n}w) = λ_{Z}^{in}(t_{n}) ⪯ \overline{z}. Since J is cofinal in K and t_{n}w is consistent with J, we must have t_{n}w consistent with K, and hence in K, because K is a behavior. Thus, λ_{Z}^{in}(t_{n+1}) = λ_{Z}^{out}(t_{n+1}) = λ_{Z}^{out}(t_{n}u) = λ_{Z}^{out}(t_{n}w) ⪯ \overline{z}. But then t_{n+1} must be in K, since it is consistent with J, hence with K, we have λ_{Z}^{in}(t_{n+1}) ⪯ \overline{z}, and K is a behavior.

4.4 Histories

An (X, Y)-history is a nonempty, join-closed, and directed subset H of X × Y, with the following additional property: for each x; y ∈ H, there exists a sequence

ϵ_{X}; ϵ_{Y} = x_{0}; y_{0} ⪯ x_{1}; y_{1} ⪯ … ⪯ x_{n}; y_{n} = x; y,

such that for each k with 0 ≤ k < n, the trace x_{n}; y_{n+1} is in H. We call such a sequence a computation sequence for H, and the trace x; y its result. If H is an (X, Y)-history, then the ideal \overline{x}; \overline{y} = ⋁ H ∈ \overline{X} × \overline{Y} is called the complete trace of H, with \overline{x} called the complete input trace and \overline{y} called the complete output trace.

If J is a behavior of an (X, Y)-input/output diagram, then it is easy to see from the properties of such diagrams that the history λ(J) of J is, in fact, an (X, Y)-history.

Suppose H is a (Z ×X, Y ×Z)-history. A feedback computation sequence for H is a computation sequence

z_{0}; x_{0}; y_{0}; z_{0} ⪯ z_{1}; x_{1}; y_{1}; z_{1} ⪯ … ⪯ z_{n}; x_{n}; y_{n}; z_{n},

for H. If z; x; y; z is the result z_{n}; x_{n}; y_{n}; z_{n} of a feedback computation sequence for H, then we say that z; x; y; z is feedback-reachable in H. It is easy to see that the set of all x; y; z ∈ X × Y × Z such that z; x; y; z is feedback-reachable in H is an (X, Y × Z)-history, and we denote it by {H}_{Z} .

Lemma 4.4.1 Suppose D = (D, λ) is a (Z × X, Y × Z)-input/output diagram. If H is the history of a behavior K of D, then {H}_{Z} is the history of the set of feedback-reachable elements of K.

Proof – Let J be the set of feedback-reachable elements of K, and let G = {H}_{Z} .

To see that the history of J is a subset of G, suppose x; y; z is in the history of J. Then z; x; y; z is the trace of the result t_{n} of a feedback computation sequence t_{0} ≺_{1} t_{1} ≺_{1} … ≺_{1} t_{n} for K. Let z_{k}; x_{k}; y_{k}; z_{k} be the trace of t_{k}, for each k. We claim that the sequence

z_{0}; x_{0}; y_{0}; z_{0} ⪯ z_{1}; x_{1}; y_{1}; z_{1} ⪯ … ⪯ z_{n}; x_{n}; y_{n}; z_{n}

is a feedback computation sequence for H, thus showing that x; y; z = x_{n}; y_{n}; z_{n} ∈ {H}_{Z} . We show this as follows: Let u_{k} = t_{k+1} ↑ t_{k}; then u_{k} is a transition of D. By the properties of input/output diagrams, we may write u_{k} = v_{k} ∨w_{k}, where v_{k} is the pure-input transition of D with dom(v_{k}) = dom(u_{k}) and trace λ^{in}(u_{k}); ϵ_{Y ×Z}. Then w_{k} has trace ϵ_{Z×X}; λ^{out}(u_{k}), so t_{k}w_{k} has trace z_{k}; x_{k}; y_{k+1}; z_{k+1}. Since t_{k}w_{k} ⪯ t_{k+1} ∈ K, we must have t_{k}w_{k} ∈ K, and hence z_{k}; x_{k}; y_{k+1}; z_{k+1} ∈ H. But this is exactly what is required to show that the z_{k}; x_{k}; y_{k}; z_{k} form a feedback computation sequence for H.

Conversely, if x; y; z ∈ G, then z; x; y; z is the result z_{n}; x_{n}; y_{n}; z_{n} of a feedback computation sequence

z_{0}; x_{0}; y_{0}; z_{0} ⪯ z_{1}; x_{1}; y_{1}; z_{1} ⪯ … ⪯ z_{n}; x_{n}; y_{n}; z_{n}

for H. We claim that there exists a feedback computation sequence

t_{0} ≺_{1} t_{1} ≺_{1} … ≺_{1} t_{n}

for K, and nonnegative integers 0 = m_{0}, m_{1},…, m_{n} = n, such that z_{k}; x_{k}; y_{k}; z_{k} is the trace of t_{m_{k}}, for each k.

The construction proceeds by induction on k. For the basis case (k = 0), we take m_{0} = 0, and t_{0} = ⊥. Suppose now, for some k with 0 ≤ k < n, that we have constructed m_{k} and t_{0} ≺_{1} t_{1} ≺_{1} … ≺_{1} t_{m_{k}} ∈ K, such that t_{m_{k}} has trace z_{k}; x_{k}; y_{k}; z_{k}. By definition of a feedback sequence, we know that z_{k}; x_{k}; y_{k+1}; z_{k+1} is in H, hence is the trace of an element u_{k} of K. Without loss of generality, we may assume that t_{k} ⪯ u_{k}. Thus, we may obtain v_{0} ≺_{1} v_{1} ≺_{1} … ≺_{1} v_{p} ∈ K, with v_{0} = t_{m_{k}} and v_{p} = u_{k}. For 0 ≤ i ≤ p, let w_{i} be the pure-input element of D with trace λ_{Z}^{out}(v_{i}); ϵ_{X}; ϵ_{Y}; ϵ_{Z}. Note that then v_{i} ∨ w_{i} exists for each i with 0 ≤ i ≤ p, and we have v_{i} ∨ w_{i} ≺_{1} v_{i+1} ∨ w_{i+1} for each i with 0 ≤ i < p, by the properties of input/output diagrams. Moreover, v_{i} ∨ w_{i} ∈ K for each i with 0 ≤ i ≤ p because v_{i} ∈ K and λ^{in}(w_{i}) ⪯ z_{k+1}, which is a prefix of the complete input trace of H, hence of K. Let m_{k+1} = m_{k} + p, and let t_{m_{k}+i} = v_{i} ∨ w_{i} for each i with 0 < i ≤ p. Then

t_{0} ≺_{1} t_{1} ≺_{1} … ≺_{1} t_{m_{k}} ≺_{1} t_{m_{k}+1} ≺_{1} … ≺_{1} t_{m_{k+1}}

is the required feedback computation sequence for K, thus completing the induction step and the proof.

Theorem 4.5 Suppose D = (D, λ) is a (Z ×X, Y ×Z)-input/output diagram. Then an (X, Y ×Z)- history G, with complete trace \overline{x}; \overline{y}; \overline{z}, is a history of \{D\}_{._{=}Z} iff G = \{H\}_{Z} for some history H of D with complete trace \overline{z}; \overline{x}; \overline{y}; \overline{z}.

Proof – If G is a history of \{D\}_{._{=}Z}, with complete trace \overline{x}; \overline{y}; \overline{z}, then G is the history of some behavior J of {D}_{._{=}Z}. By Theorem 4.4, there exists a behavior K of D such that J is the set of feedback-reachable elements of K, and J is cofinal in K. Let H be the history of K; then H has complete trace \overline{z}; \overline{x}; \overline{y}; \overline{z} by Lemma 4.3.2. Moreover, G = \{H\}_{Z} by Lemma 4.4.1.

Conversely, suppose G = \{H\}_{Z} for some history H of D. Suppose G has complete trace \overline{x}; \overline{y}; \overline{z} and H has complete trace \overline{z}; \overline{x}; \overline{y}; \overline{z}. Then H is the history of some behavior K of D. By Lemma 4.4.1, G is the history of the set J of feedback-compatible elements of K, from which it follows by Lemma 4.3.2 that J is cofinal in K. Thus, J is a behavior of {D}_{._{=}Z}, and G is a history of {D}_{._{=}Z}.

4.5 Scenarios

An (X, Y)-Kahn function is a continuous function ϕ from an initial segment (a nonempty, downwardclosed, and directed-complete subset) of dom(ϕ) of \overline{X} to \overline{Y}. If dom(ϕ) = \overline{X}, then ϕ is called total. If U is an initial segment of \overline{X}, then the set of all (X, Y)-Kahn functions with domain U forms a directed-complete poset under the argumentwise ordering. We use the traditional notations ⊑ and ⊔ to denote this ordering and the associated supremum operation, respectively.

Suppose ϕ is a (Z × X, Y × Z)-Kahn function. We say that ϕ is feedback-compatible if \overline{y}; \overline{z} ∈ ϕ(dom(ϕ)) implies \overline{z}; \overline{x} ∈ dom(ϕ) for all \overline{x} ∈ dom(ϕ). Note that total (Z ×X, Y ×Z)-Kahn functions are always feedback-compatible.

If ϕ is feedback compatible, then define the feedback functional Φ associated with ϕ, to be the functional

Φ : [π\overline{X}(dom(ϕ)) → \overline{Y} × \overline{Z}] → [π\overline{X}(dom(ϕ)) → \overline{Y} × \overline{Z}]

that takes each (X, Y ×Z)-Kahn function ψ : π\overline{X}(dom(ϕ)) → \overline{Y} ×\overline{Z} to an (X, Y ×Z)-Kahn function

Φ(ψ) = ϕ ∘ ((π\overline{Z} ∘ ψ) × id_{dom(ψ)}).

The feedback-compatibility of ϕ guarantees that Φ is well-defined, and it is easily verified that Φ is continuous. Define {ϕ}_{Z} to be the least fixed point of Φ.

Lemma 4.5.1 If ϕ is a feedback-compatible (Z ×X, Y ×Z)-Kahn function, and Φ is the associated feedback functional, then

{ϕ}_{Z} = ⨆_{k=0}^{∞} ϕ^{(k)},

where ϕ^{(0)} is the identically ϵ function, and ϕ^{(k+1)} = Φ(ϕ^{(k)}) for each k ≥ 0.

Proof – Standard.

An (X, Y)-scenario is an (X, Y)-Kahn function whose domain is directed. The pair

(⋁ dom(ϕ)); (⋁ ϕ(dom(ϕ)))

is called the complete trace of ϕ, with ⋁ dom(ϕ) called the complete input trace and ⋁ ϕ(dom(ϕ)) called the complete output trace.

Suppose H is an (X, Y)-history, with complete trace \overline{x}_{0}; \overline{y}_{0}. Then H determines an (X, Y)- scenario

ϕ : \{\overline{x} ∈ \overline{X} : \overline{x} ⪯ \overline{x}_{0}\} → \overline{Y} ,

according to the definition

ϕ(\overline{x}) = ⋁\{y ∈ Y : ∃x; y ∈ H, x ⪯ \overline{x}\}.

Intuitively, a scenario represents some information about how inputs precede outputs in a single computation. That is, ϕ(\overline{x}) = \overline{y} iff, in a single computation with scenario ϕ, the input trace \overline{x} “enables” the output trace \overline{y} in the sense that it is possible for arbitrarily large finite prefixes y of \overline{y} to be generated in response to inputs that are finite prefixes of \overline{x}.

Brock and Ackerman [7, 6] have defined “scenario” based on the notion of when finite inputs “must precede” finite outputs. The two notions of scenario are evidently equivalent, since in a computation with complete trace \overline{x}_{0}; \overline{y}_{0}, \overline{x} “enables” \overline{y} iff every finite prefix x of \overline{x}_{0} that “must precede” some finite prefix y of \overline{y} is already a prefix of \overline{x}, and x “must precede” y iff for all \overline{x} ⪯ \overline{x}_{0}, if \overline{x} “enables” y, then x ⪯ \overline{x}. We find that a definition of scenario based on “enables,” rather than “must precede,” is easier to relate to Kahn’s continuous function model of processes.

Lemma 4.5.2 Suppose H is a (Z × X, Y × Z)-history, with scenario ϕ. Let G = {H}_{Z} , and let ψ be the scenario of G. If ϕ is feedback-compatible, then ψ = {ϕ}_{Z} .

Proof – We show (⇒) ψ(\overline{x}) ⪯ \{ϕ\}_{Z} (\overline{x}) for all \overline{x} ∈ \overline{X}, and (⇐) ψ is a fixed point of the feedback functional associated with ϕ.

(⇐) Suppose ψ(\overline{x}) = \overline{y}; \overline{z}. Let y; z be an arbitrary finite prefix of \overline{y}; \overline{z}. Then there exists a feedback computation sequence

z_{0}; x_{0}; y_{0}; z_{0} ⪯ z_{1}; x_{1}; y_{1}; z_{1} ⪯ … ⪯ z_{n}; x_{n}; y_{n}; z_{n}

for H, such that x_{n} ⪯ \overline{x} and y; z ⪯ y_{n}; z_{n}. A simple induction shows that for each k with 0 ≤ k < n we have

y_{k+1}; z_{k+1} ⪯ ϕ^{(k+1)}(\overline{x}),

where ϕ^{(k)} is as defined in Lemma 4.5.1. It follows that y; z ⪯ \{ϕ\}_{Z} (\overline{x}). Since y; z was an arbitrary finite prefix of \overline{y}; \overline{z}, it follows that \overline{y}; \overline{z} ⪯ \{ϕ\}_{Z} (\overline{x}), as was to be shown.

(⇒) Since we already know that ψ ⊑ {ϕ}_{Z} , to show that ψ is a fixed point of the feedback functional Φ associated with ϕ, it remains only to show that Φ(ψ) ⊑ ψ. That is, we must show that ϕ((π\overline{Z}(ψ(\overline{x})); \overline{x}) ⪯ ψ(\overline{x}) for all \overline{x} ∈ \overline{X}. To show this, it suffices to show that for all x; y; z ∈ G, if y′; z′ is a finite prefix of ϕ(z; x), then there exists x; y′′; z′′ ∈ G, such that y′ ⪯ y′′ and z′ ⪯ z′′.

Now, if x; y; z ∈ G, then x; y; z is the result x_{n}; y_{n}; z_{n} of a feedback computation sequence

z_{0}; x_{0}; y_{0}; z_{0} ⪯ z_{1}; x_{1}; y_{1}; z_{1} ⪯ … ⪯ z_{n}; x_{n}; y_{n}; z_{n}

for H. If y′; z′ ⪯ ϕ(z; x), then z; x; y′′; z′′ ∈ H for some y′′ ∈ Y and z′′ ∈ Z with y′ ⪯ y′′ and z′ ⪯ z′′. This shows that

z_{0}; x_{0}; y_{0}; z_{0} ⪯ z_{1}; x_{1}; y_{1}; z_{1} ⪯ … ⪯ z_{n}; x_{n}; y_{n}; z_{n} ⪯ z′′; x; y′′; z′′

is a feedback sequence for H. It follows that x; y′′; z′′ is in G.

Theorem 4.6 Suppose D = (D, λ) is a (Z ×X, Y ×Z)-input/output diagram. Then an (X, Y ×Z)- scenario ψ, with complete trace \overline{x}; \overline{y}; \overline{z}, is a scenario of \{D\}_{._{=}Z} iff ψ = \{ϕ\}_{Z} , where ϕ is a scenario of D with complete trace \overline{z}; \overline{x}; \overline{y}; \overline{z}.

Proof – If ψ is a scenario of \{D\}_{._{=}Z}, with complete trace \overline{x}; \overline{y}; \overline{z}, then it is the scenario of some history G of {D}_{._{=}Z}, with the same complete trace. By Theorem 4.5 there exists a history H of D, with complete trace \overline{z}; \overline{x}; \overline{y}; \overline{z}, such that G = \{H\}_{Z} . If ϕ is the scenario of H, then ϕ is obviously feedback-compatible, and ψ = {ϕ}_{Z} by Lemma 4.5.2.

Conversely, if ψ = \{ϕ\}_{Z} has complete trace \overline{x}; \overline{y}; \overline{z}, where ϕ is a scenario of D with complete trace \overline{z}; \overline{x}; \overline{y}; \overline{z}, then ϕ is the scenario of some history H of D, and is clearly feedback-compatible. By Theorem 4.5, {H}_{Z} is a history of {D}_{._{=}Z}, and by Lemma 4.5.2, {H}_{Z} has scenario ψ.

4.6 Input/Output Relations

Given an (X, Y)-input/output diagram D, define the input/output relation Reln(D) of D to be the set of all complete traces of scenarios of D.

Lemma 4.6.1 Suppose D is an (X, Y)-input/output diagram. Then Reln(D) is:

• (Total) For all \overline{x} ∈ \overline{X}, there exists \overline{y} ∈ \overline{Y} such that \overline{x}; \overline{y} ∈ Reln(D).

• (Monotone) If \overline{x}; \overline{y} ∈ Reln(D), and \overline{x} ⪯ \overline{x}′, then there exists \overline{y}′, with \overline{y} ⪯ \overline{y}′, such that \overline{x}′; \overline{y}′ ∈ Reln(D).

Moreover, if D is a Kahn diagram, then Reln(D) is (the graph of) a total (X, Y)-Kahn function, and the scenarios of D are exactly the restrictions of Reln(D) to directed initial segments of \overline{X}.

Proof – Straightforward from Lemma 4.3.1.

If R ⊆ \overline{X} × \overline{Y}, then let R_{fin} denote the set of finite prefixes of elements of R. The relation R is called continuous if, for all \overline{x} ∈ \overline{X}, whenever U is a maximal directed subset of

\{y ∈ Y : ∃x ⪯ \overline{x}, x; y ∈ R_{fin}\},

then \overline{x}; (⋁ U) ∈ R. Note that if R is the graph of a total (X, Y)-Kahn function, then R is continuous.

Lemma 4.6.2 Suppose R ⊆ \overline{X} × \overline{Y} is total, monotone, and continuous. Then there exists an (X, Y)-machine M with R as its input/output relation.

Proof – Define the machine M as follows:

• Proper states: all elements x; y ∈ R_{fin}. Take ϵ_{X}; ϵ_{Y} as the start state.

• Proper transitions: all pairs (x; y, v) ∈ R_{fin} × Y, such that x; yv ∈ R_{fin}. Define dom(x; y, v) = x; y and cod(x; y, v) = x; yv. Take the transitions (x; y, ϵ_{Y}) as identities.

• Residual: define (x; y, v) and (x; y, v′) to be consistent iff v and v′ are consistent, in which

case define

(x; y, v) ↑ (x; y, v′) = (x; yv′, v ↑ v′).

• Output map: define λ(x; y, v) = v.

• Input map: define δ_{x′}(x; y, v) = (xx′; y, v).

It is not difficult to verify that M is an (X, Y)-machine. Moreover, a set H ⊆ X × Y is the history of a behavior of M exactly when π_{X}(H) is an ideal \overline{x} of X, and π_{Y} (H) is a maximal directed subset of

\{y ∈ Y : ∃x ⪯ \overline{x}, x; y ∈ R_{fin}\}.

Since R is continuous, it follows that M has R as its input/output relation.

Lemma 4.6.3 Suppose ϕ is a total (Z × X, Y × Z)-Kahn function with complete trace \overline{z}; \overline{x}; \overline{y}; \overline{z}, ψ is the restriction of ϕ to prefixes of \overline{z}; \overline{x}, and \{ψ\}_{Z} has trace \overline{x}; \overline{y}; \overline{z}. Then \{ψ\}_{Z} is the restriction of \{ϕ\}_{Z} to prefixes of \overline{x}.

Proof – A simple induction shows that for each k ≥ 0 the scenario ψ^{(k)} is the restriction to prefixes of \overline{x} of ϕ^{(k)}, where ψ^{(k)} and ϕ^{(k)} are as defined in Lemma 4.5.1. From this, the result follows by continuity of restriction.

Lemma 4.6.4 Suppose ϕ is a total (Z × X, Y × Z)-Kahn function. Then \{ϕ\}_{Z} (\overline{x}) = \overline{y}; \overline{z} iff the restriction ψ of ϕ to prefixes of \overline{z}; \overline{x} is feedback-compatible, and \{ψ\}_{Z} has complete trace \overline{x}; \overline{y}; \overline{z}.

Proof – Suppose \{ϕ\}_{Z} (\overline{x}) = \overline{y}; \overline{z}. Let ψ be the restriction of ϕ to prefixes of \overline{z}; \overline{x}. Then ϕ(\overline{z}; \overline{x}) = \overline{y}; \overline{z}, so ψ is feedback-compatible. By Lemma 4.6.3, \{ψ\}_{Z} is the restriction of \{ϕ\}_{Z} to prefixes of \overline{x}, hence \overline{x}; \overline{y}; \overline{z} is the complete trace of \{ψ\}_{Z} .

Conversely, suppose the restriction ψ of ϕ to prefixes of \overline{z}; \overline{x} is feedback-compatible, and \{ψ\}_{Z} has trace \overline{x}; \overline{y}; \overline{z}. By Lemma 4.6.3, \{ψ\}_{Z} is the restriction to prefixes of \overline{x} of \{ϕ\}_{Z} . Since \{ψ\}_{Z} has complete trace \overline{x}; \overline{y}; \overline{z}, it follows that (\{ψ\}_{Z} )(\overline{x}) = \overline{y}; \overline{z}, and hence \{ϕ\}_{Z} (\overline{x}) = \overline{y}; \overline{z}.

Theorem 4.7 (Kahn Principle) Suppose D is a (Z × X, Y × Z)-Kahn diagram. Then

Reln({D}_{._{=}Z}) = {Reln(D)}_{Z} .

Proof – By definition of Reln, \overline{x}; \overline{y}; \overline{z} ∈ Reln(\{D\}_{._{=}Z}) iff there exists a scenario of \{D\}_{._{=}Z} with complete trace \overline{x}; \overline{y}; \overline{z}. By Lemma 4.6.4, this is true iff there exists a feedback-compatible scenario ϕ of D, with trace \overline{z}; \overline{x}; \overline{y}; \overline{z}, such that \{ϕ\}_{Z} has trace \overline{x}; \overline{y}; \overline{z}. By Lemma 4.6.3, this is true iff the restriction ϕ of Reln(D) to prefixes of \overline{z}; \overline{x} is feedback-compatible, has trace \overline{z}; \overline{x}; \overline{y}; \overline{z}, and \{ϕ\}_{Z} has trace \overline{x}; \overline{y}; \overline{z}. By Lemma 4.6.4, this is true iff \overline{x}; \overline{y}; \overline{z} ∈ \{Reln(D)\}_{Z} .

5 Discussion

The author was led to define concurrent transition systems because of the apparent difficulty of establishing relationships between operational and denotational models of concurrent computation. The problems, of finding a natural characterization of a large class of dataflow-like processes with functional behavior, and of proving that the feedback operation on such processes satisfies the Kahn Principle, served as primary motivating examples. Before trying the concurrent transition system approach reported here, an attempt was made to try to solve these problems using a model of processes based on ordinary (nondeterministic) labeled transition systems. Although other researchers have shown how various parallel composition operations of CCS and CSP can be given reasonably natural definitions in such a model, our situation is somewhat different, because we have drawn a distinction between input and output, and because we are interested in infinite computations as well as finite ones.

There were two difficulties that seemed inherent in an approach based on ordinary transition systems. The first difficulty arose from the fact that, although we are interested in infinite computations of a system, we are only interested in those infinite computations that are “completed” in the sense that each process produces all the output implied by the input it has received. The usual method of handling this is to distinguish between “fair” and “unfair” computations. This approach leads to technical problems, as pointed out in Section 1. The second difficulty with the nondeterministic transition system approach was that the notion of “primitive” or “atomic” steps of a process seemed not to behave smoothly with respect to the feedback operation. One can see the problem by considering an “identity” process, which simply passes its input through unchanged to its output. One would like to have the atomic steps of this process correspond to the receipt of input and the issuance of output. Now, consider what happens when the output of the identity process is fed back to its input. The “intuitively correct” result of this construction is a process that produces no output. It seems most natural to define the atomic steps of the fed-back identity to correspond to the simultaneous issuance of output and the absorption of that output as feedback input. However, the question arises of how to define the construction in such a way that “nonintuitive” computations, in which output is produced, are avoided.

In retrospect, concurrent transition systems seem to provide exactly the right structure to circumvent the difficulties mentioned above. The fairness problem is solved, in the concurrent transition system approach, by replacing the notion “fair computation sequence” by the more convenient notion “behavior” or “maximal ideal.” The atomic step problem is solved by restricting attention to a class of processes whose transitions have pure-input/output decompositions. In essence, the existence of such decompositions means that there is an inherent delay of one atomic step between input and output, and this allows nonintuitive computations to be avoided. The existence of pure-input/output decompositions is easily and naturally expressed with concurrent transition systems, whereas it is not clear how the same could be done with ordinary transition systems.

5.1 Related Work

As mentioned in Section 2, the defining axioms for concurrent transition systems are satisfied by the derivation relation of the λ-calculus, and the computation category construction is an abstract version of a construction that has already been found useful in that setting. The goal of the λcalculus work [22, 5], and the extension of this work to term-rewriting systems [15], is to try to find reduction strategies that are optimal in the sense that only redexes that are “needed” are contracted, and each needed redex is contracted only once. The main theorem one tries to prove is that every derivation is in a sense equivalent to an optimal derivation. To make the notions “needed redex” and “equivalent derivations” precise, the “residual” operation is defined. Intuitively, the residual operation serves to keep track of what happens to one redex when others are contracted. A redex is “needed” if it (or its residuals) must be contracted in any derivation sequence that leads to a normal form. Two derivation sequences are regarded as equivalent iff the same set of reductions is performed in each, where the notion “same set of reductions” is interpreted modulo residuals. The residual operation for CTS’s was introduced for an essentially similar purpose: to keep track of what happens to a particular atomic transition (say for one process) of a system, when other atomic steps (say for other, concurrently executing processes) are executed. Two computation sequences are regarded as equivalent representatives of the same concurrent computation if they contain the “same set of atomic steps.”

A difference between the CTS and and term-rewriting settings are that in the former we regard inconsistent pairs of coinitial transitions as meaningful, whereas in the latter one is usually interested only in confluent or Church-Rosser systems. Also, with CTS’s we are interested in nonterminating computations, whereas in the rewriting situation one is primarily interested in terminating or normalizing computations.

Several authors have investigated algebraic structures for modeling concurrency that seem related to concurrent transition systems. Winskel [42] defines the notion of a “synchronization tree,” which is a (possibly infinite) tree whose arcs are labeled with elements of a “synchronization algebra.” In [41], labeled event structures [29] are used in place of labeled trees. Using various synchronization algebras, Winskel is able to show several notions of parallel composition from CCS and CSP to be special cases of a single definition. It is clear that Winskel’s trees are special cases of our computation diagrams. Also, Winskel’s synchronization algebras are rather similar to our trace algebras. Specifically, a trace algebra can be regarded as a synchronization algebra if we identify Winskel’s ∗ with our ϵ, and Winskel’s operation • with our operation ∨. It is not possible, in general, to regard a synchronization algebra as a trace algebra, since the latter are somewhat more highly structured. We use trace algebras to label the transitions of CTS’s in essentially the same way as Winskel uses synchronization algebras to label trees. However, we find it an advantage that trace algebras are a particular kind of CTS. By regarding Winskel’s synchronization trees as special cases of our synchronization diagrams, essentially the same parallel composition constructions can be carried out in our framework.

Event structures and CTS’s can be related as follows: Given a CTS with start state (C, ι), it is straightforward to make the set of elements of Diag(C, ι) into an event structure by defining the “consistent” sets of elements to be the finite sets that are consistent in the sense we have defined here, and defining a consistent set T to “enable” an element t iff there is a subset U of T such that (⋁ U) ≺_{1} t. Conversely, the set of “configurations” of an event structure is a partially ordered set in which every finite subset with an upper bound has a least upper bound, and hence is easily made into a complete CTS, by taking configurations as proper states and the ordering relation as the set of proper transitions. In a sense, CTS’s can be thought of as a somewhat more primitive operational model than event structures, since in the former one is free to designate the set of states, whereas in the latter, states are always obtained as configurations.

Main and Benson [25] use ideas from multilinear algebra to model nondeterministic and concurrent processes without iteration or recursion. An important role is played by “positive semi-rings,” whose formal properties are closely related the trace algebras used in the present paper. Essentially, a trace algebra Z is a positive semiring in which a left-cancellation law holds for multiplication, and in which there is a further connection between addition and multiplication; namely, addition is least upper bound with respect to the prefix order induced by multiplication.

Arbib and Manes [2] have developed a categorical theory of automata, which generalizes several classical situations. They generalize the notion of an “action” or “transition map” as a function δ : Q × X → Q to the notion of a “dynamics,” which is a morphism δ : X(Q) → Q, where Q is an object of an arbitrary category K, and X is an endofunctor of K. Arbib and Manes’ theory is applied to “port automata” in [37]. In that paper, concurrency is modeled by interleaving, and the issue of fair infinite computations is not considered. It would be nice if the definition of “action” we have given here could be shown to be a special case of Arbib and Manes’ dynamics. However, we have yet to identify the proper endofunctor X of CTS to achieve this goal. The product-forming functor (- × X) does not yield a general enough class of dynamics.

The work of Winkowski [39, 40], is motivated by considerations in the theory of Petri nets. In [39], Winkowski defines the notion of a “behavior algebra,” which is a category equipped with (among other things) a partial binary operation + on the arrows of the category, representing independent concurrent composition. The properties of a behavior algebra are similar in many respects to those enjoyed by the computation categories defined in this paper. However, the theory of computation categories appears to be somewhat simpler than that of behavior algebras, primarily due to the fact that in computation categories there is a connection between concurrency and pushouts. The existence of this connection means that the concurrency information in a computation category can be obtained entirely from the structure of the category itself, without requiring the specification of additional information such as the operation + of a behavior algebra. It also makes possible the definition of computations as ideals, which is substantially simpler than the definition of “histories” given by Winkowski.

Staples and Nguyen [34] define a dataflow-like model in which a process is represented by a partially ordered set whose elements are labeled by “histories” (“traces,” in our terminology). Processes are required to satisfy a collection of axioms, which appear related to the properties enjoyed by synchronization diagrams in the present paper. It would seem that by taking an input/output synchronization diagram and equipping the cpo of its computations with the map that takes each computation to its complete trace, one obtains a structure that is similar to the processes of Staples and Nguyen, both in formal properties and in intuitive content. However, there is not an exact correspondence, since one of Staples and Nguyen’s axioms concerns greatest lower bounds, whose existence we have not found it necessary to assume.

Labella and Pettorossi [21] have given categorical characterizations of various operations of CCS and CSP. In their approach they take as given a semantics of these languages defined in terms of equivalence classes of trees. A suitable definition of morphism makes the set of all these equivalence classes into a category, in which their characterizations are valid. The characterizations they obtain are not particularly simple, and one is not left with the feeling they are likely to translate to categories obtained from other concurrent programming languages. In contrast, in the present paper we hope that by defining a model in which simple categorical constructions appear to correspond to intuitively meaningful semantic operations on processes, we can use the same model to define the semantics of a number of different concurrent programming languages.

5.2 Directions for Future Research

One obvious avenue for future research is to extend the machine model to include a way of defining machines recursively. Presumably, a recursive definition of an (X, Y)-machine would denote a limit of an inverse system generated by a suitable continuous endofunctor on Mach_{X,Y}. To properly develop this idea, we have to establish that such a limit construction would produce a machine with the intuitively correct set of computations. We also have to establish the continuity of a set of network-building operations, such as the parallel product, relabeling, and feedback operations defined in this paper.

Although the machine model defined here is capable of representing a large class of processes, including processes with functional input output behavior and an “unfair merge” process, it is possible to show that “fair merge” cannot be modeled. In addition, it is impossible to model processes that have “conflicts” or “race conditions” between input and output. An interesting question is whether it is possible to generalize our definitions in a natural way, so that a larger class of processes can be modeled. One way to approach this is to investigate classes of automata obtained by weakening some of the conditions of Theorem 4.1.

In Section 4, we pointed out that the feedback operation on machines, when mapped to automata and synchronization diagrams, could be characterized as right-adjoint to a relabeling functor. The parallel product of automata can also be characterized in a similar way. This phenomenon suggests the idea of defining a “process algebra” to be an (X, Y)-indexed collection of categories Proc_{X,Y}, and to require that operations on processes be defined as adjoints to various naturally occurring functors. The advantages of such an approach include the ability to compare the concrete form taken by the “same operations” in different process algebras, and automatic proofs of continuity of operations arising from the adjoint characterizations. However, it is not clear whether such an approach is feasible, since we do not yet have an adjoint characterization of the feedback operation on machines, nor do we know whether it is possible to impose useful categorical structure on the behavior, history, and input/output relation models.

It would be nice to understand better the relationships between the CTS-based models defined in this paper and other models of concurrency, especially Petri Nets. One question here would be to see how much of the modeling power of Petri Nets is shared by CTS’s, which are somewhat more abstract. Comparisons of input/output automata with labeled transition system models of CCS and CSP would also be useful. An interesting question is how the notion of “bisimulation” [30, 28], which is fundamental for ordinary transition systems, might be reasonably generalized to CTS’s.

Finally, the full abstraction problem for machines remains open. Although we were not able to solve this problem in this paper, we have been able to make the problem more concrete by establishing the existence of a seemingly natural “fully abstract” algebra of processes. Moreover, we feel that the information about the feedback operation we have obtained is likely to be useful in ultimately resolving this important question.

Acknowledgement I am grateful to the anonymous referees for their careful reading and perceptive comments.

References

[1] S. Abramsky. Experiments, powerdomains, and fully abstract models for applicative multiprogramming. In Foundations of Computation Theory, pages 1–13, Springer-Verlag. Volume 158

of Lecture Notes in Computer Science, 1983.

[2] M. A. Arbib and E. G. Manes. Arrows, Structures, and Functors: The Categorical Imperative. Academic Press, 1975.

[3] R. J. Back and N. Mannila. A refinement of Kahn’s semantics to handle nondeterminism and communication. In Proc. ACM Symposium on Principles of Distributed Computing, pages 111– 120, 1982.

[4] H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Volume 103 of Studies in Logic and the Foundations of Mathematics, North-Holland, 1981.

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

[6] J. D. Brock. A Formal Model of Non-Determinate Dataflow Computation. PhD thesis, Massachusetts Institute of Technology, 1983. Available as MIT/LCS/TR-309.

[7] J. D. Brock and W. B. Ackerman. Scenarios: a model of non-determinate computation. In Formalization of Programming Concepts, pages 252–259, Springer-Verlag. Volume 107 of Lecture Notes in Computer Science, 1981.

[8] S. D. Brookes. On the relationship of ccs and csp. In ICALP 83, Springer Verlag, 1983.

[9] S. D. Brookes and W. C. Rounds. Behavioral equivalence relations induced by programming logics. In Proceedings of ICALP 83, 1983.

[10] A. A. Faustini. An operational semantics for pure dataflow. In Automata, Languages, and Programming, 9th Colloquium, pages 212–224, Springer-Verlag. Volume 140 of Lecture Notes in Computer Science, 1982.

[11] I. Guessarian. Algebraic Semantics. Volume 99 of Lecture Notes in Computer Science, Springer Verlag, 1981.

[12] M. Hennessy and R. de Nicola. Testing equivalences for processes. In ICALP 1983, Springer-Verlag. Volume 154 of Lecture Notes in Computer Science, 1983.

[13] H. Herrlich and G. E. Strecker. Category Theory. Sigma Series in Pure Mathematics, Heldermann Verlag, 1979.

[14] C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666– 676, 1978.

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

[16] G. Kahn. The semantics of a simple language for parallel programming. In J. L. Rosenfeld, editor, Information Processing 74, North-Holland, 1974.

[17] G. Kahn and D. B. MacQueen. Coroutines and networks of parallel processes. In B. Gilchrist, editor, Information Processing 77, North-Holland, 1977.

[18] R. M. Keller. Denotational models for parallel programs with indeterminate operators. In E. J. Neuhold, editor, Formal Description of Programming Concepts, pages 337–366, North-Holland. 1978.

[19] R. M. Keller and P. Panangaden. Semantics of networks containing indeterminate operators. In Seminar on Concurrency, pages 479–496, Springer-Verlag. Volume 197 of Lecture Notes in Computer Science, 1984.

[20] J. N. Kok. Denotational semantics of nets with nondeterminism. In ESOP 86, pages 237–249, Springer-Verlag. Volume 213 of Lecture Notes in Computer Science, March 1986.

[21] A. Labella and A. Pettorossi. Categorical models for handshaking communications. In Annales Societatis Mathematicae Polonae. SERIES IV: Fundamenta Informaticae, 1985.

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

[23] S. Mac Lane. Categories for the Working Mathematician. Volume 5 of Graduate Texts in Mathematics, Springer Verlag, 1971.

[24] D. B. MacQueen. Models for Distributed Computing. Technical Report 351, INRIA, 1979.

[25] M. G. Main and D. B. Benson. Functional behavior of nondeterministic and concurrent programs. Information and Control, 62:144–189, 1984.

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

[27] R. Milner. A Calculus of Communicating Systems. Volume 92 of Lecture Notes in Computer Science, Springer Verlag, 1980.

[28] R. Milner. Lectures on a calculus for communicating systems. In Seminar on Concurrency, pages 197–220, Springer-Verlag. Volume 197 of Lecture Notes in Computer Science, 1984.

[29] M. Nielsen, G. Plotkin, and G. Winskel. Petri nets, event structures, and domains, part I. Theoretical Computer Science, 13:85–108, 1981.

[30] D. M. R. Park. Concurrency and automata on infinite sequences. In Theoretical Computer Science, Springer-Verlag. Volume 104 of Lecture Notes in Computer Science, 1981.

[31] D. M. R. Park. The “fairness problem” and nondeterministic computing networks. In Proceedings, 4th Advanced Course on Theoretical Computer Science, Mathematisch Centrum, 1982.

[32] V. R. Pratt. On the composition of processes. In Ninth Annual ACM Symposium on Principles of Programming Languages, pages 213–223, January 1982.

[33] V. R. Pratt. The pomset model of parallel processes: unifying the temporal and the spatial. In Seminar on Concurrency, pages 180–196, Springer-Verlag. Volume 197 of Lecture Notes in Computer Science, July 1984.

[34] J. Staples and V. L. Nguyen. A fixpoint semantics for nondeterministic data flow. Journal of the ACM, 32(2):411–444, April 1985.

[35] E. W. Stark. The Computation Category of a Concurrent Transition System. Technical Report 86/08, State University of New York at Stony Brook Computer Science Dept., May 1986.

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

[37] M. Steenstrup, M. A. Arbib, and E. G. Manes. Port automata and the algebra of concurrent processes. JCSS, 27(1):29–50, 1983.

[38] P. S. Thiagarajan. Elementary net systems. In Advanced Course on Petri Nets, GMD, Bad Honnef, September 1986.

[39] J. Winkowski. An algebraic description of system behaviors. Theoretical Computer Science, 21:315–340, 1982.

[40] J. Winkowski. Behaviors of concurrent systems. Theoretical Computer Science, 12:39–60, 1980.

[41] G. Winskel. Event structures. In Advanced Course on Petri Nets, GMD, Bad Honnef, September 1986.

[42] G. Winskel. Synchronization trees. Theoretical Computer Science, 34:33–82, 1984.