# «A dissertation submitted in partial satisfaction of the requirements for the degree of Doctor of Philosophy in Electrical Engineering and Computer ...»

The word asynchronous is derived from the Greek word ασύγχρονος. The latter is a compound of the privative preﬁx α-, the preﬁx συν-, in the sense of of identical, and χρόνος, the Greek word for time. It is used in a strict sense to assert that one does not coincide in time with another, or, more often, in a loose sense to assert that one need not coincide in time with another. And in the context of concurrency theory, it is the only in a loose sense that it can be used without any contradiction. For if two events must be non-synchronized, then there is a synchronization between the presence of the one and absence of the other.

## CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 94

The most important implication from this intuitive notion of asynchrony is that communication must be unidirectional. In other words, in an asynchronous setting, if a process wants to communicate with another process, then the most it can do is pass a message for it to read at its own leisure. And this means that there must be some place to leave that message. Therefore, a process is determined by a number of ports, or mailboxes, as we like to call them, which is the interface of the process to the outside world.Based on this, we shall now give an informal, anthropomorphic description of how we think an asynchronous process works. The precise concept will only be understood after the axioms are presented. But this informal description will be very useful in understanding the intuition behind the mathematics, and we shall return frequently to it. We only advise the reader not to take it too literally.

We shall then think of an asynchronous process as an organization of people. And this organization will communicate with the outside world through the exchange of messages.

Speciﬁcally, it will have a number of mailboxes, and a number of workers and messengers.

We will not constrain the internal structure of the mailboxes at all. These may act as bounded or unbounded buﬀers, ﬁrst-in-ﬁrst-out queues or push-and-pop stacks, single-token places or multisets. The workers inside the organization will be responsible for the operation of the organization, and their access to these mailboxes will too be left unconstrained. For all we know, a worker might choose to ignore all messages, or might be sitting behind a mailbox waiting for the next message. Finally, the messengers will be responsible for delivering messages to other organizations, and thus, represent the communication capabilities of the organization. And while the number of mailboxes will be considered ﬁxed for an organization, the number of workers and messengers will, in principle, be allowed to vary.

Here, we will focus on a speciﬁc type of asynchronous process, a sequential asynchronous process. What this corresponds to in our anthropomorphic description is the constraint that there be just one worker. Messengers may by many and variable, but there is always going to be a single worker.

4.2 Asynchronous process types Our ﬁrst step is to formalize this anthropomorphic notion of interface of a process.

Deﬁnition 4.2.1. An asynchronous process type is an ordered pair I, O such that the

**following are true:**

(c) dom I and dom O are disjoint.

In an asynchronous process type I, O, I represents that mailboxes of a process, and the types of messages that can be deposited to them. O, on the other hand, represents all the mailboxes that a process might deposit a message to, and all the kinds of messages it might deposit. This creates some redundancy, but a typed approach greatly simpliﬁes things.

Note that the constraint that dom I and dom O be disjoint makes sense from an observational point of view: if a process deposits a message to itself, only it can observe that deposition.

One interesting question here is why we have decided to make the number of input and output channels countable when we have intentionally left everything else unbounded. The reason is simple: our executions are ﬁnite or inﬁnite sequences, as they must be if we want our processes to maintain a connection with reality. And thus, a process with an uncountable number of channels could never communicate over all of them through its lifetime.

4.3 Systems and coalgebras The type of an asynchronous process determines the diﬀerent kinds of actions that it can perform. Basically, these are input actions, which are to be understood as the event of deposition of a message to a mailbox of the process, output actions, which correspond to the deposition of a message by a messenger of the process to some mailbox, and internal actions, which model the work done internally by the workers of the process.

Assume an asynchronous process type I, O.

We write actin I, O for { i, m | i ∈ dom I and m ∈ I(i)}.

We write actout I, O for { o, m | o ∈ dom O and m ∈ O(o)}.

We write τ for ∅.

We write act I, O for actin I, O ∪ actout I, O ∪ {τ }.

## CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 96

We call any i, m ∈ actin I, O an input action, any o, m ∈ actout I, O an output action, and τ an internal action.Notice that the choice of ∅ for τ is arbitrary. Any object diﬀerent from an ordered pair would do. The symbol itself is used for conformance with the literature.

It is also worth noting that there is no predeﬁned set of actions. Any pair of functions satisfying the deﬁnition of an asynchronous process type will do.

We now begin to formalize our notion of process. The ﬁrst step is to deﬁne a notion of path. This is understood as any ﬁnite or inﬁnite sequence of steps through the underlying transition system of a labelled execution system.

Assume an (act I, O )-labelled execution system S, E.

We write paths S, E for the largest subset X of S × S (act I, O × S) such that for every

**s, e ∈ X, one of the following is true:**

(i) e = ;

α (ii) there is α, s, and e such that s −→trans E s, s, e ∈ X, and ·e.

e= α, s The existence of a largest such set is easily veriﬁed by straightforward order-theoretic arguments, which we will henceforth omit.

We next begin to deﬁne a notion of fairness for such paths. Intuitively, we want every diﬀerent party involved in the execution of a process to be given the chance to proceed.

This include the worker of the process, the messengers, and of course the environment.

However, we want to place as little constraints as possible, making sure that in the end, every possible interleaving of them will be part of the behaviour of the process.

Assume s, e ∈ paths S, E.

We say that τ is eventually in s, e if and only if s, e is a member of the smallest set X

**such that the following are true:**

τ (i) for every s, s, and e, if s −→trans E s and s, e ∈ paths S, E, then s, τ, s · e ∈ X;

