On the Relations Computable by a Class of Concurrent Automata

Eugene W. Stark^{∗}

Department of Computer Science State University of New York at Stony Brook

Stony Brook, NY 11794 USA

Abstract

We consider monotone input/output automata, which model a usefully large class of dataflow networks of indeterminate (or nonfunctional) processes. We obtain a characterization of the relations computable by these automata, which states that a relation R : X → 2^{Y} (viewed as a “nondeterministic function”) is the input/output relation of an automaton iff there exists a certain kind of Scott domain D, a continuous function F : X → [D → Y] and a continuous function G : X → P(D), such that R(x) = F (x)†(G(x)) for all inputs x ∈ X. Here P denotes a certain powerdomain operator, and † denotes the pointwise extension to the powerdomain of a function on the underlying domain. An attractive feature of this result is that it specializes to two subclasses of automata, determinate automata, for which G is single-valued, and semi-determinate automata, for which G is a constant function. A corollary of the latter result is the impossibility of implementing “angelic merge” by a network of determinate processes and “infinity-fair merge” processes.

1 Introduction

Dataflow networks (see, e.g. [3, 4, 6, 7, 8]) consist of a collection of concurrently executing sequential processes that communicate by transmitting sequences or “streams” of “value tokens” over FIFO communication channels. Typically, a network is described as a directed graph, whose nodes are processes and whose arcs are communication channels. Each channel serves to connect an “output port” of one process to an “input port” of another process. “Determinate” (or functional) networks were first studied by Kahn [7], who gave an elegant fixed-point principle for determining the function computed by a network from the functions computed by the components. “Indeterminate” (or non-functional) networks remain less well understood, despite extensive study. An interesting class of indeterminate processes are the “merge” processes, which shuffle together sequences of values from two input channels onto a single output channel. Fair merge (fmerge) guarantees that every value arriving on either of the two inputs will eventually be transmitted to the output. Angelic merge (amerge) guarantees to transmit all values from one input channel only in case the sequence of values arriving on the other channel is finite. Infinity-fair merge (imerge) guarantees to transmit all values from one input channel only in case the sequence of values arriving on the other channel is infinite.

In previous papers [15, 21, 22], we identified the networks of “monotone” processes as an interesting and particularly well-behaved subclass of the class of indeterminate dataflow networks. The main result of [15] was that, although such networks can be used to perform the “unfair” merging operations amerge and imerge, no such network can implement fmerge. We obtained this result by showing that every network of monotone processes implements a monotone input/output relation, that amerge and imerge are implementable by networks of monotone processes, but that fmerge is not a monotone relation. Now, it is not difficult to see how to use fmerge to implement imerge, and Panangaden [13] has shown how, using fmerge, we can implement amerge. Thus the questions left unanswered in [15] are: (1) Can amerge be implemented by a network of imerge processes and processes with functional behaviors? (2) Can imerge be so implemented by amerge? Question (1) was answered in the negative by Panangaden and Shanbhogue [14], using ad hoc techniques. In this paper, we give an alternative proof by the more general methods of [15]. Contrary to our initial expectations, we have found that question (2) has an affirmative answer, and we exhibit a network with the stated property. This network can be viewed as a demonstration that there can be no notion of “finite indeterminacy” that is preserved by network construction. The three merge primitives, arranged in order of their power to implement relations when used in combination with functional processes, thus form a strict hierarchy with imerge the weakest of the three primitives, amerge strictly stronger, and fmerge the strongest.

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

0

To obtain the negative answer to question (1), we refine the methods of [15], thereby obtaining a useful characterization of the relations implemented by the class of “monotone input/output automata.” Our characterization theorem states that a relation R : X → 2^{Y} (viewed as a “nondeterministic function”) is the input/output relation of such an automaton iff there exists a certain kind of Scott domain D, a continuous function F : X → [D → Y] and a continuous function G : X → P(D), such that R(x) = F (x)†(G(x)) for all inputs x ∈ X. Here P denotes a certain powerdomain operator, and † denotes the pointwise extension to the powerdomain of a function on the underlying domain. This characterization also specializes nicely to the classes of “determinate” and “semideterminate” automata. For determinate automata, the theorem holds with the restriction that G be singlevalued, and for semi-determinate automata, G is restricted to be a constant function. The latter result is interesting, since it shows that semi-determinate automata may be thought of as implementing a collection of continuous functions, indexed by an “oracle set” (the constant value of G). Since imerge is representable as such an oracleized set of functions, but amerge is not, we conclude that imerge is implementable by a semideterminate automaton, but amerge is not. Since the class of semi-determinate automata is closed under network construction, it follows that amerge cannot be implemented by a network of imerge and functional components.

As in [15], our main tool is the notion of permutation equivalence of computation sequences. Intuitively, two finite computation sequences are permutationequivalent if one can be transformed into the other by a finite sequence of steps in which the order of adjacent “concurrent pairs” of transitions is permuted. We use a result, shown elsewhere [20, 23], that the set of equivalence classes of computation sequences of an automaton, under the induced partial order, is a Scott domain whose finite elements are exactly the equivalence classes of finite computation sequences, and which has other useful properties. This result was established in the previous work by using the auxiliary notion of the residual of one finite computation sequence by another, to obtain an alternative characterization of permutation equivalence. For this paper, we simply quote the previous result without proof, and this permits us to prove our main result without having to develop the algebra of residuals.

2 Preliminaries

We require some concepts from trace theory [1, 12] and domain theory [16, 17, 18]. In the sequel, all sets whose cardinality is left unspecified are assumed to be at most countable.

2.1 Domains

A (Scott) domain is an ω-algebraic, consistently complete cpo. A subdomain of D is a subset U of D, which is a domain under the the ordering inherited from D, such that the inclusion of U in D is continuous. A subdomain U of D is normal if for every d ∈ D, the set {u ∈ U : u ⊑ d} is directed. Normal subdomains have the following property, which we use in the proof of Lemma 7.

Lemma 1 Suppose U is a normal subdomain of a domain D. Then any continuous F : U → E extends to a least continuous F′ : D → E.

Proof – Take F′(d) = ⨆{F (u) : u ∈ U, u ⊑ d}.

An interval in a domain D is a pair [d, d′] with d ⊑ d′. An interval [d, d′] is prime if d′ covers d; that is, there does not exist d′′ with d ⊏ d′′ ⊏ d′.

2.2 The Fringe Set Powerdomain

