First-Order Axioms for Asynchrony

Peter Selinger^{∗} Department of Mathematics University of Pennsylvania Philadelphia, PA 19104-6395

Abstract. We study properties of asynchronous communication independently of any concrete concurrent process paradigm. We give a general-purpose, mathematically rigorous definition of several notions of asynchrony in a natural setting where an agent is asynchronous if its input and/or output is filtered through a buffer or a queue, possibly with feedback. In a series of theorems, we give necessary and sufficient conditions for each of these notions in the form of simple first-order or second-order axioms. We illustrate the formalism by applying it to asynchronous CCS and the core join calculus.

Introduction

The distinction between synchronous and asynchronous communication is a relevant issue in the design and analysis of distributed and concurrent networks. Intuitively, communication is said to be synchronous if messages are sent and received simultaneously, via a ’handshake’ or ’rendez-vous’ of sender and receiver. It is asynchronous if messages travel through a communication medium with possible delay, such that the sender cannot be certain if or when a message has been received.

Asynchronous communication is often studied in the framework of concurrent process paradigms such as the asynchronous π-calculus, which was originally introduced by Honda and Tokoro [9], and was independently discovered by Boudol [6] as a result of his work with Berry on chemical abstract machines [5]. Another such asynchronous paradigm is the join calculus, which was recently proposed by Fournet and Gonthier as a calculus of mobile agents in distributed networks with locality and failure [7, 8].

In this paper, we study properties of asynchronous communication in general, not with regard to any particular process calculus. We give a general-purpose, mathematically rigorous definition of asynchrony, and we then show that this notion can be axiomatized. We model processes by labeled transition systems with input and output, a framework that is sufficiently general to fit concurrent process paradigms such as the π-calculus or the join calculus, as well as data flow models and other such formalisms. These transition systems are similar to Lynch and Stark’s input/output automata [10], but our treatment is more category-theoretical and close in spirit to Abramsky’s interaction categories [1, 2].

Various properties of asynchrony have been exploited in different contexts by many authors. For instance, Lynch and Stark [10] postulate a form of input receptivity for their automata. Palamidessi [13] makes use of a certain confluence property to prove that the expressive power of the asynchronous π-calculus is strictly less than that of the synchronous π-calculus. Axioms similar to ours have been postulated by [4] and by [14] for a notion of asynchronous labeled transition systems, but without the input/output distinction which is central to the our approach.

∗This research was supported by an Alfred P. Sloan Doctoral Dissertation Fellowship.

The main novelty of this paper is that our axioms are not postulated a priori, but derived from more primitive notions. We define asynchrony in elementary terms: an agent is asynchronous if its input and/or output is filtered through a communication medium, such as a buffer or a queue, possibly with feedback. We then show that our first- and second-order axioms precisely capture each of these notions. This characterization justifies the axioms a posteriori. As a testbed and for illustration, we apply these axioms to an asynchronous version of Milner’s CCS, and to the core join calculus.

Due to limitations of space, most proofs are omitted in this abbreviated version of the paper. Only the proof of Theorem 2.1 is included as a typical example of the type of reasoning that is employed here. A full version of the paper is available from the author and will also appear as part of his Ph.D. Thesis.

Acknowledgments. I would like to thank Catuscia Palamidessi, Davide Sangiorgi, Benjamin Pierce, Dale Miller, Steve Brookes, Ian Stark, and Glynn Winskel for discussions and helpful comments on this work.

1 An Elementary Definition of Asynchrony

If R is a binary relation, we write R^{−1} for the inverse relation and R^{∗} for the reflexive, transitive closure of R. We also write ⟵ for ⟶^{−1}, etc. The binary identity relation on a set is denoted Δ. The composition of two binary relations R and Q is written R ∘ Q or simply RQ, i.e. xRQz if there exists y such that xRyQz. The disjoint union of two sets X and Y is denoted by X + Y.

1.1 Labeled Transition Systems and Bisimulation

To keep this paper self-contained, we summarize the standard definitions for labeled transition systems and weak and strong bisimulation.

Definition. A labeled transition system (LTS) is a tuple S = ⟨S, A, ⟶_{S}, s_{0}⟩, where S is a set of states, A is a set of actions, ⟶_{S} ⊆ S × A × S is a transition relation and s_{0} ∈ S is an initial state. We call A the type of S, and we write S: A.

We often omit the subscript on ⟶_{S}, and we write |S| for the set of states S. For α ∈ A, we regard ⟶^{α} as a binary relation on |S| via s ⟶^{α} s′ iff ⟨s, α, s′⟩ ∈ ⟶.

Definition. Let S and T be LTSs of type A. A binary relation R ⊆ |S|×|T| is a strong bisimulation if for all α ∈ A, R⟶^{α} ⊆ ⟶^{α}R and R^{−1}⟶^{α} ⊆ ⟶^{α}R^{−1}. In diagrams:

[figure: s; R; t; α; t′] ⇒ ∃s′. [figure: s; R; α; t; α; s′; R; t′]  and  [figure: s; R; α; t; s′] ⇒ ∃t′. [figure: s; R; α; t; α; s′; R; t′]

