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

Here, we will feel comfortable working with large coalgebras, and refrain from imposing additional constraints, just for the sake of size. Indeed, the very reason that we have decided to work within a theory of classes in the ﬁrst place was not having to worry about size at all. If we want to understand ‘behaviour’ in terms of branching structure, then it seems inappropriate to constrain that structure by means that only reﬂect our own CHAPTER 2. TRANSITION SYSTEMS 49 preconceptions about how that ‘behaviour’ may come about. And a bound on the branching degree of that structure seems to do just that: reﬂect our own bias toward a kind of process that “computes” its own evolution using a ﬁxed set of predeﬁned resources.

Before we leave this chapter, we note that the notion of an F -coalgebra can be deﬁned for any endofunctor F on any arbitrary category, concrete or not. See, for example, [57], for an adaptation of the theory to the categories of metric spaces and ordered sets, or [51], for an entirely axiomatic approach.

Chapter 3 Execution Systems

3.1 From transitions to executions Perhaps the ﬁrst thing to decide when setting out to develop an observational theory of processes of some kind is what the unit of observation should be. For a theory based on the concept of labelled transition system, this unit is eﬀectively ﬁxed to what can be represented by a single transition: a single action or event. But at that scale of observation, it is only the local properties of the behaviour of a process that carry over to the model. Non-local properties, speciﬁcally those concerning inﬁnite executions of the process, do not. For examples of the ﬁrst kind, one may look at safety properties, such as mutual exclusion or deadlock freedom, whereas for examples of the second kind, one may look at liveness properties, such as termination or guaranteed service (see [8]).

We might think of a labelled transition system as an intuitionistic approach to a model of a process. For an intuitionist, an inﬁnite execution cannot possibly claim existence as a completed totality of actions or events. It is only “a manifold of possibilities open towards inﬁnity; it remains forever in the status of creation, but is not a closed realm of things existing in themselves” (see [63, p. 9]). This rejection of the notion of actual inﬁnity is detrimental to the expressiveness of a theory. All limits of partial executions become complete executions in the model, which is the source of bounded indeterminacy (see [19, chap. 9]), and the reason behind the well known problems with properties like fairness ([50]) or ﬁnite delay ([30]) (for example, see [45]).

Here, instead, we take what we might say is a more classical approach, and ﬁx our unit of observation at the level of a complete execution of a process. And for that, we need a diﬀerent type of mathematical structure.

We call any s ∈ S a state of S, E, and any s, e ∈ graph E an execution of S, E.

Notice that an execution is an ordered pair of a state and a sequence of states, rather than a single sequence of states, what might have seemed a more natural option. And while we do think that there is a certain clarity in distinguishing the starting state of an execution from any subsequent step, this was mainly a choice of mathematical convenience. Its merit will soon become apparent.

The idea of an execution system has been around at least since the early days of temporal logic in computer science, in the form of a type of semantic structure called a path structure in [53] (for example, see [52], [1], and [34]). The states of a system would represent the various memory conﬁgurations and control locations traversed in the course of a computation of a possibly concurrent program, and the executions those computations permitted by the assumed implementation, and over which the modalities of the logic were to be interpreted. Here, we will need one more thing: labels.

Deﬁnition 3.1.2. An L-labelled execution system is an ordered pair S, E such that the

**following are true:**

We call any s ∈ S a state of S, E, and any s, e ∈ graph T an execution of S, E.

Despite the rich cross-fertilization of ideas between temporal logic and process algebra, and the obvious parallel between semantic structures and labelled systems in the two ﬁelds, path structures were never really assimilated for use as models of process theories. In fact, the concept of labelled execution system is almost absent from the literature. Looking back For every set S, we write S S for the set of all ﬁnite and inﬁnite sequences over S.

** CHAPTER 3. EXECUTION SYSTEMS 52 to it, we could only ﬁnd a handful of sporadic instances of the general notion.**

We discuss them at the end of this chapter, where we also oﬀer our own opinion on this surprising omission.