Suppose D is a domain. Let I_{D} : D → 2^{D} denote the map that takes d to {d}. If F : D → E is any function, then its pointwise extension is the function F † : 2^{D} → 2^{E} defined by: F †(U) = {F (d) : d ∈ U}. Call a subset U of D closed if it is downward-closed, closed under lubs of directed subsets, and also closed under lubs of pairs of elements that are consistent in D. The closure U^{c} of U is the least closed set containing U. Define a nonempty subset U of D to be a fringe set if U is precisely the set of all maximal elements of U^{c}. It follows that fringe sets are pairwise inconsistent: if d, d′ are two distinct elements of a fringe set U, then the set {d, d′} has no upper bound in D. Define a binary relation ⊑ on fringe sets of D by defining U ⊑ V iff U^{c} ⊆ V^{c}. An equivalent characterization of ⊑ is the following: U ⊑ V iff ∀x ∈ U ∃y ∈ V (x ⊑ y). It is clear from this definition that ⊑ is a preorder, and since U and V are fringe sets, the relation ⊑ is a partial order. In fact, in view of the bijective correspondence between fringe sets and their closures, we have the following:

Lemma 2 The set P(D) of all fringe sets of D, equipped with the ordering ⊑, is a domain.

Indeed, this is nothing more than a slight variant of the “relational,” “lower,” or “Hoare” powerdomain of D [16, 17], whose elements we have chosen to represent by fringe sets, rather than by closed sets as is perhaps more usual. The fringe set representation proves more convenient for our purposes. Usually, the relational powerdomain of a domain D is defined in terms of sets that are closed in the Scott topology on D. The set of maximal elements of a Scott-closed set is pairwise incomparable under the ordering on D, but it is not necessarily pairwise inconsistent. The closed sets defined above are Scott-closed sets with the additional property of being closed under lubs of consistent pairs.

2.3 Traces

A concurrent alphabet is a set X, equipped with a symmetric, irreflexive binary relation ∥ on X, called the concurrency relation. The direct product of concurrent alphabets X and Y is the concurrent alphabet X ⊗ Y whose set of elements is the disjoint union of X + Y of X and Y, and whose concurrency relation ∥_{X⊗Y} is defined to be

∥_{X⊗Y} = ∥_{X} ∪ ∥_{Y} ∪ (X × Y) ∪ (Y × X).

Suppose X is a concurrent alphabet. Let X^{∗} denote the free monoid generated by X, then there is a least congruence ∼ on X^{∗} such that a∥b implies ab ∼ ba for all a, b ∈ X. The quotient X^{∗} /∼ is the free partially commutative monoid generated by X, and its elements are called traces. We use ϵ to denote the identity element (the empty trace). The monoid X^{∗} /∼ is partially ordered, with x ⊑ y iff ∃z(xz = y). Let X̄ denote the domain obtained by ideal completion of this poset. We call X̄ the trace domain generated by the concurrent alphabet X. Notice that since the finite (=isolated=compact) elements of X̄ are in bijective correspondence with the elements of X^{∗} /∼, they inherit the monoid operation of X^{∗} /∼, with the bottom element of X̄ as the monoid identity. Let X̄^{o} denote the set of finite elements of X̄. In the sequel, we identify the elements of X^{∗} /∼ with the corresponding elements of X̄^{o}. If Z ⊆ X, then the monoid homomorphism from X^{∗} to Z^{∗} that deletes elements of X \ Z, respects ∼, hence induces a monoid homomorphism from X^{∗} /∼ to Z^{∗} /∼ and a continuous map from X̄ to Z̄. We write x|Z for the application of this map to a trace x ∈ X̄.

Lemma 3 The following are equivalent statements about a domain D:

1. D is isomorphic, by a map that preserves prime intervals, to a normal subdomain of X̄ for some concurrent alphabet X.

2. E is an event domain in the sense of [5, 24].