Next, we consider LTSs with a distinguished action τ ∈ A, called the silent or the unobservable action. Let ⇒^{τ} be the relation ⟶^{τ}^{∗}. For a ∈ A \ τ, let ⇒^{a} be the relation ⟶^{τ}^{∗}⟶^{a}⟶^{τ}^{∗}. A binary relation R ⊆ |S| × |T| is a weak bisimulation if for all α ∈ A,

R⟶^{α} ⊆ ⇒^{α}R and R^{−1}⟶^{α} ⊆ ⇒^{α}R^{−1}. In diagrams:

[figure: s; R; t; α; t′] ⇒ ∃s′. [figure: s; R; α; t; α; s′; R; t′]  and  [figure: s; R; α; t; s′] ⇒ ∃t′. [figure: s; R; α; t; α; s′; R; t′]

It is well-known that there is a maximal strong bisimulation, which we denote by ∼, and a maximal weak bisimulation, which we denote by ≈. We say that s ∈ |S| and t ∈ |T| are strongly (weakly) bisimilar if s ∼ t (s ≈ t). Finally, S and T are said to be strongly (weakly) bisimilar if s_{0} ∼ t_{0} (s_{0} ≈ t_{0}).

The relations ∼ and ≈, as binary relations on an LTS S, are equivalence relations. We denote the respective equivalence classes of a state s by [s]_{∼} and [s]_{≈}. On the quotient S/∼, we define transitions [s]_{∼} ⟶^{a} [t]_{∼} iff s ⟶^{a}∼ t, making it into a well-defined transition system. Similarly, on S/≈, we define [s]_{≈} ⟶^{a} [t]_{≈} iff s ⟶^{a}≈ t. For all s ∈ S, one has s ∼ [s]_{∼} and s ≈ [s]_{≈}, and hence S ∼ (S/∼) and S ≈ (S/≈). We say that S is ∼-reduced if S = S/∼, and ≈-reduced if S = S/≈.

1.2 Input, Output and Sequential Composition

So far we have distinguished only one action: the silent action τ. We will now add further structure to the set of actions by distinguishing input and output actions. Let in and out be constants. For any sets X and Y, define a set of input actions InX := {in} × X, and a set of output actions OutY := {out} × Y. Note that InX and OutY are disjoint. We will write input and output actions as inx and outx instead of ⟨in, x⟩ and ⟨out, x⟩, respectively. Let B be a set whose elements are not of the form inx, outy or τ. The elements of B + {τ} are called internal actions.

Definition. We define X→_{B}Y to be the set InX + OutY + B + {τ}. A labeled transition system S of type X→_{B}Y is called an LTS with input and output, or simply an agent. If B is empty, we will omit the subscript in X→_{B}Y.

Our labeled transition systems with input and output are similar to the input/output automata of Lynch and Stark [10]. However, we consider a notion of sequential composition that is more in the spirit of Abramsky’s interaction categories [1, 2]. Given two agents S: X→_{B}Y and T: Y →_{B}Z, we define S; T: X→_{B}Z by feeding the output of S into the input of T. This is a special case of parallel composition and hiding. Notice that this notion of sequential composition is different from the one of CSP or ACP, where T cannot start execution until S is finished.

Definition 1.1. Let S: X→_{B}Y and T: Y →_{B}Z be agents with respective initial states s_{0} and t_{0}. The sequential composition S; T is of type X→_{B}Z. It has states |S| × |T| and initial state ⟨s_{0}, t_{0}⟩. The transitions are given by the following rules:

\frac{s ⟶^{α}_{S} s′  α not output}{⟨s, t⟩ ⟶^{α}_{S;T} ⟨s′, t⟩}  \frac{t ⟶^{α}_{T} t′  α not input}{⟨s, t⟩ ⟶^{α}_{S;T} ⟨s, t′⟩}  \frac{s ⟶^{out y}_{S} s′  t ⟶^{in y}_{T} t′}{⟨s, t⟩ ⟶^{τ}_{S;T} ⟨s′, t′⟩}

Example 1.2. For any set X, define an agent I_{X} of type X→X with states X + {⊥}, initial state ⊥ and transitions ⊥ ⟶^{inx} x and x ⟶^{outx} ⊥, for all x ∈ X. I_{X} acts as a buffer of capacity one: A possible sequence of transitions is

⊥ ⟶^{inx} x ⟶^{outx} ⊥ ⟶^{iny} y ⟶^{outy} ⊥ ⟶^{inz} z ⟶^{outz} ⊥ …

Let X = {x}. Then I_{X} and I_{X}; I_{X} are the following agents:

I_{X} = [figure: ⊥; inx; x; outx] I_{X}; I_{X} = [figure: ⟨⊥, ⊥⟩; inx; ⟨⊥, x⟩; outx; inx; ⟨x, ⊥⟩; τ; ⟨x, x⟩; outx]

Here the initial state of each agent is circled. When representing agents in diagrams like these, it is often convenient to omit the names of the states, and to identify weakly bisimilar states. With that convention, we write:

I_{X} = [figure: •; inx; •; outx] I_{X}; I_{X} ≈ [figure: •; inx; •; outx; inx; •; outx]