α (ii) for every s, α, s, and e, if s −→trans E s and s, e ∈ X, then s, α, s · e ∈ X.

The meaning of these two predicates should be clear. The ﬁrst asserts that in an execution, the worker does at some point make progress, and the second that at some point in the execution, the worker cannot make progress.

The following is meant to take care the progress of a messenger.

o,m Assume o, m ∈ actout I, O and s such that s −→ trans E s.

We say that o, m, s is eventually in s, e if and only if s, e is a member of the

**smallest set X such that the following are true:**

Here, the situation is more complex. The problem is that at any point, there may be more than one messenger with identical messages and destinations. If we used the same type of predicate as in the case of an internal action, there would be cases where a messenger was put on hold forever, just because another messenger with the same message and destination was making progress. And for all we know, the behaviour of the worker may depend on the identity of the available messengers. In Deﬁnition 4.3.1, the necessary conﬂuence constraints are imposed so that the above method does indeed guarantee that every single messenger will eventually make progress.

With these inductively deﬁned predicates, we can now deﬁne a notion of fairness coinductively.

We say that s, e is fair in S, E if and only if s, e is a member of the largest subset X

**of paths S, E such that for every s, e ∈ X, one of the following is true:**

We note that similar approaches of iterated induction and coinduction to fairness have been used before (for example, see [45]).

By requiring the executions of a process to coincide with all fair paths in the underlying labelled transition system, we guarantee that all diﬀerent interleavings of the worker, the messengers, and the environment are accounted for.

Deﬁnition 4.3.1.

**A sequential asynchronous process system of type I, O is an (act I, O )-labelled execution system S, E such that the following are true:**

We brieﬂy go over the clauses of this deﬁnition.

Clause (a) corresponds to the most basic assumption of asynchrony, that we should be able to deposit any kind of message in any mailbox at any time. Diagrammatically, we have the

**following representation:**

Here, the dashed line is used to signify existence of the corresponding transition, which is understood as a transition of the underlying labelled transition system of the sequential asynchronous process system.

Clause (b) formalizes the idea that the eﬀect of deposition of a message in a mailbox is uniquely determined. In other words, there are no diﬀerent ways of depositing a message in

**a mailbox. Diagrammatically, we have the following:**

## CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 100

Clause (c) is the last clause concerned with input, and what it states is essentially that diﬀerent mailboxes are physically distinct. Thus, depositing messages to two diﬀerent mailboxes in any order will have the same eﬀect in the content of each mailbox. This is

**portrayed in the following conﬂuent diagram:**

Clauses (d), (e), and (f) are concerned with output, and essentially, assert that a messenger can never be recalled. Once a decision is made, and a messenger is dispatched, that messenger will insist until his job is done. This is expressed by the conﬂuence of the

**following three diagrams:**

Clause (g) is the last of the clauses that constrain the underlying labelled transition system, and is, as we shall see, somewhat controversial. Essentially, what it asserts is that it cannot be the case that a worker waits for a messenger to continue with his job. This clearly precludes the situation where there is only one person in the organization, switching between a worker and a messenger. This is the intuitive idea behind the following

**commutative diagram:**

## CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 101

Finally, clause (h) is the place where our work begins to pay oﬀ. All previous clauses concern transitions, and while more general than the typical approach to asynchrony (for example, see [59]), are after all expressed in terms of labelled transition systems. It is in (h), where we begin to express properties about our systems that are impossible to capture with labelled transition systems. And this will become all the more important, when we use our coalgebraic framework to obtain an extensional model for these properties.

To be formal, we repeat all the above, this time for labelled execution coalgebras.

Assume an (act I, O )-labelled execution coalgebra C, ε.

We write paths C, ε for the largest subclass X of C × Seq(act I, O × C) such that for

**every c, e ∈ X, one of the following is true:**

Assume c, e ∈ paths C, ε.

We say that τ is eventually in c, e if and only if c, e is a member of the smallest set X

**such that the following are true:**

We say that c, e is fair in C, ε if and only if c, e is a member of the largest subset X

**of paths C, ε such that for every c, e ∈ X, one of the following is true:**

Deﬁnition 4.3.2.

**A sequential asynchronous process coalgebra of type I, O is an (act I, O )-labelled execution coalgebra C, ε such that the following are true:**

Clearly, sequential asynchronous process systems and small sequential asynchronous process coalgebras are the same objects in diﬀerent guises.

Assume a sequential asynchronous process system S, E of type I, O.

## CHAPTER 4. SEQUENTIAL ASYNCHRONOUS PROCESSES 104

Assume a sequential asynchronous process coalgebra C, ε of type I, O.**The following is immediate from :**

**Proposition 4.3.3. The following are true:**

(a) the (act I, O )-labelled execution coalgebra S, fun E is a sequential asynchronous process coalgebra of type I, O ;

(b) if C, ε is small, then the (act I, O )-labelled execution system C, rel ε is a sequential asynchronous process system of type I, O.

We write SAPC I,O for the category whose objects are all the asynchronous process coalgebras of type I, O, and arrows all the homomorphisms from one asynchronous process coalgebra of type I, O to another.

Clearly, SAPC I,O is a full subcategory of (Pow ◦ Seq ◦ (act I, O × Id))-Coalg.

**The following is straightforward from Proposition 3.3.1 and a routine proof by cases:**

** Theorem 4.3.**

4. SAPC I,O is a (Pow ◦ Seq ◦ (act I, O × Id))-covariety.