3. D is isomorphic to the domain of configurations of an event structure (E, ⊢, #), where E is a set of events, ⊢ is an enabling relation between finite subsets of E and elements of E, and # is a binary conflict relation on E.

The equivalence of (2) and (3) is a theorem of Winskel [5, 24]. The equivalence of (1) and (2) is shown in [20]. We shall see that event domains arise naturally as the domains of computations of the kind of automata we consider.

3 Monotone Input/Output Automata

A monotone input/output automaton (henceforth simply “automaton”) is a tuple

A = (E, X, Y, Q, qi, T),

where

• E is a concurrent alphabet of actions, and X, Y are disjoint subsets of E, called the sets of input actions and output actions, respectively. The elements of E \ (X ∪ Y) are called internal actions.

• Q is a set of states.

• qi ∈ Q is a distinguished initial state.

• T is a function that maps each pair of states q, r ∈ Q to a set T (q, r) ⊆ E.

These data are required to satisfy the following conditions:

(Disambiguation) r ≠ r′ implies T (q, r) ∩ T (q, r′) =

∅.

(Commutativity) For all states q and actions a, b, if a∥b, a ∈ T (q, r), and b ∈ T (q, s), then there exists

a state p such that a ∈ T (s, p) and b ∈ T (r, p).

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

(Receptivity) For all states q and input actions a, there exists a state r such that a ∈ T (q, r).

Intuitively, if a ∈ E, then a ∈ T (q, r) iff it is possible for A to take a step from state q in which action a occurs and the state changes to r. Input actions represent steps in which input is received from the external environment, and output actions represent steps in which output is transmitted to the external environment. We say that action a is enabled in state q if a ∈ T (q, r) for some r. By the disambiguation condition, if a is enabled in state q, then there is a unique state r such that a ∈ T (q, r). We sometimes denote this state by qa.

The transitions of an automaton are the triples (q, a, r) with a ∈ T (q, r). We often use the notation q⟶^{a}r or a : q → r to denote the transition (q, a, r). If t is the transition (q, a, r), then q is called the domain dom(t) of t and r is called the codomain cod(t) of t. Transitions t and u are called coinitial if dom(t) = dom(u).

Monotone input/output automata are closely related to the input/output automata defined by Lynch and Tuttle [10, 11]. If we ignore the distinction between input and output actions, and we delete the monotonicity and receptivity conditions, we obtain automata similar to those that have been studied by Bednarczyk [2], Kwiatkowska [9], and Shields [19]. To further motivate the definitions, we describe how monotone input/output automata can be used to model dataflow networks. For this, we use a restricted class of automata called “monotone port automata,” which are similar to the monotone port automata defined in [15].

Formally, let us fix in advance countably infinite sets P of ports and V of values. We call elements of the set P ×V port actions, and if e is the port action (p, v), then we write port(e) for its port component p, and value(e) for its value component v. Define an automaton A = (E, X, Y, Q, qi, T) to be a port automaton if X = P^{in}×V and Y = P^{out} × V for some disjoint finite subsets P^{in} and P^{out} of P, and for all e, e′ ∈ X ∪ Y we have e∥e′ iff port(e) ≠ port(e′). Such an automaton models a dataflow process or network with input port set P^{in} and output port set P^{out}. An input (output) action (p, v) corresponds to the receipt (transmission) of value v on port p, and internal actions correspond to internal computation steps in which communication with the environment does not take place. It follows from the definition of ∥ that the trace domains X̄ and Ȳ are, up to isomorphism, domains of “port histories” as in [15]. That is, the elements of X̄ and Ȳ are functions, mapping ports to finite and infinite sequences of values, and ordered argumentwise by prefix.

Notice that, in contrast to more typical models for dataflow networks, our definitions do not specify directly any particular concrete structure for the state sets of port automata, such as the existence of a FIFO “channel buffers” for each input or output port. However, the receptivity, commutativity, and monotonicity axioms can be interpreted as abstract statements about the properties of such buffers. The receptivity condition can be interpreted as stating that arriving input values can always be placed into an input buffer. The commutativity condition, together with the definition of the relation ∥, captures the notion that distinct ports have separate buffers, The monotonicity condition can be viewed as a restriction on the way input buffers can be accessed: since arriving input cannot disable transitions previously enabled, one can test for the presence of input in a buffer, but never for its absence.

4 Computations of Automata

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

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

The number n is called the length |γ| of γ. We call the computation sequence of length 0 from state q the identity computation sequence, and we denote it by id_{q}, or just id, when q is clear from the context. Also, it will sometimes be convenient to write id_{q} = (q⟶^{ϵ}q). An infinite computation sequence is an infinite sequence of transitions:

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

A computation sequence that contains only input actions is called a pure-input computation sequence; one containing no input actions is called a non-input computation sequence. The trace of γ is the element tr(γ) = e_{1}e_{2} … of the trace domain Ē.

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

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

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

Closely related to permutation equivalence is the permutation preorder relation ⊏ ∼ on finite computation sequences of A, which is defined to be the transitive closure of ⪯ ∪ ∼. That is, γ ⊏ ∼ δ iff there is a way to perform a finite number of permutations of adjacent concurrent transitions in δ, and obtain a computation δ′ that has γ as a prefix. It is not difficult to see that γ ∼ δ iff γ ⊏ ∼ δ and δ ⊏ ∼ γ. Permutation preorder extends in a straightforward way to infinite computation sequences as well: if γ′ and δ′ are coinitial finite or infinite computation sequences, then define γ′ ⊏ ∼ δ′ to hold iff for every finite γ ⪯ γ′ there exists a finite δ ⪯ δ′, such that γ ⊏ ∼ δ. We may then extend permutation equivalence to infinite computation sequences by defining γ′ ∼ δ′ iff γ′ ⊏ ∼ δ′ and δ′ ⊏ ∼ γ′.

A computation is a ∼-equivalence class of computation sequences. Obviously, all finite computation sequences that are representatives of the same ∼- equivalence class have the same length, so the notion of the length |γ| of a finite computation γ makes sense. For each state q, the permutation preorder ⊏ ∼ on computation sequences from state q induces a partial order ⊑ on the set of all computations from state q. Coinitial computations γ and γ′ are called consistent if they have an upper bound with respect to ⊑. For finite γ, γ′, this is equivalent to the existence of a pair of finite computations δ, δ′ such that γδ′ = γ′δ.

The following result, proved in [20], provides a great deal of information about the structure of the partially ordered set of computations of an automaton. Our main theorem is a direct consequence.

Lemma 4 Suppose A is an automaton. For each state q, the set Comp_{q}(A) of computations of A with domain q, partially ordered by ⊑, is an event domain whose finite elements are exactly the equivalence classes of finite computation sequences. Moreover, the map tr : Comp_{q}(A) → Ē that takes each equivalence class to the corresponding trace, is a prime-interval-preserving embedding of Comp_{q}(A) as a normal subdomain of Ē.

Rather than reproving this result here, we merely comment on the method used. It is fairly obvious from the definitions we have given that the map tr : Comp_{q}(A) → Ē is a monotone injection that preserves prime intervals. To show Comp_{q}(A) is a domain, it is necessary to show that all directed subsets have lubs and that all consistent pairs of computations have lubs. To show that the map tr is an embedding of a normal subdomain, we may show that tr is strict, additive, continuous, and reflects consistency. To show these facts, we define the auxiliary notion of the residual of one computation sequence “after” another. Formally, we have the following: Suppose γ and γ′ are consistent finite computations. Then there exists a unique pair of finite computations γ\γ′ and γ′\γ (read “γ after γ′” and “γ′ after γ”), such that γ(γ′\γ) = γ′(γ\γ′), and such that if δ and δ′ are any finite computations with γδ′ = γ′δ, then there exists a unique finite computation ξ such that (γ\γ′)ξ = δ and (γ′\γ)ξ = δ′.

We may think of \ as a partial binary operation on coinitial pairs of computations, where γ\δ is defined exactly when γ and δ are consistent, or when they could both be part of the “same concurrent computation.” In this case, δ may contain some transitions that “overlap” with γ and some that are “concurrent” with γ. Then γ\δ should be thought of as what is “left” of γ after the part that overlaps with δ has been deleted. The residual γ\δ is undefined exactly when γ contains some indeterminate choice that conflicts with a choice made in δ. A concrete construction of γ\δ for arbitrary consistent finite computations γ and δ is performed by induction on their length.

A similar residual operation can be defined on finite traces (in fact more easily so, since there are no states to worry about). Formally, if x and x′ are consistent traces then the residual of x after x′ is the unique trace x\x′ with the property that x′(x\x′) = x⊔x′. From this definition, one can easily see that x ⊑ y iff x\y = ϵ. A similar relation holds for computations: γ ⊑ δ iff γ\δ = id. Thus, the partial ordering on computations has an equivalent characterization in terms of residuals. Using this observation, Lemma 4 may then be proved by using residuals to perform an inductive construction of lubs of directed collections of computations and of consistent pairs, and also to show that the map tr : Comp_{q}(A) → Ē preserves residuals (hence is continuous) and reflects consistency.

We conclude this section with some additional facts about the computations of monotone input/output automata. We do not use these facts explicitly in this paper, but they are helpful in understanding the behavior of these automata. Proofs can be found (in a somewhat more abstract setting) in [21, 22].

Proposition 5 A monotone automaton A has the following properties:

1. For every state q and input trace x, there exists a unique computation ι_{x}(q) with dom(ι_{x}(q)) = q and tr(ι_{x}) = x. Moreover, the map ι : X̄ → Comp_{q}(A) that takes x ∈ X̄ to ι_{x} ∈ Comp_{q}(A), is a primeinterval-preserving embedding of X̄ as a normal subdomain of Comp_{q}(A).

2. Suppose γ is a computation with dom(γ) = q, and x is an input trace that is consistent with tr(γ)|X. Then γ and ι_{x}(q) are consistent.

3. Every finite computation γ factors uniquely as γ = δξ, where δ is a pure-input computation and ξ is a non-input computation. We call the pair (δ, ξ) a pure-input/non-input factorization of γ.

4. For every computation γ, there exists a computation δ that is ⊑-maximal among all computations γ′ such that γ ⊑ γ′ and tr(γ)|X = tr(γ′)|X.

5 Relations Computed by Automata

A computation is called completed if it is ⊑-maximal among all computations having the same input trace. In [15] it was shown that this notion coincides with an appropriate notion of “fairness” for monotone automata that are constructed as the parallel composition of a collection of “single-process” components. Specifically, a computation is “fair” if every component process having an enabled non-input action eventually performs some non-input action. Here, we consider a more general situation in which automata need not be networks of single-process components. Although fairness does not generalize directly to this situation, the notion “completed” does, and we therefore adopt it as the appropriate generalization of fairness.

The input/output relation of an automaton A is the function R : X̄ → 2Ȳ that maps each x ∈ X̄ to the set of all y ∈ Ȳ, such that for some some completed initial computation γ of A, we have x = tr(γ)|X and y = tr(γ)|Y.

We can now state our main result:

Theorem 1 A map R : X̄ → 2Ȳ is the input/output relation of a monotone input/output automaton iff there exists an event domain D, a continuous function F : X̄ → [D → Ȳ], and a continuous function G : X̄ → P(D), such that R(x) = F (x)†(G(x)) for all x ∈ X̄.

Proof – Follows from Lemmas 6 and 7 below.

Before proceeding to the proof, we give the definitions of fmerge, amerge, and imerge, and mention the implications of Theorem 1 for these. Intuitively, each of these relations takes as input finite or infinite sequences of values on two input ports, and produces a finite or infinite sequence of values on one output port. To formalize this, let p_{0} and p_{1} stand for the two input ports, and let p_{2} stand for the single output port. Let V be a countably infinite set of values. Form a concurrent alphabet X = {p_{0}, p_{1}} × V with (p, v)∥(p′, v′) iff p ≠ p′, and a concurrent alphabet Y = {p_{2}} × V with ∥ = ∅. Then the trace domain X̄ is isomorphic to the domain of functions mapping {p_{0}, p_{1}} to finite or infinite sequences of values with the prefix order; similarly, Ȳ is isomorphic to the domain of functions from {p_{2}} to value sequences. It will be convenient notationally to regard x ∈ X̄ as a function on {p_{0}, p_{1}}, and similarly y ∈ Ȳ as a function on {p_{2}}.

The three relations are defined as follows:

• fmerge is the set of all (x, y) ∈ X̄ × Ȳ such that y(p_{2}) is a shuffle of x(p_{0}) and x(p_{1}).

• amerge is the set of all (x, y) ∈ X̄ × Ȳ such that y(p_{2}) is a shuffle of a prefix x_{0} of x(p_{0}) and a prefix x_{1} of x(p_{1}), such that

1. If x(p_{0}) is finite, then x_{1} = x(p_{1}).

2. If x(p_{1}) is finite, then x_{0} = x(p_{0}).

3. If both x(p_{0}) and x(p_{1}) are infinite, then either x_{0} = x(p_{0}) or x_{1} = x(p_{1}).

• imerge is the set of all (x, y) ∈ X̄ × Ȳ such that y(p_{2}) is a shuffle of a prefix x_{0} of x(p_{0}) and a prefix x_{1} of x(p_{1}), such that

1. If x(p_{0}) is infinite then x_{1} = x(p_{1}).

2. If x(p_{1}) is infinite, then x_{0} = x(p_{0}).

3. If one of x(p_{0}) and x(p_{1}) is finite, then both x_{0} and x_{1} are finite, and either x_{0} = x(p_{0}) or else x_{1} = x(p_{1}).

As a consequence of Theorem 1, if R is the input/output relation of an automaton, then R has the following monotonicity property: If y ∈ R(x), and x ⊑ x′, then there exists y′ ∈ R(x′) with y ⊑ y′. The relation fmerge is not monotone (consider x(p_{0}) = ϵ, x(p_{1}) = 555 …, y(p_{2}) = 555 …, x′(p_{0}) = 7 and x′(p_{1}) = 555 …), hence is not the input/output relation of an automaton. In contrast, amerge can be expressed in the form of Theorem 1: assuming that the set of values that arrive on port p_{0} is disjoint from those that arrive on p_{1}, we may take D = Ȳ, take G = amerge, and take F (x)(y) = y for all x ∈ X̄ and y ∈ Ȳ. (If the value sets are not disjoint, then we may use a slight modification of this construction, in which we take D to be a “tagged” version of Ȳ, and the function F (x) removes the tags.) Hence amerge is the input/output relation of an automaton. It is slightly more complicated to express imerge in the required form, and we postpone this to Section 6.2 below. The results of [15] are therefore a corollary of Theorem 1.

Lemma 6 Suppose A is an automaton with input/output relation R : X̄ → 2Ȳ. Then there exists an event domain D, a continuous function F : X̄ → [D → Ȳ], and a continuous function G : X̄ → P(D), such that R(x) = F (x)†(G(x)) for all x ∈ X̄.

Proof – Let D = Comp_{qi}(A), then D is an event domain by Lemma 4. Define F : X̄ → [D → Ȳ] by:

F (x)(γ) = ⨆{tr(δ)|Y : δ ⊑ γ, tr(δ)|X ⊑ x}.

That is, F (x)(γ) is the maximum output that can be produced in a “prefix up to permutation” δ of γ, when the input is constrained to be less than x. It is straightforward to check that F is well-defined and continuous. Define G : X̄ → 2^{D} to map each x ∈ X̄ to the set of all completed initial computations with input history x. By construction, R(x) = F (x)†(G(x)) for all x ∈ X̄. It remains to be shown that G : X̄ → P(D) and that G is continuous.

We first claim that G(x) is a fringe set for all x ∈ X̄. But this is clear from the fact that the set Γ(x) of all initial computations γ with tr(γ)|X ⊑ x is closed, and G(x) is the set of its maximal elements. Next, we show that G is monotone. This is immediate from the fact that if x ⊑ x′, then Γ(x) ⊆ Γ(x′). Finally, we show that G is continuous. Given a directed collection {x_{i} : i ∈ I} of inputs, with supremum x, let Γ = ⋃ Γ(x_{i}), and note that Γ = Γ(x). Thus, G(x) = ⨆{G(x_{i}) : i ∈ I}.

Lemma 7 Let R : X̄ → 2Ȳ and suppose there exists an event domain D, a continuous function F : X̄ → [D → Ȳ], and a continuous function G : X̄ → P(D), such that R(x) = F (x)†(G(x)) for all x ∈ X̄. Then R is the input/output relation of a monotone automaton.

Proof – Since D is an event domain, by Lemma 4 it is isomorphic via a prime-interval-preserving map μ to a normal subdomain of Z̄, for some concurrent alphabet Z. Define C(x) = μ(G(x)^{c}). Let F′ : X̄ → [Z̄ → Ȳ] be defined so that for each x ∈ X̄, the map F′(x) : Z̄ → Ȳ is the least continuous function (which exists by Lemma 1) with the property that F (x) = F′(x) ∘ μ.

Next, we construct an automaton

A = (E, X, Y, Q, qi, T)

as follows:

• Let E = X ⊗ Y ⊗ Z.

• Let Q = X̄^{o} × Ȳ^{o} × Z̄^{o}, with qi = (ϵ, ϵ, ϵ).

• The map T is defined as follows:

1. If a ∈ X, then a ∈ T ((x, y, z), (x′, y′, z′)) iff x′ = xa, y′ = y, and z′ = z.

2. If b ∈ Y, then b ∈ T ((x, y, z), (x′, y′, z′)) iff x′ = x, y′ = yb, z′ = z, and y′ ⊑ F′(x)(z).

3. If c ∈ Z, then c ∈ T ((x, y, z), (x′, y′, z′)) iff x′ = x, y′ = y, z′ = zc ∈ C(x).

Intuitively, the first component of the state will is used to keep track of the finite input received so far in a computation, the second component keeps track of the finite output issued so far, and the third keeps track of the history of how indeterminate choices have been resolved so far.

It is straightforward to check that the definition of A satisfies the requirements for a monotone input/output automaton. The commutativity property of A follows from the fact that G(x), hence C(x), is closed under lubs of consistent pairs of elements. We also observe, by a straightforward induction, that if γ is any finite initial computation sequence for A, then tr(γ)|Y ⊑ F′(tr(γ)|X)(tr(γ)|Z)) and tr(γ)|Z ∈ C(tr(γ)|X). By continuity, these relationships extend also to infinite γ.