Note that I_{X}; I_{X} is a queue of capacity 2. In general, for any set Y, I_{Y}; I_{Y} is a first-in, first-out queue of capacity 2.

Two LTSs S and T of type A are isomorphic if there is a bijection between |S| and |T| preserving ⟶ and initial states.

Lemma 1.3. 1. Sequential Composition of labeled transition systems is associative up to isomorphism.

2. Sequential Composition of agents respects both weak and strong bisimulation, i.e.

\frac{S_{1} ≈ S_{2}  T_{1} ≈ T_{2}}{S_{1}; T_{1} ≈ S_{2}; T_{2}}  and  \frac{S_{1} ∼ S_{2}  T_{1} ∼ T_{2}}{S_{1}; T_{1} ∼ S_{2}; T_{2}}

Unfortunately, agents do not form a category under sequential composition: there are no identity morphisms. In Section 1.4, we will introduce two categories of agents, one of which has unbounded buffers as its identity morphisms, and the other one queues.

1.3 Buffers and Queues

For any set X, let X^{∗} be the free monoid and X^{∗∗} the free commutative monoid generated by X. The elements of X^{∗} are finite sequences. The empty sequence is denoted by ϵ. The elements of X^{∗∗} are finite multisets. The empty multiset is denoted by ∅. We define the following agents of type X→_{B}X:

1. The buffer B_{X} has states X^{∗∗}, initial state ∅, and transitions w ⟶^{inx} wx and xw ⟶^{outx} w, for all w ∈ X^{∗∗} and x ∈ X.

2. The queue Q_{X} has states X^{∗}, initial state ϵ, and transitions w ⟶^{inx} wx and xw ⟶^{outx} w, for all w ∈ X^{∗} and x ∈ X.

The only difference between the definitions of B_{X} and Q_{X} is whether the states are considered as sequences or multisets. We will write B and Q without subscript if X is clear from the context. B acts as an infinite capacity buffer which does not preserve the order of messages. For example, one possible sequence of transitions is

∅ ⟶^{inx} x ⟶^{iny} xy ⟶^{inz} xyz ⟶^{outy} xz ⟶^{outx} z ⟶^{inw} wz …

Q acts as an infinite capacity first-in, first-out queue. A possible sequence of transitions is

ϵ ⟶^{inx} x ⟶^{iny} xy ⟶^{outx} y ⟶^{inz} yz ⟶^{inw} yzw ⟶^{outy} zw …

Lemma 1.4. 1. B; B ≈ B and B; B ≁ B.

2. Q; Q ≈ Q and Q; Q ≁ Q.

3. Q; B ≈ B and Q; B ≁ B.

4. If |X| ≥ 2, then B; Q ≉ B and B; Q ≉ Q.

The remainder of this paper is devoted to examining the effect of composing arbitrary agents with buffers and queues.

1.4 Notions of Asynchrony

In the asynchronous model of communication, messages are assumed to travel through a communication medium or ether. Sometimes, the medium is assumed to be first-in, first-out (a queue); sometimes, as in the asynchronous π-calculus, messages might be received in any order (a buffer).

Our approach is simple: we model the medium explicitly. An asynchronous agent is one whose output and/or input behaves as if filtered through either a buffer B or a queue Q.

Definition 1.5. An agent S: X→_{B}Y is

out-buffered if S ≈ S; B
in-buffered if S ≈ B; S
buffered if S ≈ B; S; B

out-queued if S ≈ S; Q
in-queued if S ≈ Q; S
queued if S ≈ Q; S; Q

We use the word asynchrony as a generic term to stand for any such property. Distinguishing these six different notions will allow us to study them separately. Yet another notion of asynchrony, incorporating feedback, will be defined in Section 3.2.

Remark. Because of Lemma 1.4, the operation of pre- or post-composing an agent with B or Q is idempotent up to ≈. Consequently, any agent of the form S; B is outbuffered, any agent of the form B; S is in-buffered, an agent is buffered iff it is inand out-buffered, and so on. Also, each of the six properties is invariant under weak bisimulation.

Let B be a set. Buffered agents S: X→_{B}Y form the morphisms of a category Buf_{B}, whose objects are sets X, Y, etc.; the identity morphism on X is given by the buffer B_{X}. Similarly, queued agents form a category Que_{B}. These categories have a symmetric monoidal structure, which will be described in Section 3.1.

1.5 Examples

Example 1.6. The first example shows the effect of post-composing different agents with the buffer B. Notice that although B has infinitely many states, S; B may have only finitely many states up to weak bisimulation.

S = [figure: s; outy; t; inx; u] S; B_{{y}} = [figure: ⟨s, ∅⟩; τ; ⟨s, y⟩; outy; τ; ⟨s, y^{2}⟩; outy; ⋯; ⟨t, ∅⟩; inx; ⟨t, y⟩; outy; inx; ⟨t, y^{2}⟩; outy; ⋯; inx; ⟨u, ∅⟩; ⟨u, y⟩; outy; ⟨u, y^{2}⟩; outy; ⋯] ≈ [figure: •; inx; outy; •; inx; •; outy; •]

Example 1.7.

