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

And it is not hard to see that gen τ is the greatest ﬁxed point of Gτ, with respect to the aforementioned pointwise ordering. Therefore, we can read Corollary 3.4.9 as saying that every post-ﬁxed point of Gτ is below the greatest ﬁxed point of Gτ in that ordering, which is precisely what the coinduction proof technique of [42] mandates. Unlike the latter, we could not have used Tarski’s Lattice-theoretical Fixpoint Theorem (see [61, thm. 1]) to deduce our proof rule here. For if C is a proper class, then Pow Seq(L × C) is not a complete lattice under inclusion, and so neither is the induced ordering of class functions from C to Pow Seq(L × C). Nevertheless, the principle is the same.

Note that an ordered set can be viewed as a category, an order-preserving function on that set as a functor on that category, and a post-ﬁxed point of that function as a coalgebra for that functor. And if that ordered set is a complete lattice, then, by Tarski’s ﬁxed-point theorem, there is a ﬁnal coalgebra for that functor. And so the coinduction proof technique of [42] is just another variation of the general ﬁnality theme that lies behind the coinduction proof principle of Theorem 2.4.2. The same, of course, is true for the more ad hoc proof rule of Corollary 3.4.9.

For a historical account on the emergence of coinduction in computer science, we refer to [58].

We have now ﬁnally reached our generability characterization theorem.

**Theorem 3.4.11. ε is generable if and only if the following are true:**

Thus, by generalization, (c) is true.

For every c and e, if e ∈ (gen τ )(c) and ∈ (gen τ )(c), then, by Corollary 3.4.10, τ (c) = ∅, and hence, e =. Thus, (d) is true.

By Theorem 3.4.5 and the Axiom of Dependent Choice, (e) is true.

Conversely, suppose that (a), (b), (c), (d), and (e) are true.

We prove that ε = gen(η(C) ◦ ε).

Assume c ∈ C and e ∈ ε(c).

, then, by (d), ε(c) = { }, and thus, η(C)(ε(c)) = ∅.

If e = Otherwise, there is l, c, and e such that ·e.

e= l, c Thus, by deﬁnition of η, l, c ∈ η(C)(ε(c)), and by (a), e ∈ ε(c ).

Thus, by generalization, ε is consistent with η(C) ◦ ε, and by Corollary 3.4.9, for any c ∈ C, ε(c) ⊆ (gen(η(C) ◦ ε))(c).

And since η(C)(ε(c )) = ∅, by (e), tailj+1 e ∈ ε(c ).

Otherwise, there is k n + 1 such that j + 1 = k. Then there is l, c, l, c, and e2 such that l, c ∈ η(C)(ε(c )) and

Thus, by (c), e2 ∈ ε(c ). And since l, c ∈ η(C)(ε(c)), there is e1 such that l, c · e1 ∈ ε(c). Thus, by (b), l, c · e2 ∈ ε(c), and hence, e ∈ ε(c).

Thus, by generalization, for any c ∈ C, ε(c) ⊇ (gen(h(C) ◦ ε))(c).

Thus, ε = gen(h(C) ◦ ε), and hence, ε is generable.

Clause (a) of Theorem 3.4.11 corresponds to suﬃx closure, clause (b), conditioned on (a), to fusion closure, and clause (c) to limit closure. Clause (d) asserts the impossibility of indeterminate termination. Finally, clause (e) is the non-triviality condition discussed earlier, and essentially replaces Emerson’s left totality condition on the generating transition relation (see [20]).

Each of these ﬁve properties has come about in connection with a diﬀerent cause of failure of the converse of Proposition 3.3.4, and hence of Proposition 3.3.1 and 3.3.2. And if we have been thorough enough, we should expect that the conjunction of all ﬁve properties be suﬃcient a condition for eliminating that failure altogether. This turns out to be the case.

We say that C, ε is generable if and only if ε is generable.

** Theorem 3.4.**

12. If C1, ε1 and C2, ε2 are generable, then h is a homomorphism from C1, ε1 to C2, ε2 if and only if h is a homomorphism from the L-labelled transition coalgebra C1, η(C1 ) ◦ ε1 to the L-labelled transition coalgebra C2, η(C2 ) ◦ ε2.

Then, by Proposition 3.3.1, h is a homomorphism from the L-labelled transition coalgebra C1, η(C1 ) ◦ ε1 to the L-labelled transition coalgebra C2, η(C2 ) ◦ ε2.

Conversely, suppose that h is a homomorphism from C1, η(C1 ) ◦ ε1 to C2, η(C2 ) ◦ ε2.