We claim that the automaton A has R as its input/output relation. There are two parts to the proof:

(1) show that if y ∈ R(x), then there exists a completed initial computation sequence γ with x = tr(γ)|X and y = tr(γ)|Y; (2) show that if γ is a completed initial computation sequence, then tr(γ)|Y ∈ R(tr(γ)|X).

(1) Suppose y ∈ R(x). Then by hypothesis, there exists z ∈ Z̄ such that z ∈ μ(G(x)) and y = F′(x)(z). Choose sequences a_{1}, a_{2},… ∈ X ∪ {ϵ}, b_{1}, b_{2},… ∈ Y ∪{ϵ}, and c_{1}, c_{2},… ∈ Z ∪{ϵ}, such that x = a_{1}a_{2} …, y = b_{1}b_{2} …, and z = c_{1}c_{2} . . .. These sequences exist by the fact that trace domains are ω-algebraic and finitary (there are at most finitely many prefixes of any finite trace). Also, because the map μ : D → Z̄ preserves prime intervals, we may choose c_{1}, c_{2},… so that c_{1}c_{2} … c_{k} ∈ C(x) for all k.

Next, we use these sequences in a “scheduling argument” to construct a sequence d_{1}, d_{2},… ∈ E ∪ {ϵ} such that if w = d_{1}d_{2} …, then x = w|X, y = w|Y, and z = w|Z. We do this as follows: Suppose we have defined d_{1}, d_{2},…, d_{k}, for some k ≥ 0. Suppose further that