S = [figure: •; inx; outy; outz; •; •; •] S; B ≈ [figure: •; inx; τ; τ; •; outy; •; •; •; outz; •]

Example 1.8. Here is an example on in-bufferedness. Notice that an input action is possible at every state of B; S.

S = [figure: •; inx; inx; •; outy; •; outz; •] B_{{x}}; S ≈ [figure: •; outy; inx; •; inx; •; τ; τ; inx; •; inx; •; outz; inx]

2 First-Order Axioms for Asynchrony

In this section, we will give necessary and sufficient conditions for each of the notions of asynchrony from Definition 1.5. These conditions take the form of first-order axioms, by which we mean axioms that use quantification only over states and actions, but not over subsets of states or actions. The axioms, which are shown in Tables 1 through 2, characterize each of our notions of asynchrony up to weak bisimulation; this means, an LTS is asynchronous iff it is weakly bisimilar to one satisfying the axioms. It is possible to lift the condition “up to weak bisimulation” at the cost of introducing second-order axioms; this is the subject of Section 6.

Table 1: First-order axioms for out-buffered agents

\xymatrix{s \ar[r]^{outy} & s′ \ar[d]^{α} \\ & t} ⇒ \xymatrix{s \ar[r]^{outy} \ar[d]_{α} & s′ \ar[d]^{α} \\ s′′ \ar[r]^{outy} & t}

output-commutativity (ob1)

\xymatrix{s \ar[r]^{outy} \ar[d]_{α} & s′ \\ s′′} ⇒ \xymatrix{s \ar[r]^{outy} \ar[d]_{α} & s′ \ar[d]^{α} \\ s′′ \ar[r]^{outy} & t}

where α ≠ outy output-confluence (ob2)

\xymatrix{s \ar[r]^{outy} \ar[d]_{outy} & s′ \\ s′′} ⇒ s′ = s′′

output-determinacy (ob3)

2.1 Out-Buffered Agents

Table 1 lists three axioms for out-buffered agents. We use the convention that variables are implicitly existentially quantified if they occur only on the right-hand-side of an implication, and all other variables are implicitly universally quantified. Thus the axioms are:

(ob1) Output-commutativity: output actions can always be delayed.

(ob2) Output-confluence: when an output action and some other action are possible, then they can be performed in either order with the same result. In particular, neither action precludes the other.

(ob3) Output-determinacy: from any state s, there is at most one transition outy for each y ∈ Y.

Each of these axioms is plausible for the behavior of a buffer. Output-determinacy is maybe the least intuitive of the three properties; the idea is that once an output action is stored in a buffer, there is only one way of retrieving it. Together, these axioms characterize out-bufferedness up to weak bisimulation:

Theorem 2.1 (Characterization of out-buffered agents). An agent S is out-buffered if and only if S ≈ T for some T satisfying (ob1)–(ob3).

This is a direct consequence of the following proposition:

Proposition 2.2. 1. Every agent of the form S; B satisfies (ob1)–(ob3).

2. If S satisfies (ob1)–(ob3), then S ≈ S; B.

Proof. 1. Clearly, the buffer B satisfies (ob1)–(ob3). Moreover, these conditions are preserved by arbitrary sequential composition from the left.

Table 2: First-order axioms for in-buffered agents

\xymatrix{s \ar[r]^{α} & s′ \ar[d]^{inx} \\ & t} ⇒ \xymatrix{s \ar[r]^{α} \ar[d]_{inx} & s′ \ar[d]^{inx} \\ s′′ \ar[r]^{α} & t}

input-commutativity (ib1)

\xymatrix{s \ar[r]^{inx} \ar[d]_{α} & s′ \\ s′′} ⇒ \xymatrix{s \ar[r]^{inx} \ar[d]_{α} & s′ \ar[d]^{α} \\ s′′ \ar[r]^{inx} & t}

input-confluence (ib2)

\xymatrix{s \ar[r]^{inx} \ar[d]_{inx} & s′ \\ s′′} ⇒ s′ = s′′

input-determinacy (ib3)

s ⇒ s ⟶^{inx} t

input-receptivity (ib4)

2. Suppose S: X→_{B}Y satisfies (ob1)–(ob3). For a sequence w = y_{1}y_{2} ⋯ y_{n} ∈ Y^{∗}, we write s ⟶^{outw} t if s ⟶^{outy_{1}}⟶^{outy_{2}} ⋯ ⟶^{outy_{n}} t (n ≥ 0). Note that if w′ ∈ Y^{∗} is a permutation of w, then s ⟶^{outw′} t iff s ⟶^{outw} t by (ob1). Consider the relation R ⊆ |S| × |S; B| given by sR⟨t, w⟩ iff s ⟶^{outw} t. Clearly, R relates initial states. We show that R is a weak bisimulation. In one direction, suppose

[figure: s; R; α; ⟨t, w⟩; s′.]

Two cases arise:

Case 1: α = outy for some y ∈ w. By the definition of R, s ⟶^{outy} s′′ ⟶^{outw′} t, where w = yw′. By (ob3), we have s′ = s′′. Therefore s′R⟨t, w′⟩, and also ⟨t, w⟩ ⟶^{α} ⟨t, w′⟩.^{√} Case 2: α ≠ outy for all y ∈ w. From s ⟶^{outw} t and s ⟶^{α} s′, we get s′ ⟶^{outw} t′ and t ⟶^{α} t′ by repeated application of (ob2). Therefore s′R⟨t′, w⟩ and ⟨t, w⟩ ⇒^{α} ⟨t′, w⟩ (notice the use of ⇒ here, which is necessary in case α is an output action).^{√}

In the other direction, suppose

[figure: s; R; ⟨t, w⟩; α; ⟨t′, w′⟩.]

We distinguish three cases for ⟨t, w⟩ ⟶^{α} ⟨t′, w′⟩, depending on which rule in Definition 1.1 was used.

Case 1: t ⟶^{α} t′, w = w′ and α not output. Then s ⟶^{outw} t ⟶^{α} t′, which implies s ⟶^{α} s′ ⟶^{outw} t′ by repeated application of (ob1), i.e.s ⟶^{α} s′R⟨t′, w⟩.^{√} Case 2: t = t′, w ⟶^{α} w′ and α not input. Since B has only input and output transitions, α must be outy for some y ∈ Y with w = yw′. Then s ⟶^{outy} s′ ⟶^{outw′} t, i.e.

s ⟶^{α} s′R⟨t, w′⟩.^{√}

Case 3: t ⟶^{outy} t′, w ⟶^{iny} w′ and α = τ. In this case, w′ = wy and s ⟶^{outw} t ⟶^{outy} t′, hence sR⟨t′, w′⟩.^{√} □

Remark 2.3. Theorem 2.1 generalizes to other notions of equivalence of processes, as long as they are coarser than weak bisimulation. Indeed, if ≅ is an equivalence of processes such that ≈ ⊆ ≅, then for any agent S, there exists some out-buffered T with S ≅ T iff there exists T′ satisfying (ob1)–(ob3) and S ≅ T′. This is a trivial consequence of Theorem 2.1. Similar remarks apply to the other results in this section and in Section 3.

2.2 In-Buffered Agents and Queues

The axioms for in-buffered agents are listed in Table 2. The main difference to the out-buffered case is the property input-receptivity: an in-buffered agent can perform any input action at any time. This was illustrated in Example 1.8. The input/output automata of Lynch and Stark [10] have this property, and so does Honda and Tokoro’s original version of the asynchronous π-calculus [9].

Remark. Somewhat surprisingly, the axioms in Table 2 are not independent. In fact, (ib1) and (ib2) are equivalent in the presence of (ib3) and (ib4). We present all four axioms in order to highlight the analogy to the output case.

Theorem 2.4 (Characterization of in-buffered agents). An agent S is in-buffered if and only if S ≈ T for some T satisfying (ib1)–(ib4).

The axioms can be adjusted to accommodate queues rather than buffers: In (ob1) and (ob2), change the side conditions to “α not output”. Change (ob3) to “if s ⟶^{outy} s′ and s ⟶^{outz} s′′ then y = z and s′ = s′′”. In (ib1) and (ib2), change the side conditions to “α not input”. Then the analogs of Theorems 2.1 and 2.4 hold.

3 More Constructors and Asynchrony with Feedback

3.1 Agent Constructors

In this section, we will introduce some operations on agents, such as renaming and hiding of actions, parallel composition and feedback.

1. Domain extension. If S is an LTS of type A, and if A ⊆ A′, then S can also be regarded as an LTS of type A′.

2. Domain restriction (hiding). If S is an LTS of type A, and if τ ∈ A′ ⊆ A, then S|_{A′} is defined to be the LTS of type A′ which has the same states as S, and whose transitions are those of S restricted to |S| × A′ × |S|.

Domain extension and domain restriction are special cases of the following, general renaming construct:

3. General renaming and hiding. Let S be an LTS of type A and let r ⊆ A × A′ be a relation such that τrα′ iff τ = α′. Define S_{r} to be the LTS of type A′ that has the same states and initial state as S and transitions s ⟶^{α}_{S_{r}} t iff s ⟶^{α′}_{S} t for some αrα′.

Let us now turn to various forms of parallel composition.

4. Parallel composition without interaction. Let S and T be LTSs of type A. Then S∥T is the LTS of type A with states |S|×|T| and initial state ⟨s_{0}, t_{0}⟩, and whose transitions are given by the rules

\frac{s ⟶^{α}_{S} s′}{⟨s, t⟩ ⟶^{α}_{S∥T} ⟨s′, t⟩} \frac{t ⟶^{α}_{T} t′}{⟨s, t⟩ ⟶^{α}_{S∥T} ⟨s, t′⟩} .

5. Symmetric monoidal structure. Let X ⊕ X′ be the disjoint union of sets. For S: X→_{B}Y and T: X′→_{B}Y′, define S⊕T: X ⊕X′→_{B}Y ⊕Y′ to be the agent S_{r}∥T_{q}, where r and q are the inclusions of X→_{B}Y, respectively X′→_{B}Y′ into X ⊕ X′→_{B}Y ⊕ Y′. Then ⊕ defines a symmetric monoidal structure on the categories Buf and Que. The tensor unit is given by the agent I of type ∅ → ∅ with one state and no transitions.

