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

The concept of F -covariety is the coalgebraic counterpart of the concept of F -variety, which is a generalization, in the same sense as before, of the concept of Σ-variety, what Birkhoﬀ called a family of algebras when he introduced the concept in [13]. It is our idea of a “reasonably speciﬁed” full subcategory of F -Coalg.

For example, the category of all Abrahamson labelled execution coalgebras, deﬁned in the obvious way, and all homomorphisms between them is a (Pow ◦ Seq ◦ (L × Id))-covariety, as is the category of all generable labelled execution coalgebras and all homomorphisms between them. But we will not need to prove this here.

Just as we did with the notion of ﬁnality, we generalize the notion of completeness to full subcategories.

We say that C, γ is complete in S if and only if C, γ is in S, and for every F -coalgebra C, γ in S and any c ∈ C, there is exactly one c ∈ C such that c and c are bisimilar among C, γ and C, γ.

**The following is a generalization of Theorem 2.4.13:**

CHAPTER 3. EXECUTION SYSTEMS 88

**Theorem 3.5.2. For every F -covariety C, the following are true:**

(a) C, γ is ﬁnal in C;

(b) for every small F -coalgebra C, γ in C, there is exactly one homomorphism from C, γ to C, γ ;

(c) C, γ is complete in C;

(d) for every small F -coalgebra C, γ in C, and any c ∈ C, there is exactly one c ∈ C such that c and c are bisimilar among C, γ and C, γ.

Proof. See proof of Theorem 2.4.13.

The reason that we were able to reuse the proof of Theorem 2.4.13 here without any modiﬁcation or adjustment is that, because of the closure properties of an F -covariety, all relevant constructions in that proof can be carried out inside C. The only structures in that proof that are not necessarily in C are the bisimulations, which are not supposed to either.

**The following is a generalization of Theorem 2.5.1:**

** Theorem 3.5.**

3. For every F -covariety C, there is an F -coalgebra that is ﬁnal in C.

Proof. Assume an F -covariety C.

Let C, γ be an F -coalgebra that is ﬁnal in F -Coalg.

Let C, γ be a direct sum of all small F -coalgebras in C.

Let h be the unique homomorphism from C, γ to C, γ.

Then, by Theorem 2.4.5, there is a class function ρ : ran h → F (ran h) such that

Let ι be the canonical injection map from C to C.

Then h ◦ ι is a homomorphism from C, γ to ran h, ρ.

Suppose, toward contradiction, that there are homomorphisms h1 and h2 from C, γ to ran h, ρ such that

contrary to C, γ being ﬁnal in F -Coalg.

Therefore, there is at most one homomorphism from C, γ to ran h, ρ.

Thus, there is exactly one homomorphism, namely h ◦ ι, from C, γ to ran h, ρ.

Thus, by generalization and Theorem 3.5.2, ran h, ρ is ﬁnal in C.

** Theorem 3.5.**

3 is easy enough to be already known. But being unable to trace it in the literature, we have taken care to prove it here (but see [3, thm 2.2]).

3.6 Execution systems in the literature The process algebra literature is dominated by the concept of labelled transition system.

And to some extent, this is understandable. For process algebra emerged from a marriage of Plotkin’s structural operational semantics (see [48]), and Keller’s named transition systems (see [32]) (see [41, chap. 12], [12], [49], and [10]). This marriage was the work of Robin Milner, and is most clearly expounded in [41], but was already present in [36], where the so-called expansion law was stated for the ﬁrst time.

The expansion law has been a constant source of controversy in the theory of concurrency.

In the language of Milner’s CCS (see [40], [41]), a typical equation asserted by the law is

**the following:**

** a.0 | b.0 = a.b.0 + b.a.0.**

Here, ‘a’ and ‘b’ stand for arbitrary actions, ‘0’ for the inactive agent, which is incapable of performing any action, ‘.’ for sequential composition, ‘|’ for parallel composition, and ‘+’ for alternative composition. Thus, the intended meaning of the equation is that the parallel CHAPTER 3. EXECUTION SYSTEMS 90 execution of a and b is “equivalent”, in some sense, to the indeterminate serialization of the two.