x_{k} = a_{1}a_{2} … a_{l} = (d_{1}d_{2} … d_{k})|X,
y_{k} = b_{1}b_{2} … b_{m} = (d_{1}d_{2} … d_{k})|Y,
z_{k} = c_{1}c_{2} … c_{n} = (d_{1}d_{2} … d_{k})|Z.

Define d_{k+1} as follows:

• Suppose k mod 3 = 0. Then let d_{k+1} = a_{l+1}.

• Suppose k mod 3 = 1. If y_{k}b_{m+1} ⊑ F′(x_{k})(z_{k}), then let d_{k+1} = b_{m+1}, otherwise let d_{k+1} = ϵ.

• Suppose k mod 3 = 2. If z_{k}c_{n+1} ∈ C(x_{k}), then let d_{k+1} = c_{n+1}, otherwise let d_{k+1} = ϵ.

It is clear from the construction that w|X = x, w|Y ⊑ y, and w|Z ⊑ z. Moreover, since the domain Z̄ is algebraic, and the function G is continuous, given any finite z′ ⊑ z, there exists K such that z′ ∈ C(x_{k}) for all k ≥ K, thus z′ ⊑ z_{k} for sufficiently large k. Since z′ may be arbitrary, we conclude w|Z = z. Similar reasoning shows that w|Y = y.

Now, it follows from the definition of A and the construction of the sequence d_{1}, d_{2},…, that there exist states qi = q_{0}, q_{1},…, such that for each k ≥ 0 we have

q_{k}⟶^{d_{k+1}}q_{k+1}, and thus

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

is an initial computation for A. We claim that γ is completed. For if not, then there would exist δ with γ ⊑ δ but γ ≠ δ, such that tr(δ)|X = x = tr(γ)|X. By the injectiveness of the map tr, we would have either tr(γ)|Z ⊏ tr(δ)|Z or else tr(γ)|Y ⊏ tr(δ)|Y. The former is impossible because z = tr(γ)|Z is maximal in C(x) = μ(G(x)^{c}), and then the latter is also impossible because tr(δ)|Y is functionally determined (via F′) by tr(δ)|X = x and tr(δ)|Z = z.

(2) Suppose γ is a completed initial computation. Let x = tr(γ)|X, y = tr(γ)|Y, and z = tr(γ)|Z. As previously observed, we know that y ⊑ F′(x)(z) and z ∈ C(x). We claim that in fact y = F′(x)(z) and z ∈ μ(G(x)). First, suppose y ⊏ F′(x)(z). Then there is some finite y′′ ⊑ F′(x)(z), such that y′′ ⋢ y. Assume y′′ is chosen to be of minimal length, then y′′ = y′b where y′ ⊑ y and b is an output action. Using the algebraicity of Ȳ and the continuity of F′, we can obtain finite x′ ⊑ x and z′ ⊑ z such that y′b ⊑ F′(x′)(z′). Choose a finite prefix γ′ of γ such that x′ ⊑ tr(γ′)|X, y′ ⊑ tr(γ′)|Y, and z′ ⊑ tr(γ′)|Z. By the definition of A, and the monotonicity of F′, we must have b enabled in state cod(γ′). If r = cod(γ′) and t is the transition r⟶^{b}rb, then tr(γ) and tr(γ′t) are consistent, hence γ and γ′t are consistent, and they have a ⊑-upper bound δ ≠ γ. Since this contradicts the assumption that γ is completed, we conclude that y = F′(x)(z).

