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

Axioms for Asynchronous Processes

by

Eleftherios Matsikoudis

A dissertation submitted in partial satisfaction of the

requirements for the degree of

Doctor of Philosophy

in

Electrical Engineering and Computer Sciences

in the

Graduate Division

of the

University of California, Berkeley

**Committee in charge:**

Professor Edward A. Lee, Chair

Professor Christos H. Papadimitriou

Professor Leo A. Harrington

Fall 2010

Axioms for Asynchronous Processes

Copyright 2010 by Eleftherios Matsikoudis Abstract Axioms for Asynchronous Processes by Eleftherios Matsikoudis Doctor of Philosophy in Electrical Engineering and Computer Sciences University of California, Berkeley Professor Edward A. Lee, Chair From classical computability theory to modern programming language design, the mathematical concept of function has dominated our perception of sequential computation.

But as soon as we venture into the realm of concurrent interaction, it is well understood that this concept has to be abandoned. What are we to replace it with?

This question is considered too general to admit a deﬁnitive answer. If we want such an answer, we must be willing to narrow our scope, and impose some constraint on the form of concurrent interaction that we choose to consider. Here, we derive such a constraint solely from the intuitive notion of asynchrony. And under this constraint, we propose a mathematical concept of sequential asynchronous process, which we deﬁne axiomatically, and put forward as the sought replacement to the classical function.

Our theory is an interleaving theory. And traditionally, interleaving theories have failed to integrate a satisfactory treatment of what is known as the ﬁnite delay property, according to which, if a process can make progress, then it will eventually do so, but after an arbitrary amount of time. This failure is generally attributed to the so-called expansion law of such theories, which reduces parallel execution to indeterminate serialization. But in truth, the problem is deeply rooted in the concept of labelled transition system, which is the pervasive mathematical object underlying such theories.

To solve this problem, we introduce a new type of system, in which, instead of labelled transitions, we have, essentially, sequences of labelled transitions. We call systems of this type labelled execution systems. We use a coalgebraic representation to obtain a proper concept of bisimilarity among such systems, and study the conditions under which that concept agrees with the intuitive notion of branching equivalence that one has for them.

Finally, we examine the diﬀerence in expressive power and branching complexity between labelled execution systems and labelled transition systems.

The intended interpretation of our concept of asynchronous process is a state of what we

Chapter 1 Introduction From classical computability theory to modern programming language design, the mathematical concept of function has dominated our perception of sequential computation.

But as soon as we venture into the realm of concurrent interaction, it is well understood that this concept has to be abandoned. What are we to replace it with?

This question is considered too general to admit a deﬁnitive answer. If we want such an answer, we must be willing to narrow our scope, and impose some constraint on the form of concurrent interaction that we choose to consider. Here, we derive such a constraint solely from the intuitive notion of asynchrony. And under this constraint, we propose a mathematical concept of sequential asynchronous process, which we deﬁne axiomatically, and put forward as the sought replacement to the classical function.

Our theory is an interleaving theory. And traditionally, interleaving theories have failed to integrate a satisfactory treatment of what is known as the ﬁnite delay property, according to which, if a process can make progress, then it will eventually do so, but after an arbitrary amount of time. This failure is generally attributed to the so-called expansion law of such theories, which reduces parallel execution to indeterminate serialization. But in truth, the problem is deeply rooted in the concept of labelled transition system, which is the pervasive mathematical object underlying such theories.

To solve this problem, we introduce a new type of system, in which, instead of labelled transitions, we have, essentially, sequences of labelled transitions. We call systems of this type labelled execution systems. We use a coalgebraic representation to obtain a proper concept of bisimilarity among such systems, and study the conditions under which that concept agrees with the intuitive notion of branching equivalence that one has for them.

Finally, we examine the diﬀerence in expressive power and branching complexity between labelled execution systems and labelled transition systems.

The intended interpretation of our concept of asynchronous process is a state of what we

## CHAPTER 1. INTRODUCTION 2

may think of as a very large labelled execution system, and the role of our axioms is to ﬁx the shape of that system.There are two groups of axioms. The ﬁrst group is used to specify the form of the executions of the system, and the way in which they branch oﬀ one another, in a manner consistent with our intuitive notion of behaviour of an asynchronous process. The second group is deduced from a single extremal axiom asserting the ﬁnality of the system in a covariety of coalgebras relating to the ﬁrst group of axioms, and is used to guarantee that every behaviour is accounted for exactly once.

Chapter 2 Transition Systems

2.1 Basic deﬁnitions Deﬁnition 2.1.1. A transition system is an ordered pair S, T such that the following are

**true:**

(b) T is a binary relation1 on S.

Assume a transition system S, T.

We write s −→T s if and only if s T s.

We call any s ∈ S a state of S, T, and any s, s ∈ graph T a transition of S, T.

The concept of transition system is ubiquitous in computer science: Turing machines, rewriting systems, Kripke structures are only but a few examples. But as versatile as it is, one cannot use it to model anything more about an individual transition than a change of state in the system. And we will need more than that.

Assume a non-empty set L of labels.

(b) T is a binary relation between S and L × S.

Assume an L-labelled transition system S, T.

l We write s −→T s if and only if s T l, s.

We call any s ∈ S a state of S, T, and any s, l, s ∈ graph T a transition of S, T.

Labelled transition systems have been around at least since Moore’s work on ﬁnite automata in [43], where they appeared in tabular as well as pictorial form. In their present form, they were ﬁrst introduced by Keller in [32], where they were called named transition systems. And although Keller used them to model parallel computation, it was apparently Milner who ﬁrst saw labels as shared vehicles of interaction, and labelled transition systems as models of communicating behaviour, paving the way for [37] and the advent of process algebra.