In order to justify the expansion law, and the blurring between causal dependence and

**temporal precedence resulting from it, Milner wrote the following in [36, p. 81]:**

We do not yet know how to frame a suﬃciently general law without, in a sense, explicating parallelism in terms of non-determinism. More precisely, this means that we explicate a (parallel) composition by presenting all serializations - or interleavings - of its possible atomic actions. This has the disadvantage that we lose distinction between causally necessary sequence, and sequence which is ﬁctitiously imposed upon causally independent actions; [... ]. However, it may be justiﬁed to ignore it if we can accept the view that, in observing (communicating with) a composite system, we make our observations in a deﬁnite time sequence, thereby causing a sequencing of actions which, for the system itself, are causally independent.

Eﬀectively, what he argued for was a dichotomy between causation and observation in the theory of concurrency. And what he proposed as an observational view to the theory was the interleaving of the atomic actions of the various agents inside a system as would be perceived by a single, sequential observer outside the system. But what he failed to recognize was that the expansion law is in fact inconsistent with that view.

To understand the mismatch, consider the following equation derived from the expansion

**law, again in the language of CCS:**

ﬁx(X = a.X) | ﬁx(X = b.X) = ﬁx(X = a.X + b.X).

Here, we use recursion expressions to deﬁne agents with inﬁnite behaviour. Thus, ﬁx(X = a.X) is an agent that forever iterates a, ﬁx(X = b.X) one that forever iterates b, and ﬁx(X = a.X + b.X) one that at each iteration, does either a or b, indeterminately choosing between the two. But whereas every inﬁnite sequence over {a, b} is a trace of a possible execution of ﬁx(X = a.X + b.X), not every such sequence is consistent with what could be perceived by a sequential observer of ﬁx(X = a.X) | ﬁx(X = b.X). Indeed, only those sequences that contain an inﬁnite number of a’s and an inﬁnite number of b’s are.

For if ﬁx(X = a.X) and ﬁx(X = b.X) execute in parallel, each of them must eventually perform an inﬁnite number of actions, and each of these actions must eventually be perceived by any sequential observer of ﬁx(X = a.X) | ﬁx(X = b.X).

All this goes unnoticed in the ﬁnite case, because interleaving the executions of two ﬁnite agents is ultimately equivalent to indeterminately alternating between the two. But the expansion law blindly carried that equivalence over to the inﬁnite case. And this created CHAPTER 3. EXECUTION SYSTEMS 91 confusion. The word “interleaving” became synonymous to the word “indeterminate”, and the observational view was robbed of its power to express liveness properties such as ﬁnite delay or termination.

Of course, it is not the expansion law per se that is to blame for this confusion.

Interleaving is an operation on executions, not transitions, and the use of labelled transition systems was always going to cause problems with it. But instead of replacing transitions with executions in their systems, people started augmenting them with all kinds of diﬀerent pieces of information that would allow them to distinguish the “admissible” sequences of transitions from the “inadmissible” ones. And more often than not, the result was a type of modelling structure that could no longer claim adherence to the observational view. The few attempts that did use executions directly, at least those that we are aware of (see [18], [17]), were not concerned with organizing them into structures and looking at their branching properties, and anyway, seem to have received only scant attention, possibly due to their poor presentation.

The ﬁrst place where we do see executions organized into structures is not process algebra, but temporal logic. These so-called path structures (see Section 3.1) are quite popular in the beginning. We do not see a formal concept of bisimulation for them, but there is deﬁnitely interest in their branching properties. The notions of suﬃx, fusion, and limit closure are all deﬁned in connection with path structures. Eventually, they give way to Kripke structures, inherited from modal logic, and claimed to provide “a setting more appropriate to concurrency” (see [21, p. 152]). They do not. But despite the voices of reason asking for a separation between implementation and correctness issues in reasoning about concurrent programs (for example, see [16]), transitions remain in the lead role.