Finally, suppose z ∉ μ(G(x)). Because z ∈ C(x) = μ(G(x)^{c}), we have z ⊏ μ(d) for some d ∈ G(x). Therefore, there must exist some finite z′′ ∈ C(x), such that z′′ ⋢ z, but with z and z′′ consistent and z ⊔ z′′ ⊑ μ(d). The argument then proceeds for z′′ similarly to the above for y′′, contradicting the assumption that γ is completed, and concluding that z ∈ μ(G(x)).

6 Specializations of the Main Result

Our result specializes to two interesting subclasses of automata: “determinate” automata and “semideterminate” automata. In the case of determinate automata, we restrict G to be single-valued in Theorem 1. The theorem then becomes the statement that the determinate automata compute exactly the class of continuous functions from input to output. Although this result has perhaps been known in various forms for a long time, the interesting point here is how we obtain it as a specialization of a general result. In the case of semi-determinate automata, we restrict G to be a constant function in Theorem 1. The theorem then states that semi-determinate automata compute exactly those relations R such that R(x) = {F_{i}(x) : i ∈ G(ϵ)}, where the F_{i} are continuous and G(ϵ) may be thought of as an “oracle set.”

An interesting consequence of the latter result is that there are relations (e.g. amerge) that are implementable by monotone automata, but cannot be represented in oracleized form as above, hence cannot be implemented by semi-determinate automata. Since imerge can be implemented by a semi-determinate automaton, this gives us a separation in expressive power between amerge and imerge.

6.1 Determinate Automata

An automaton is determinate if it satisfies the following condition:

(Determinacy) Suppose b : q → r and b′ : q → r′, where b and b′ are distinct non-input actions. Then b∥b′.

Intuitively, a determinate automaton exhibits no “internal nondeterminism”—the only possible nondeterministic choices are those that occur between input transitions. The determinacy property may also be seen as a kind of Church-Rosser or “diamond” property for non-input actions.

Call coinitial computations γ and δ input-consistent if their input traces tr(γ)|X and tr(δ)|X are consistent.

The following lemma gives the characteristic property of determinate automata:

Lemma 8 Suppose A is a determinate automaton. Then two coinitial computations γ and δ of A are consistent iff they are input-consistent.

Proof – The proof may be accomplished by an inductive argument in which residuals are used to construct the lub of two coinitial input-consistent computations γ and δ. (See [21].)

Theorem 2 For determinate automata, Theorem 1 holds if we restrict G to be single-valued.

Proof – Suppose R(x) = F (x)†(G(x)) for all x ∈ X̄, where G is single-valued and F and G are as in Theorem 1. It is straightforward to check that application of the construction in the proof of Lemma 7 yields a determinate automaton.

Conversely, suppose A is a determinate automaton with input/output relation R. Lemma 4 and Lemma 8, together with an application of Zorn’s Lemma, show that for each x ∈ X̄, there is a unique completed computation γ_{x} with tr(γ_{x})|X = x. Hence G is single-valued.

Corollary 9 Suppose R : X̄ → 2Ȳ. Then R is the input/output relation of a determinate automaton iff R = I_{Y} ∘ H, where H : X̄ → Ȳ is continuous.

Proof – Given H, we may take D to be a one-element domain, and G to be the identically ⊥ function, which is clearly single-valued.

Since there exist nonfunctional relations (e.g. imerge and amerge) that are computable by monotone automata, it follows from the previous theorem that the class of determinate automata is strictly weaker in expressive power than the class of all monotone automata.

6.2 Semi-Determinate Automata

An automaton A is semi-determinate if it satisfies the following condition:

(Semi-Determinacy) There exists a collection C ⊆ E \ (X ∪ Y) of choice actions, such that:

1. Whenever q⟶^{a}r and r⟶^{c}s, where c ∈ C and a ∉ C, then a∥c and c is enabled in state q.

2. The automaton, formed from A by deleting all elements of C from each set T (q, r), is determinate.

It is not difficult to see from this definition that if there exists a set C with these properties, then there is a unique largest such set. When we speak of the set C of choice actions for a particular semi-determinate automaton, we refer to the largest such set. A pure-choice computation will be a computation in which only choice actions occur.

Lemma 10 Suppose A is semi-determinate. Then every finite computation γ of A can be factored uniquely as γ = γ′γ′′, where γ′ contains only choice actions, and γ′′ contains no choice actions. Moreover, if γ = γ′γ′′ and δ = δ′δ′′ are two such factorizations, where γ and δ are input-consistent, then γ and δ are consistent iff γ′ and δ′ are consistent.

Proof – The required factorization is obtained by using property (1) in the definition of semi-determinacy, and the commutativity property in the definition of automata, to “permute all choice actions to the front.” The consistency assertion then follows using property (2) in the definition of semi-determinacy. A formal proof may be carried out by induction on the length of a computation sequence.

Theorem 3 For semi-determinate automata, Theorem 1 holds if we restrict G to be a constant function.

Proof – Given D, F, and constant function G, let A be constructed as in the proof of Lemma 7. Because the enabling of actions in Z depends only on the Z̄^{o} component of the state, it follows that A is semi-determinate with C = Z.

Conversely, given A, we use a slight modification of the construction in the proof of Lemma 6. Let D be the domain of all initial pure-choice computations. For each x ∈ X̄, let G(x) be the set of all maximal initial purechoice computations. Then G(x) is obviously a fringe set, and G is constant, hence continuous. Now, the fact that deleting the choice transitions from A yields a determinate automaton implies that for each x ∈ X̄ and for each initial pure-choice computation δ, there exists a unique completed initial computation γ_{x,δ} of A such that tr(γ_{x,δ})|X = x and such that δ is the greatest pure-choice computation with δ ⊑ γ_{x,δ}. Let F (x) be the function that takes each δ ∈ D to the trace tr(γ_{x,δ})|Y. It is straightforward to see from this definition that F (x) is continuous for each x ∈ X̄, and that F itself is continuous as a function of x. Finally, observe that R(x) = F (x)†(G(x)) for all x ∈ X̄.

Corollary 11 The relation imerge is the input/output relation of a semi-determinate automaton, but amerge is not.