3.2 From systems to coalgebras and back As our choice of formalization should have made obvious, the concept of labelled execution system is a direct generalization of that of labelled transition system. The idea of a single step from one state to another is replaced by that of an “admissible” path through the system over which a sequence of steps can be taken. The result is a more elaborate notion of branching structure. And if we are to associate this notion with ‘behaviour’ of some kind, we need to understand what constitutes similarity and dissimilarity of it. In other words, we need a concept of branching equivalence suited to labelled execution systems.

What should that concept be?

In [57], Rutten and Turi propose a simple approach to this type of problem: all we have to do is ﬁnd a suitable endofunctor to represent our systems coalgebraically. We can then use that endofunctor to instantiate the “parametric” concept of bisimulation of Deﬁnition 2.2.8, and obtain not only the equivalence concept that we seek, but a model too that is fully

**Abstract**

with respect to that concept (see Theorem 2.4.13 and 2.5.1).2 This is straightforward here.

We write Seq for an endofunctor on Class that assigns to every class C the class

At this point, the reader may protest against the seeming circularity in the way we have speciﬁed the action of Seq on class functions; what may look like a harmless deﬁnition by recursion is really a descending argument over a possibly inﬁnite deduction sequence: there is no base case. A little thought, however, will suﬃce to convince oneself that there is nothing ambiguous about it. Seq f is a simple lift of f to sequences over dom f. Informally, if c0, c1,... is a sequence over dom f, then (Seq f )( c0, c1,... ) is the result of replacing each ci in that sequence with its own image under f, namely the sequence f (c0 ), f (c1 ),.... We are thus entitled to use this contentious form of speciﬁcation as a deﬁnition. The question is how do we justify it formally.

In principle, we could use induction on the index of a sequence to prove that each point in the sequence is uniquely determined. But we can do better.

First, notice that Seq C2 can be given the structure of a ({ } + (C2 × Id))-coalgebra, where { } + (C2 × Id) is the composite of the left sum endofunctor { } + Id on Class with the left product endofunctor C2 × Id on Class: simply let σ2 be a class function from Seq C2 to { } + (C2 × Seq C2 ) such that for every s ∈ Seq C2,

**Now, we can use f to give Seq C1 the structure of a ({ } + (C2 × Id))-coalgebra as well:**

just let σ1 be a class function from Seq C1 to { } + (C2 × Seq C1 ) such that for every s ∈ Seq C1,

All our deﬁnition says then is that Seq f is a homomorphism from Seq C1, σ1 to Seq C2, σ2. And the existence and uniqueness of this homomorphism follows from the fact that Seq C2, σ2 is actually ﬁnal in ({ } + (C2 × Id))-Coalg, as the reader may wish to prove.

With experience, all this can be inferred immediately by simple inspection of the form of the deﬁning equations. More importantly, the same type of argument can be applied to the case of any endofunctor, even if there is no readily available representation of a ﬁnal coalgebra amenable to inductive reasoning (see [44]). A deﬁnition that relies in this way on the ﬁnality of the implicit target coalgebra is what we call a deﬁnition by corecursion. This particular use of the term appears to have originated with [11], and is justiﬁed by the duality to the more familiar notion of deﬁnition by recursion, which, in similar fashion, relies on the initiality of the implicit source algebra (see [28]).

We can now compose Seq with the left product endofunctor L × Id on Class to obtain the CHAPTER 3. EXECUTION SYSTEMS 54 endofunctor Seq ◦ (L × Id) on Class, which assigns to every class C the class

Finally, we can compose Pow with Seq ◦(L × Id) to obtain the endofunctor Pow ◦ Seq ◦ (L × Id) on Class, which assigns to every class C the class

Just as we did with transition systems, we can take now advantage of the formal analogy between the concepts of binary relation and set-valued function, and use Proposition 2.2.1 to obtain our coalgebraic representation. This unity of treatment is the reward of our aforementioned formalization choice.

By Proposition 2.2.1 then, an L-labelled execution system S, E can be represented as a (Pow ◦ Seq ◦ (L × Id))-coalgebra, namely as S, fun E, and conversely, a (Pow ◦ Seq ◦ (L × Id))-coalgebra C, ε can be represented as an L-labelled execution system, namely as C, rel ε, again with the caveat that C be a set.