In [26], Hennessy and Stirling introduce what appears to be the ﬁrst type of labelled execution system in the literature. They call systems of that type general transition systems, and in their deﬁnition, demand not only suﬃx and fusion closure, but preﬁx closure as well, with the justiﬁcation that it “also appears to be natural” (see [26, p. 27]).

They also deﬁne a concept of extended bisimulation for such systems, which is basically the same as our formally derived concept of bisimulation between labelled executions systems (see Deﬁnition 3.2.3). The focus in [26] is in logic, and speciﬁcally, in a generalization of Hennessy-Milner Logic (see [25]) to general transition systems. But what is surprising is that no attempt is later made to apply the ideas of general transition systems and extended bisimulations to the semantics of processes.

More than ten years later, these ideas pop up in a “very rough and incomplete draft” of Aczel (see [4]), who is aware of Hennessy’s work in [24], a precursor of [26], but apparently, unaware of the work in [26] (see footnote in [4, p. 3]). Aczel’s intention is to apply the ﬁnal universe approach of [3] to the semantics of Milner’s SCCS with ﬁnite delay (see [38]). But his execution is indeed “very rough and incomplete”. The proposed type of structure is a generalized type of labelled transition system, where each state is equipped with the set of CHAPTER 3. EXECUTION SYSTEMS 92 all inﬁnite sequences of transitions “admissible” from that state. An added condition of “stability” makes structures of that type ultimately equivalent to the general transition systems of [26], but only because the latter are preﬁx closed. Eventually, these structures are represented as coalgebras over Class, and [3, thm. 2.2] is used to prove the existence of a ﬁnal coalgebra in the full subcategory of all such coalgebras that are “stable”.

The only other place where we ﬁnd these ideas applied to the semantics of processes is [27].

The starting point is again Milner’s SCCS with ﬁnite delay, and the structures used are practically the same as in [4]. But the approach is purely categorical. Indeed, the main goal in [27] is showing how much can be done within category theory alone. Apparently, a lot, but not without cost.

Comparing [26], [4], and [27] with our work here, there are two things that we think stand out and would like to mention.

First, as regards the general idea underlying the concept of labelled execution system, we ﬁnd that in all three of [26], [4], and [27], the notion of indeterminate termination, and its use in modelling the behaviour of reactive systems, has been completely overlooked. This is easy to put right in [26], where preﬁx closure is an added feature, but not so in [4] and [27], where the property is practically built into the structure of a system.

Second, as regards the formalization of the idea, we believe that the present approach represents a great simpliﬁcation, both conceptually and notationally, over what was done in all three of [26], [4], and [27], and hope that the reader will appreciate the power and elegance of our framework, which, we think, are felt in every part of the theory.

It should be emphasized that the precedence of [26], [4], and [27] over our work here is not causal, only temporal. Our ideas were developed, and for the most part, worked out before any acquaintance with these studies. The above review was mainly driven by our curiosity to understand why ideas that in retrospect seem so natural have not found their way into the household of the average concurrency theorist.

In the end, one can only speculate. But one thing is certain: if matters of pedagogy have played any role in this, transition semantics have deﬁnitely proﬁted from it; for people like pictures, and execution systems are impossible to draw.

Chapter 4 Sequential Asynchronous Processes

4.1 Our intuitive notion of asynchronous process What is a process? This is a question that has troubled concurrency theorists ever since the birth of the ﬁeld almost ﬁfty year ago. And yet, there is still very little agreement as to what the answer is. With the advent of process algebra in the eighties came the well known controversy between so-called true concurrency and interleaving semantics, adding another dimension to the problem.

The central ﬁgure in this controversy was of course Robin Milner, who, as we have seen, was the one to argue for the dichotomy between causation and observation, which can be tersely described as the diﬀerence between events partially ordered by causal dependence, and actions totally ordered by temporal precedence (see [9]). Milner’s idea was nothing less than brilliant. But it was marred by the inadequacies of the used model, the labelled transition system.

Our work thus far has been to ﬁx just that. And we have done so by introducing a model that we believe can do justice to the interleaving approach. We now want to use this model to deﬁne an abstract notion of asynchronous process.