The constructors we have considered so far, including sequential composition, are not sufficient to build arbitrary networks. What is missing is the ability to construct loops. The next constructor allows the output of an agent to be connected to its own input:

6. Self-composition (feedback). Let S: X→_{B}Y. Let O ⊆ Y × X be a set of pairs. Define S ⟲ O, the self-composition of S along O, to be the LTS of type X→_{B}Y whose states are identical with those of S, and whose transitions are given by the rules

\frac{s ⟶^{α}_{S} t}{s ⟶^{α}_{S⟲O} t}  \frac{s ⟶^{outy}⇒^{τ}⟶^{inx}_{S} t  ⟨y, x⟩ ∈ O}{s ⟶^{τ}_{S⟲O} t} .

In the common case where S: X→_{B}X and O = {⟨x, x⟩ | x ∈ X}, we will write S^{∘} instead of S ⟲ O.

We can use self-composition to define both sequential and parallel composition.

7. Sequential composition. The sequential composition of agents was defined in Definition 1.1. Alternatively, one can define it from the more primitive notions of direct sum, feedback and hiding: Let S: X→_{B}Y and T: Y →_{B}Z. Then S ⊕ T: X ⊕ Y →_{B}Y ⊕ Z, and with ΔY = {⟨y, y⟩ | y ∈ Y }, one gets S; T ≈ ((S ⊕ T) ⟲ ΔY)|_{X→_{B}Z}.

8. Parallel composition (with interaction). Let S, T: X→_{B}X. The parallel composition S|T is defined to be the agent (S∥T)^{∘}.

Proposition 3.1. All of the agent constructors in this section respect weak bisimulation. For instance, if S ≈ S′ and T ≈ T′, then S_{r} ≈ S′_{r} and S∥T ≈ S′∥T′, etc.

Table 3: First-order axioms for out-buffered agents with feedback

\xymatrix{s \ar[r]^{outx} & s′ \ar[d]^{α} \\ & t} ⇒ \xymatrix{s \ar[r]^{outx} \ar[d]_{α} & s′ \ar[d]^{α} \\ s′′ \ar[r]^{outx} & t}

output-commutativity (fb1)

\xymatrix{s \ar[r]^{outx} \ar[d]_{α} & s′ \\ s′′} ⇒ \xymatrix{s \ar[r]^{outx} \ar[d]_{α} & s′ \ar[d]^{α} \\ s′′ \ar[r]^{outx} & t}

where α ≠ outx and α ≠ τ output-confluence (fb2)

\xymatrix{s \ar[r]^{outx} \ar[d]_{outx} & s′ \\ s′′} ⇒ s′ = s′′

output-determinacy (fb3)

\xymatrix{s \ar[r]^{outx} & s′ \ar[d]^{inx} \\ & t} ⇒ \xymatrix{s \ar[r]^{outx} \ar[dr]_{τ} & s′ \ar[d]^{inx} \\ & t}

feedback (fb4)

\xymatrix{s \ar[r]^{outx} \ar[d]_{τ} & s′ \\ s′′} ⇒ \xymatrix{s \ar[r]^{outx} \ar[d]_{τ} & s′ \ar[d]^{τ} \\ s′′ \ar[r]^{outx} & t} or \xymatrix{s \ar[r]^{outx} \ar[d]_{τ} & s′ \ar[dl]^{inx} \\ s′′}

output-tau (fb5)

3.2 Asynchrony with Feedback

In concurrent process calculi such as CCS or the π-calculus, messages that are emitted from a process are immediately available as input to all processes, including the sending process itself. In our setting, this is best modeled by requiring that all processes are of type X→X for one fixed set X, and by using self-composition to feed the output back to the input.

In the presence of feedback, out-bufferedness takes a slightly different form, which is expressed in the following definition.

Definition. An agent S: X→_{B}X is out-buffered with feedback if S ≈ R^{∘} for some out-buffered agent R.

Example 3.2. The following agent S is out-buffered with feedback but not out-buffered:

S = [figure: •; inx; outx; τ; •; inx; outx; τ; •; inx; •; outx; •; outx; •.]

Remark. Recently, Amadio, Castellani and Sangiorgi [3] have given a definition of asynchronous bisimulation, which accounts for the fact that an agent of type X→X

Table 4: Transitions for asynchronous CCS

(act)  \overline{α.P ⟶^{α} P}
(sum) \frac{G ⟶^{α} P}{G + G′ ⟶^{α} P}
(sum′) \frac{G′ ⟶^{α} P}{G + G′ ⟶^{α} P}
(comp) \frac{P ⟶^{α} P′}{P |Q ⟶^{α} P′|Q}
(comp′) \frac{Q ⟶^{α} Q′}{P |Q ⟶^{α} P |Q′}

(synch) \frac{P ⟶^{α} P′  Q ⟶^{ᾱ} Q′}{P |Q ⟶^{τ} P′|Q′}
(res) \frac{P ⟶^{α} P′  α ∉ L ∪ L̄}{P \ L ⟶^{α} P′ \ L}
(rel)  \frac{P ⟶^{α} P′}{P [f] ⟶^{fα} P′[f]}
(rec)  \frac{P ⟶^{α} P′  A^{def} = P}{A ⟶^{α} P′}