For every ordered pair x, y, we write ﬁrst x, y for x, and sec x, y for y.

CHAPTER 3. EXECUTION SYSTEMS 55

At this stage, we could already use Proposition 3.2.4 below as our deﬁnition of bisimulation between labelled execution systems. But we prefer a diﬀerent, more operational one that will help us develop some insight into the concept. And for this, we need some more preparation.

Assume a binary class relation R : C1 ↔ C2.

We write Seq(L × R) for a binary class relation between Seq(L × C1 ) and Seq(L × C2 ) such that for every e1 ∈ Seq(L × C1 ) and every e2 ∈ Seq(L × C2 ),

Seq(L × R) is a simple lift of R to pairs of sequences over dom R and cod R. Informally, if c0, c1,... is a sequence over dom R, and c0, c1,... a sequence over cod R, then

if and only if c0 R c0, c1 R c1, etc. This is, of course, an abuse of notation. But it is a very mild form of abuse. For if R is actually a class function, then Seq(L × R) is the same as the image of R under Seq ◦(L × Id).

Assume L-labelled execution coalgebras C1, ε1 and C2, ε2.

Proposition 3.2.2. B is a bisimulation between C1, ε1 and C2, ε2 if and only if B is a binary class relation between C1, ε1 and C2, ε2, and for any c1 and c2 such that c1 B c2,

**the following are true:**

Proof. Suppose that B is a bisimulation between C1, ε1 and C2, ε2.

Let graph B, β be an L-labelled execution coalgebra such that dpr B is a homomorphism from graph B, β to C1, ε1, and cpr B one from graph B, β to C2, ε2.

Assume c1 and c2 such that c1 B c2.

Then Pow Seq(L × dpr B)(β( c1, c2 )) = ε1 ((dpr B)( c1, c2 )), and hence, by deﬁnition of Pow ◦ Seq ◦ (L × Id) and dpr B, {Seq(L × dpr B)(e) | e ∈ β( c1, c2 )} = ε1 (c1 ).

Thus, by generalization, B is a bisimulation between C1, ε1 and C2, ε2.

Proposition 3.2.2 has the same feel as Proposition 2.2.14. The diﬀerence is that the local check of correspondence of transitions has been replaced by a non-local test of agreement along entire executions. This is conceptually in tune with our intended change in scale of observation from one type of system to the other.

Assume L-labelled execution systems S1, E1 and S2, E2.

Deﬁnition 3.2.3. A bisimulation between S1, E1 and S2, E2 is a binary relation

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

**The following is of course immediate:**

Proposition 3.2.4. B is a bisimulation between S1, E1 and S2, E2 if and only if B is a bisimulation between the L-labelled execution coalgebras S1, fun E1 and S2, fun E2.

We say that B is a bisimulation equivalence on S, E if and only if B is a bisimulation on S, E, and an equivalence relation on S.

We say that s1 and s2 are bisimilar among S1, E1 and S2, E2 if and only if there is a bisimulation B between S1, E1 and S2, E2 such that s1 B s2.

We say that s1 and s2 are bisimilar in S, E if and only if s1 and s2 are bisimilar among S, E and S, E.

3.3 Abrahamson systems Informally, we can explain bisimilarity of states of labelled execution systems in the same way as we did in the case of labelled transition systems. Only now, paths are not implicitly inferred from a transition relation, but explicitly stipulated as part of the system structure.

And this can have some peculiar side eﬀects.

For example, consider two {l1, l2 }-labelled execution systems, whose executions are as

**depicted in the following left and right frames respectively:**

Then s1 and s1 are not bisimilar among the two systems, simply because the execution starting from s2 carries a diﬀerent label than the one starting from s1. But why should we care if it does? The only execution starting from s1 has only one step, labelled l1, and is in perfect agreement with the only execution starting from s1, which also has only one step, also labelled l1. So, intuitively, there is no diﬀerence in branching potential between the two states. We must therefore conclude that bisimilarity is, in this case, inconsistent with our informal sense of equivalence of branching structure.