Let ε2 be a class function from C2 to Pow Seq(L × C2 ) such that for any c2 ∈ C2,

And since h is a homomorphism from C1, η(C1 ) ◦ ε1 to C2, η(C2 ) ◦ ε2, l, h(c1 ) ∈ (η(C2 ) ◦ ε2 )(c2 ).

Thus, by generalization, ε2 is consistent with η(C2 ) ◦ ε2. Then, by Corollary 3.4.9, for any c2 ∈ C 2,

Therefore, for any c1 ∈ C1, (Pow Seq(L × h))(ε1 (c1 )) ⊆ ε2 (h(c1 )).

We use induction to prove that for any c1 ∈ C1 and any ﬁnite e2 ∈ ε2 (h(c1 )), there is e1 ∈ ε1 (c1 ) such that

, then (η(C2 ) ◦ ε2 )(h(c1 )) = ∅, and since h is a homomorphism from If e2 = C1, η(C1 ) ◦ ε1 to C2, η(C2 ) ◦ ε2, (η(C1 ) ◦ ε1 )(c1 ) = ∅. Thus, ∈ ε1 (c1 ).

Otherwise, by Corollary 3.4.10, there is l, c2, and e2 such that l, c2 ∈ (η(C2 ) ◦ ε2 )(h(c1 )), e2 ∈ ε2 (h(c1 )), and

and tailn+1 e2 ∈ ε2 (h(c1 )). Thus, by Corollary 3.4.10, there is l, c2, and e2 such that l, c2 ∈ (η(C2 ) ◦ ε2 )(h(c1 )), e2 ∈ ε2 (c2 ), and

Thus, by generalization, for every s ∈ S, there is s such that s R s. Then, by the Axiom of Dependent Choice, there is an inﬁnite sequence d over S such that for every n ∈ ω, head tailn d R head tailn+1 d.

Let n = sec head d.

We use induction to prove that for every j n + 1, there is l, c1, and e1 such that l, c1, j ∈ W (j), e1 ∈ ε1 (c1 ), and

(Seq(L × h))( l, c1 · (Seq(proj1 ((L × C1 ) × ω)))(tail d)) = tailj e2.

Otherwise, there is k n + 1 such that j + 1 = k. By the induction hypothesis, there is l, c1, and e1 such that l, c1, k ∈ W (k), e1 ∈ ε1 (c1 ), and

Since l, c1, k ∈ W (k), there is l, c1, j ∈ W (j) such that l, c1 ∈ (η(C1 ) ◦ ε1 )(c1 ) and head tailk e2 = l, h(c1 ). And clearly, l, c1 · e1 ∈ ε1 (c1 ) and

**The following is immediate from Theorem 2.2.10 and 3.4.12:**

** Theorem 3.4.**

13. If C1, ε1 and C2, ε2 are generable, then B is a bisimulation between C1, ε1 and C2, ε2 if and only if B is a bisimulation between the L-labelled transition coalgebra C1, η(C1 ) ◦ ε1 and the L-labelled transition coalgebra C2, η(C2 ) ◦ ε2.

Once more, we can translate all this back to the system side of the theory.

Assume a binary relation T : S ↔ L × S.

Assume a binary relation E : S ↔ S (L × S).

We write ET (E) for a binary relation between S and S (L × S) such that for any s ∈ S and every e ∈ S (L × S),

**The following is trivial:**

Proposition 3.4.14. ET (E) = rel Gfun T (fun E).

We think of ET as a function on binary relations between S and S (L × S). And the reason that we are interested in this function is that it preserves the ordering of binary relations between S and S (L × S) induced by the inclusion relation on their graphs: for every binary relation E1, E2 : S ↔ S (L × S), if

This ordering is of course a complete lattice, and hence, by Tarski’s Lattice-theoretical Fixpoint Theorem, so is the set of all ﬁxed points of ET.

We write exec T for the greatest ﬁxed point of ET.

Notice that here, the coinduction proof technique of [42] is directly applicable.

** The following follows from Proposition 3.4.14 and the fact that gen fun T is the greatest ﬁxed point of Gfun T :**

We say that T generates E if and only if exec T = E.

We say that E is generable if and only if there is a binary relation between S and L × S that generates E.

**The following is immediate from Proposition 2.2.1 and 3.4.15:**

Proposition 3.4.16. E is generable if and only if fun E is generable.

**The following is immediate from Proposition 2.2.1, 3.3.3, 3.4.15, and 3.4.16:**

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

(b) if E is generable, then exec trans E = E.

We say that S, E is generable if and only if E is generable.

**The following is immediate from Proposition 3.4.16:**

Proposition 3.4.18. S, E is generable if and only if the L-labelled execution coalgebra S, fun E is generable.