Proof – We may express imerge = F (x)†(G(x)), where D is the domain of finite and infinite sequences of natural numbers with the prefix order, G(x) is the set of all infinite sequences, and F (x) uses its argument as an oracle to schedule the selection of values from the two input ports. More formally, let X_{0} be the subset of X consisting of the actions (p_{0}, m), and similarly for X_{1}. Define recursively,

F (x)(ϵ) = ϵ
F (x)(nd) = H_{0}(x|X_{0}, x|X_{1}, n + 1, d)
H_{0}(x, x′, 0, ϵ) = ϵ
H_{0}(x, x′, 0, nd) = H_{1}(x, x′, n + 1, d)
H_{0}(ϵ, x′, k + 1, d) = ϵ
H_{0}((p_{0}, m)x, x′, k + 1, d) = (p_{2}, m)H_{0}(x, x′, k, d)
H_{1}(x, x′, 0, ϵ) = ϵ
H_{1}(x, x′, 0, nd) = H_{0}(x, x′, n + 1, d)
H_{1}(x, ϵ, k + 1, d) = ϵ
H_{1}(x, (p_{1}, m)x′, k + 1, d) = (p_{2}, m)H_{1}(x, x′, k, d).

In contrast, if we could express amerge in a similar form, then for any given d ∈ D, the function F_{d} defined by F_{d}(x) = F (x)(d) would be a monotone function with the property F_{d}(x) ∈ amerge(x) for all x ∈ X̄. However, no such function can exist. To see this, observe that we must have F_{d}((p_{0}, 5)) = (p_{2}, 5) and F_{d}((p_{1}, 7)) = (p_{2}, 7), so there is no possible value for F ((p_{0}, 5)(p_{1}, 7)) that will make F_{d} monotone. Hence, amerge is not the input/output relation of a semideterminate automaton.

7 Networks of Automata

So far, we have avoided entirely the issue of how automata may be composed into networks of communicating, concurrently executing components. What we have established so far is the existence of a hierarchy of monotone input/output automata, consisting of the determinate automata, the semi-determinate automata, and all the monotone automata, and we have established some separation results for this hierarchy. The results so far may be summarized by saying that semideterminate automata compute a strictly larger class of input/output relations than do determinate automata, and compute a strictly smaller class of input/output relations than do arbitrary monotone input/output automata. However, we would like to say more. We would like our results to imply something about the “implementability” of various relations in terms of networks of “primitive components.” To do this, we need to define an operation of parallel composition, by which a collection of automata is combined into a network, and we must show that the various classes of automata are closed under this operation.

7.1 Parallel Composition

Although it would be possible to define parallel composition on collections of unrestricted monotone input/output automata, the definitions are more transparent if we restrict our attention to “monotone port automata,” which we defined in Section 3.

Formally, suppose A = {A_{i} : i ∈ I} is a collection of port automata, where A_{i} = (E_{i}, X_{i}, Y_{i}, Q_{i}, qi_{i}, T_{i}). We say that A is compatible if for all i, j ∈ I, if i ≠ j then E_{i} ∩ (E_{j} \ X_{j}) ⊆ X_{i} ∩ Y_{j}.

If A is compatible, then its parallel composition is the automaton ∏ A_{i} = (E, X, Y, Q, qi, T), where

• E = ⋃ E_{i}, with a∥b iff a∥_{i}b for all i ∈ I such that both a and b are in E_{i}.

• Y = ⋃ Y_{i} and X = (⋃ X_{i}) \ Y.

• Q = ∏_{i∈I} Q_{i},

• qi = (qi_{i} : i ∈ I),

• e ∈ T ((q_{i} : i ∈ I), (r_{i} : i ∈ I)) iff for all i ∈ I, either e ∉ E_{i} and r_{i} = q_{i}, or else e ∈ E_{i} and e ∈ T_{i}(q_{i}, r_{i}).

Intuitively, component automata in a network communicate by transmitting values on shared ports. The outputting of a value v on port p by one component automaton occurs simultaneously with the inputting of value v from port p by all other automata that share port p. The compatibility condition states that only input or output actions may be shared between components, and that each shared action (port) may be an output action (port) for at most one component automaton in a network. It is not our purpose here to further justify this particular definition of parallel composition. The reader may refer to the papers [10, 11, 15] for additional motivation and discussion. Here we wish merely to observe the following:

Theorem 4 The parallel composition of a compatible collection of port automata is a port automaton. Moreover, the classes of determinate port automata and semi-determinate port automata are closed under parallel composition of compatible collections.

Proof – The disambiguation, receptivity, and commutativity properties are immediate from the definition and the corresponding properties of the A_{i}. To show monotonicity, suppose a ∈ X and b ∈ Y. Then a and b are both port actions, and port(a) ≠ port(b). Hence whenever both a, b ∈ E_{i}, we have a∥_{i}b, so a∥b.

Now, assume the A_{i} are determinate, and suppose a, b ∈ E \ X are both enabled in state q. If both a, b ∈ E_{i}, then there are four cases:

1. If both a, b ∈ E_{i} \X_{i}, then a∥_{i}b by the determinacy of A_{i}.

2. If a ∈ X_{i} and b ∈ E_{i}\X_{i}, then a∥_{i}b by monotonicity of A_{i}.

3. If a ∈ E_{i}\X_{i} and b ∈ X_{i}, then a∥_{i}b by monotonicity of A_{i}.

4. If both a, b ∈ X_{i}, then port(a) ≠ port(b). This is because if port(a) = port(b), then for some j ∈ I we would have both a, b ∈ E_{j} \ X_{j}, hence not a∥_{j}b, contradicting the determinacy of A_{j}. Since port(a) ≠ port(b), we have a∥_{i}b.

Since a∥_{i}b in all four cases, we conclude that a∥b and ∏ A_{i} is determinate.

Finally, assume the A_{i} are semi-determinate, and let C_{i} be the largest set of choice actions for A_{i}. We claim that ∏ A_{i} is semi-determinate, with C = ⋃ C_{i} as a set of choice actions. For each i ∈ I, let A′_{i} be the determinate automaton obtained from A_{i} by deleting all elements of C_{i} from each T (q, r). Similarly, let A′ be the automaton from ∏ A_{i} obtained by deleting all elements of C from each T (q, r). Then A′ = ∏ A′_{i}, so A′ is determinate. Now suppose

(q_{i} : i ∈ I)⟶^{a}(r_{i} : i ∈ I)⟶^{c}(s_{i} : i ∈ I),

where a ∈ E \ C and c ∈ C. Since each C_{i} is a set of internal actions, by compatibility we have c ∈ C_{i} for precisely one i ∈ I. There are two cases: either a ∈ E_{i} \ C_{i} or else a ∉ E_{i}. If a ∈ E_{i} \ C_{i}, then since A_{i} is semi-determinate we know that a∥_{i}c and that c is enabled for A_{i} in state q_{i}. Since c ∉ C_{j} for j ≠ i it follows that a∥c and that c is enabled for A in state (q_{i} : i ∈ I). If a ∉ E_{i}, then a∥c by definition of ∥. Since q_{i} = r_{i} we know that c is enabled for A_{i} in state q_{i}. Then c is also enabled for A in state (q_{i} : i ∈ I).