might receive a message, and then immediately send it again, without this interaction being observable on the outside. Feedback is concerned with the dual phenomenon, namely a process that sends a message and then immediately receives it again. Out-bufferedness with feedback is characterized up to weak bisimulation by the firstorder axioms that are listed in Table 3.

Theorem 3.3 (Characterization of out-buffered agents with feedback). An agent S: X→_{B}X is out-buffered with feedback if and only if S ≈ T for some agent T satisfying (fb1)–(fb5).

4 Example: Asynchronous CCS

In this section, we will show that an asynchronous version of Milner’s Calculus of Communicating Systems (CCS) [11, 12] fits into the framework outlined in the previous section of out-buffered labeled transition systems with feedback.

Let X = {a, b, c, … } be an infinite set of names, and let X̄ = {ā, b̄, c̄, … } be a corresponding set of co-names, such that X and X̄ are disjoint and in one-to-one correspondence via (¯ ). We also write ¯ ā = a. Names correspond to input-actions, and co-names to output-actions. Let τ ∉ X + X̄, and let Act = X + X̄ + {τ} be the set of actions, ranged over by the letters α, β, …; Let the letter L range over subsets of X, and write L̄ for {ā | a ∈ L}. Let the letter f range over relabeling functions, which are functions f : X → X. Any relabeling function extends to f : Act → Act by letting fā = \overline{fa} and fτ = τ.

Let A, B, C, … range over a fixed set of process constants. Asynchronous CCS processes P, Q, … and guards G, H, … are given by the following grammars:

\begin{matrix}P ::= ā.0 P |P P \ L P [f] A G \\ G ::= a.P τ.P G + G 0 \end{matrix}

Assume a set of defining equations A^{def} = P, one for each process constant A. The operational semantics of asynchronous CCS is given in terms of a labeled transition system S_{CCS} = ⟨S, Act, ⟶⟩, which is defined in Table 4. The states are CCS processes. Notice that we have not specified a distinguished initial state; this is more convenient in this context, and no harm is done. Also notice that there is no rule for 0. This is because the process 0 is inert, i.e.there are no transitions 0 ⟶^{α} P.

Theorem 4.1. The labeled transition system S_{CCS} is out-buffered with feedback.

5 Example: The Core Join Calculus

The join calculus was introduced by Fournet and Gonthier in [7] and further developed in [8]. It is a concurrent, message passing calculus like the π-calculus. However, the reaction rule is simpler and closer to the semantics of a chemical abstract machine. Here, we will only be concerned with the core join calculus.

Let x, y, … range over a countable set N of names. Let x̃, ỹ, … range over sequences of names. Core join calculus processes P, Q, … and rules R, S, … are given by the following grammars:

P ::= x⟨ỹ⟩ P |P def R_{1} ∧ … ∧ R_{m} in P R ::= x_{1}(ṽ_{1})| … |x_{n}(ṽ_{n}) ⊳ P

A process of the form x⟨ṽ⟩ is called a message. In the rule R = x_{1}(ṽ_{1})| … |x_{n}(ṽ_{n}) ⊳ P, the names ṽ_{1} … ṽ_{n} are bound, and they are assumed to be distinct. The names x_{1} … x_{n} are called the defined names of R, denoted dn(R). Finally, all of the defined names of R_{1}, …, R_{m} are bound in the process def R_{1} ∧ … ∧ R_{m} in P. For a more comprehensive treatment, see [7, 8].

The semantics of the core join calculus is given in the style of a chemical abstract machine. A state Δ ⊢_{N} Π is a multiset Δ of rules together with a multiset Π of processes. N is a set of names, such that fn(Δ, Π) ⊆ N. We identify states up to α-equivalence, i.e. up to renaming of bound variables. The transitions of this machine follow a simple idea: the processes on the right hand side evolve according to the rules on the left-hand side. There are two kinds of transitions: structural transitions, denoted ⇀, and reactions, denoted ↦:

(str1 )  Δ ⊢_{N} Π, P |Q ⇀ Δ ⊢_{N} Π, P, Q
(str2 ) Δ ⊢_{N} Π, def R_{1} ∧ … ∧ R_{m} in P ⇀ Δ, R_{1}, …, R_{m} ⊢_{N′} Π, P
where N′ = N + dn(R_{1} , …, R_{m})
(join)  Δ ⊢_{N} Π, x_{1}⟨ỹ_{1}⟩, …, x_{n}⟨ỹ_{n}⟩ ↦ Δ ⊢_{N} Π, [ỹ_{1}/ṽ_{1}, …, ỹ_{n}/ṽ_{n}]P
where (x_{1}(ṽ_{1})| … |x_{n}(ṽ_{n}) ⊳ P) ∈ Δ

The rule (join) is of course only applicable is the length of ỹ_{i} and ṽ_{i} are the same, for all i. Note that in the rule (str2 ), the sets N and dn(R_{1} , …, R_{m}) must be disjoint; this may necessitate renaming some bound variables in def R_{1} ∧ … ∧ R_{m} in P.