The following is immediate from Proposition 2.2.1(b), 2.2.15, 3.2.4, and 3.3.3, and

**Theorem 3.4.13:**

** Theorem 3.4.**

19. If S1, E1 and S2, E2 are generable, then B is a bisimulation between S1, E1 and S2, E2 if and only if B is a bisimulation between the L-labelled transition systems S1, trans E1 and S2, trans E2.

We would like to ﬁnish this section with a few remarks.

Proposition 3.4.17 and Theorem 3.4.19 conﬁrm what has been implicit throughout this section: generable labelled execution systems are just another representation of labelled transition systems. This is even more evident in the coalgebra side of the theory, where, by Proposition 3.4.7 and Theorem 3.4.12, the category of all generable labelled execution coalgebras and all homomorphisms between them is isomorphic to (Pow ◦ (L × Id))-Coalg.

Thus, for all practical purposes, generable labelled execution coalgebras are equivalent to labelled transition coalgebras.

In light of this equivalence, Theorem 3.4.11 does not just characterize generable labelled execution coalgebras. It marks the boundary between the expressive power of labelled transition coalgebras and labelled execution coalgebras. And what it implies is that there CHAPTER 3. EXECUTION SYSTEMS 86 is no sense in choosing the latter over the former, unless we are willing to give up one or more of the ﬁve properties listed in the respective clauses of Theorem 3.4.11.

In the next chapter, we will give up two of these properties: limit closure and impossibility of indeterminate termination. Giving up limit closure will enable us to faithfully model the ﬁnite delay property, so intrinsically bound to the notion of asynchrony. And indeterminate termination will provide us with the means to simulate the behaviour of a capricious environment that may at any time cease to produce input stimuli.

3.5 Behaviour modelling and covarieties In Section 2.4, in order to motivate the study of ﬁnal coalgebras, we considered a hypothetical scenario, in which we used L-labelled transition systems to model the behaviour of processes of some kind. And for simplicity, we assumed that any state of every L-labelled transition system modelled the behaviour of some process of that kind.

Here, we wish to consider a diﬀerent scenario, in which we use L-labelled execution systems instead. And this time, we make no such simplifying assumption.

We have already seen examples of labelled execution systems that are not suitable for modelling the behaviour of processes. In Section 3.3, we argued that non-Abrahamson systems should be excluded from consideration. And in the next chapter, we will exclude even more systems, leaving only those that conform with our intuitive notion of behaviour of an asynchronous process.

In cases like these, a ﬁnal L-labelled execution coalgebra is no longer the right choice of model. Sure, every behaviour modelled within the class of systems under consideration is accounted for exactly once in such a coalgebra. But there are more behaviours in there, which are neither needed nor wanted. What is required then is a suitable generalization of the ﬁnal coalgebra approach of the previous chapter.

We will need a couple of last concepts from category theory.

A subcategory of a category is a collection of objects and arrows of that category that is closed under the identity, domain, codomain, and composition operation of that category.

A full subcategory of a category is a subcategory of that category, whose arrows between any two objects are all the arrows between the two objects in that category.

Notice that a full subcategory is completely determined by its objects.

In Section 2.4, we were interested in the terminal object of F -Coalg. Here, by a similar reduction, we are interested in the terminal object of a full subcategory of F -Coalg.

** CHAPTER 3. EXECUTION SYSTEMS 87 Assume a full subcategory S of F -Coalg.**

We say that C, γ is ﬁnal in S if and only if C, γ is in S, and for every F -coalgebra C, γ in S, there is exactly one homomorphism from C, γ to C, γ.

Clearly, not every full subcategory of F -Coalg has a ﬁnal F -coalgebra. But as we will see, every “reasonably speciﬁed” one does.

We say that S is closed under the formation of homomorphic images if and only if for every F -coalgebra C, γ, if C, γ is in S, and C, γ is a homomorphic image of C, γ, then C, γ is in S.

We say that S is closed under the formation of subcoalgebras if and only if for every F -coalgebra C, γ, if C, γ is in S, and C, γ is a subcoalgebra of C, γ, then C, γ is in S.

We say that S is closed under the formation of direct sums if and only if for every class-indexed family { Ci, γi }i∈I of F -coalgebras, if for every i ∈ I, Ci, γi is in S, then i∈I Ci, γi is in S.

Deﬁnition 3.5.1. An F -covariety is a full subcategory C of F -Coalg such that the

**following are true:**

(a) C is closed under the formation of homomorphic images;

(b) C is closed under the formation of subcoalgebras;

(c) C is closed under the formation of direct sums.