Now, we can interpret our results as saying something about the implementability of relations in terms of networks of “primitives.” For each continuous input/output function, let us choose a “standard” determinate port automaton that computes that function. For example, we may choose the automata that result from the construction of Lemma 7. Similarly, we may choose a particular semi-determinate port automaton that computes imerge, and a port automaton that computes amerge. Then our results imply:

1. the impossibility of implementing fmerge by any network of our standard primitives.

2. the impossibility of implementing amerge by any network of our standard functional primitives and our standard imerge automaton.

3. the impossibility of implementing imerge or amerge by any network of our standard functional primitives.

7.2 Finite Indeterminacy

We have not yet answered the question of whether imerge can be implemented in terms of our standard functional primitives and our standard amerge automaton. Although the answer to this question is “yes,”

[figure: trig; amerge; amerge; incr; switch; amerge; restore; (output)]

Figure 1: Implementation of Iterated Unbounded Choice by amerge.

for a long time it seemed likely to the author that one could prove the opposite by trying to define a class of automata with a property of “finite indeterminacy,” and showing that no such automaton could compute imerge. This was to be accomplished by proving a version of Theorem 1 for automata with finite indeterminacy in which the sets G(x) were required to have a topological compactness property. After a number of failed attempts, the author realized that it is possible to construct a finite network of standard functional and amerge processes that computes imerge. One way to interpret this result is that there is can be no definition of “finite indeterminacy” that is satisfied by some standard automaton that computes amerge, is not satisfied by any automaton that computes imerge, and that is preserved under parallel composition.

Figure 1 shows how amerge can be used together with functional processes to construct a network that outputs an arbitrary infinite sequence of nonnegative integers. Once one has such a network, it is straightforward to use it as an “oracle” (as suggested by the proof of Corollary 11) to construct an implementation of imerge.

We give only an informal description of the operation of the network, rather than a formal definition and correctness proof. All processes other than the amerge processes are functional. All tokens that traverse the channels contain either numeric values or a special “trigger” value, used by the node switch. The process trig generates an infinite sequence of trigger values. The process incr repeatedly reads numeric values from its input, increments them and then issues the incremented values at the output. The process switch reads numeric values and outputs them to the righthand output until a trigger value is read. Once this has happened, the next numeric value is output to the left, and the cycle repeats. Multiple trigger values arriving in succession at the input are treated identically to a single trigger value. The process restore initially outputs a zero on its right-hand output and a one on its left-hand output. Once this is done, it repeats the following forever: Read a numeric value from the input; if the value read is zero, output a zero on the right-hand output, otherwise output a one on the left-hand output.

The network operates as follows: Initially, the restore process supplies a zero token at one input of the top amerge and a one token to the bottom amerge, which injects it into the loop. The nonzero token cycles an indeterminate number of times (possibly forever) around the loop, getting its value incremented each time. If a trigger token ever makes it through the middle amerge to the switch, then the loop will be terminated, however we can’t guarantee that this will ever happen. What we do know, though, is that either the zero token will make it through the top amerge, or a nonzero token will exit the loop and pass through the top amerge. Thus, eventually a token will pop out the top, and it is easy to see that any nonnegative integer value is possible.

Once a token has been output, it is the function of the restore process to reinitialize the network. If a zero was output, then the restore process supplies another zero token to the top amerge. If a nonzero value was output, then the restore process injects another “one” token into the loop via the bottom amerge. Note that it is not necessary (and it is in fact impossible) to remove the token still circulating around the loop in the case that a zero was output. Since the circulating token might have any value, simply restoring a zero token to the top amerge is sufficient to reinitialize the network.

8 Conclusion

We have defined a class of concurrent automata that can be used to model indeterminate dataflow networks, we have defined two subclasses of automata in terms of their transition structure, and we have obtained a characterization of the input/output relations computed by each class. We have also defined an operation of parallel composition, and observed that each of the three classes of automata is closed under this operation. The three classes (determinate, semi-determinate, and unrestricted) automata form a strict hierarchy with respect to their power to compute relations.

An interesting direction for future research would be to obtain a version of Theorem 1 that characterizes the relations that are computable by automata that are parallel compositions of single-process components. Formally, we may define an automaton to be single-process if it satisfies the following condition:

(Single-Process) Suppose b : q → r and b′ : q → r′, where b and b′ are distinct non-input actions. Then not b∥b′.

Define a network automaton to be an automaton of the form ∏ A_{i}, where {A_{i} : i ∈ I} is a compatible collection of single-process automata. The problem is then to find conditions under which we can “decompose” an automaton into a network of single-process automata, and to relate these conditions to the structure of the domain of computations. One condition that does permit us to perform such a decomposition is the to require that the complement # of the concurrency relation ∥ on actions be an equivalence relation. We can then recover the “processes” as the equivalence classes of #. At the moment, though, it is not clear how this equivalence relation condition on an automaton is reflected in the structure of its domain of computations.

References

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

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

[3] 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.

[4] M. Broy. Nondeterministic data-flow programs: how to avoid the merge anomaly. Science of Computer Programming, 10:65–85, 1988.

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

[6] 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.

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

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

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

[10] N. A. Lynch and E. W. Stark. A proof of the Kahn principle for input/output automata. Information and Computation, 1989. (to appear).

[11] N. A. Lynch and M. Tuttle. Hierarchical Correctness Proofs for Distributed Algorithms. Technical Report MIT/LCS/TR-387, M. I. T. Laboratory for Computer Science, April 1987.

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

[13] P. Panangaden. Implementation of amerge with fmerge. June 1988. (Private communication).

[14] P. Panangaden and V. Shanbhogue. On the Expressive Power of Indeterminate Network Primitives. Technical Report 87-891, Cornell University Dept. of Computer Science, December 1987.

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

[16] G. D. Plotkin. Domains: lecture notes. 1979. (unpublished manuscript).

[17] D. A. Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, 1986.

[18] D. S. Scott. Lectures on a Mathematical Theory of Computation. Technical Report PRG-19, Oxford University Computing Laboratory, Programming Research Group, May 1981.

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

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

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

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

[23] E. W. Stark. Connections between a concrete and abstract model of concurrent systems. In Fifth Conference on the Mathematical Foundations of Programming Semantics, Springer-Verlag. Lecture Notes in Computer Science, New Orleans, LA, 1990. (to appear).

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