Table 5: Second-order axioms for out-buffered agents

[figure: s; ≈≻^{outy}; α; t; s′] ⇒ [figure: s; ≈≻^{outy}; α; t; α; s′; ≈≻^{outy}; t′]

where α ≠ outy (ob1*)

[figure: s; ≈≻^{outy}; t; α; t′] ⇒ [figure: s; ≈≻^{outy}; α; t; α; s′; ≈≻^{outy}; t′]

where α ≠ outy (ob2*)

[figure: s; ≈≻^{outy}; outy; t; s′] ⇒ [figure: s; ≈≻^{outy}; outy; t; τ; s′; ≈; t′]

(ob3*)

s ≈≻^{outy} t ⇒ s ⟹^{outy}≈ t

(ob4*)

s ⟶^{outy} t ⇒ s ⇒^{τ}≈≻^{outy} t

where s reachable (ob5*)

Remark. In the original formulation of the join calculus [7, 8], the structural rules are assumed to be reversible. We adopt a different convention here. To fit the join calculus into our framework, we make it into a labeled transition system with input and output. Let X = {x⟨ỹ⟩ | x ∈ N , ỹ ∈ N^{∗}} be the set of messages. We add input and output transitions:

(in)  Δ ⊢_{N} Π ⟶^{inx⟨ỹ⟩} Δ ⊢_{N∪{x,ỹ}} Π, x⟨ỹ⟩
(out) Δ ⊢_{N} Π, x⟨ỹ⟩ ⟶^{outx⟨ỹ⟩} Δ ⊢_{N} Π

Further, we let ⟶^{τ} = ⇀ ∪ ↦. With these definitions, the join calculus defines a labeled transition system S_{join}: X→X.

Theorem 5.1. The labeled transition system S_{join} defined by the core join calculus is out-buffered with feedback.

6 Other Characterizations of Asynchrony

In Sections 2 and 3, we have characterized notions of asynchrony by first-order axioms up to weak bisimulation. It is possible to remove the words “up to weak bisimulation”, i.e.to characterize asynchrony directly. This happens at the cost of introducing secondorder axioms. The shift to second-order seems to be inevitable, since weak bisimulation itself is a second-order notion.

The axioms for out-buffered agents are given in Tables 5. It is possible to give corresponding axioms for in-bufferedness, out-queuedness and in-queuedness.

Theorem 6.1. An agent S: X→_{B}Y is out-buffered if and only if for each y ∈ Y there

exists a binary relation ≈≻^{outy} ⊆ |S| × |S| satisfying (ob1*)–(ob5*).

7 Conclusions and Future Work

We have shown how to abstractly characterize various notions of asynchrony in a general-purpose framework, independently of any particular process paradigm. This can be done by first-order axioms up to weak bisimulation, or by higher-order axioms “on the nose”. The present framework of labeled transition systems with input and output can be used to model asynchronous communication in CCS, as well as the join calculus. To give an adequate treatment of calculi with explicit, dynamic scoping operators, such as the π-calculus, one should equip these labeled transition systems with the ability to handle dynamically created names. Work is in progress on a notion of fibered labeled transition system that can be used to model this more general situation.

References

[1] S. Abramsky. Interaction categories and communicating sequential processes. In A. W. Roscoe, editor, A Classical Mind: Essays in honour of C. A. R. Hoare, pages 1–16. Prentice Hall International, 1994.

[2] S. Abramsky, S. Gay, and R. Nagarajan. Interaction categories and typed concurrent programming. In Proceedings of the 1994 Marktoberdorf Summer School. Springer, 1994.

[3] R. M. Amadio, I. Castellani, and D. Sangiorgi. On bisimulations for the asynchronous π-calculus. In CONCUR ’96, Springer LNCS 1119, pages 147–162, 1996.

[4] M. A. Bednarczyk. Categories of asynchronous systems. PhD thesis, University of Sussex, 1988.

[5] G. Berry and G. Boudol. The chemical abstract machine. Theoretical Computer Science, 96:217–248, 1992.

[6] G. Boudol. Asynchrony and the π-calculus. Technical Report 1702, INRIA, Sophia-Antipolis, 1992.

[7] C. Fournet and G. Gonthier. The reflexive cham and the join-calculus. In POPL ’96, 1996.

[8] C. Fournet, G. Gonthier, J.-J. Levy, L. Maranget, and D. Remy. A calculus of mobile agents. In CONCUR ’96, Springer LNCS 1119, pages 406–421, 1996.

[9] K. Honda and M. Tokoro. An object calculus for asynchronous communication. In Proc. ECOOP 91, Geneve, 1991.

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

[11] R. Milner. A Calculus of Communicationg Systems. Springer LNCS 92. 1980.

[12] R. Milner. Operational and algebraic semantics of concurrent processes. Technical report, University of Edinburgh, Nov. 1987. Chapter for the Handbook of Theoretical Computer Science.

[13] C. Palamidessi. Comparing the expressive power of the synchronous and the asynchronous π-calculus. In POPL ’97 (Paris), 1997.

[14] M. W. Shields. Concurrent machines. Theoretical Computer Science, 28:449–465, 1985.