Assume L-labelled transition systems S1, T1 and S2, T2.

Deﬁnition 2.1.3. A bisimulation between S1, T1 and S2, T2 is a binary relation

**B : S1 ↔ S2 such that for any s1 and s2 such that s1 B s2, the following are true:**

s0 and s0 are bisimilar among the ﬁrst two diagrams; neither of them is bisimilar to s0.

The idea of bisimilarity is that for any path branching out of either one of the two states, there is a path branching out of the other one, that carries the same labels in the same order, and goes through states that are again related to the corresponding states of the ﬁrst path in the same way. This last piece of recursion is what separates bisimilarity from trace equivalence, making the former sensitive to the branching potential of each state.

Notice that a transition system can be thought of as a labelled transition system, every transition of which is decorated with a single ﬁxed label. This induces a concept of bisimulation between transition systems: simply erase every instance of l in the above deﬁnition.2 The concept of bisimulation is due to David Park (see [46]), and is without doubt the most signiﬁcant contribution of the theory of concurrency to the broader arena of computer science and mathematics at large.3 After learning about Milner’s work in [39], where bisimulation was worked out in the context of a calculus for the ﬁrst time, and prompted by the perception of an analogy between the mathematical notion of a set and that of a process with just one kind of action, Peter Aczel used transition systems to model a theory of sets that need not be well founded, and the concept of bisimulation to strengthen, in a sensible and pleasing way, the Axiom of Extensionality therein (see [2]).4 But then he went further. He noticed that transition systems could be viewed as coalgebras for a certain endofunctor, and models of his axiom as ﬁnal objects in a suitable category of such coalgebras. Work on a generalization of this result culminated in [5] to bear a ﬁnal coalgebra theorem, asserting the existence of ﬁnal coalgebras for a wide range of common endofunctors, and a categorical deﬁnition of bisimulation, generalizing the latter as a viable This will be a common theme throughout this and the next chapter: we will often state deﬁnitions and prove statements only for the labelled case; a proper “unlabelling” will immediately carry these over to the non-labelled case.

To be fair, the concept of bisimulation has been independently discovered in the ﬁelds of modal logic and set theory as well. See [58] for a comprehensive historical account.

Forti and Honsell had already discovered and used the concept of bisimulation to that end in [22]. But here, we are not so much interested in non-well-founded set theory, but rather in the developments following Aczel’s work on it.

** CHAPTER 2. TRANSITION SYSTEMS 6 coalgebraic dual to the algebraic notion of congruence.**

This led eventually to a general theory of universal coalgebra (see [56]).

We will now begin to recast things in this coalgebraic framework. This will be of great technical as well as conceptual use, especially in the next chapter, when we replace the concept of transition system with another one, more apt to our purpose. Working with coalgebras, we will need to make reference to a few common concepts from category theory, and some familiarity with the latter will at times be useful. But such familiarity is not assumed, and we will make an eﬀort to supplement each category-theoretic deﬁnition or argument with a concrete explanation.

2.2 From systems to coalgebras Consider once more the concept of transition system. We have formalized this as a set of states together with a binary relation on that set. But there is another way: to look at this binary relation as a set-valued function.

Assume sets S1 and S2.

Assume a binary relation R : S1 ↔ S2.

We write fun R for a function5 from S1 to P S2 such that for any s1 ∈ S1,

By Proposition 2.2.1, a transition system S, T can be represented as a function from S to P S, namely as fun T, and conversely, a function τ : S → P S can be represented as a transition system, namely as S, rel τ. Thus, we could alternatively deﬁne a transition system to be a function from a set to the power set of that set, or more verbosely, a pair of a set S and a function τ : S → P S. This would be a coalgebraic deﬁnition, one we shall have more to say about after a more general introduction into the concept of coalgebra.

A coalgebra is deﬁned relative to an endofunctor, and an endofunctor is deﬁned relative to a category.

A category is just a two-sorted partial algebra of objects and arrows, with an identity, a domain, a codomain, and a composition operation, satisfying a couple of simple equational axioms. These operations assume their suggested meaning in every concrete category, where any object is a set, possibly with some structure, and any arrow is a function from one set to another, typically preserving structure.

For reasons that will soon become clear, we shall want to work with some very large categories, the collections of whose objects and arrows are not sets, not even proper classes.

The ﬁrst such category that we will be working with is the category of all classes7 and all class functions8 between them.

We write Class for the category whose objects are all the classes, and arrows all the class functions.

It is of course only in a generalized sense that we may think of Class as a partial algebra.

All the same, we shall not worry too much about this, or any other issue of foundational nature. Such issues can be addressed in one way or another (for example, see [35, chap. I] or [6, chap. 2]), but a thorough treatment here would only obscure the presentation of our ideas. And in any case, we will avoid impredicative constructions and comprehension principles that test the consistency of the theory.

A functor is a category homomorphism: a structure-preserving map from one category to another.

An endofunctor is a functor from a category to that same category.

For example, an endofunctor on Class is a map from Class to Class that maps classes to classes and class functions to class functions, preserving the identity operation on classes, and the domain, codomain, and composition operation on class functions.

A collection C of sets is a class if and only if there is a unary formula ϕ of set theory such that for every set S, S ∈ C if and only if ϕ(S) is true.

A class function f is an ordered triple D, C, G such that D is a class, C is a class, G ⊆ D × C, and for every d, c1 and c2, if d, c1 ∈ G and d, c2 ∈ G, then c1 = c2. We write dom f for D, cod f for C, and graph f for G. We call dom f the domain of f, cod f the codomain of f, and graph f the graph of f.