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

** CHAPTER 2. TRANSITION SYSTEMS 8 One such endofunctor is the functor Pow, which assigns to every class C the class Pow C = {S | S is a subset of C}, 9 and to every class function f : C1 → C2 a class function Pow f : Pow C1 → Pow C2 such that for every S ∈ Pow C1, (Pow f )(S) = {f (s) | s ∈ S}.**

Notice that if the class C is actually a set, then Pow C = P C.

Assume an endofunctor F on Class.

Deﬁnition 2.2.2. An F -coalgebra is an ordered pair C, γ such that the following are

**true:**

(a) C is a class;

(b) γ is a class function from C to F (C).

Assume an F -coalgebra C, γ.

We call C the carrier of C, γ, and γ the cooperation of C, γ.

We say that C, γ is small if and only if C is a set.

We say that C, γ is large if and only if C is a proper class.

By this deﬁnition, a Pow-coalgebra is just an ordered pair C, τ of a class C and a class function τ : C → Pow C, which is precisely what we have recognized as another way to formalize the concept of transition system, with the caveat that C be a set.

Assume a Pow-coalgebra C, τ.

We call C, τ a transition coalgebra.

We write c −→τ c if and only if c ∈ τ (c).

Assume a transition system S, T.

**The following is immediate:**

We use the verbal expression “S is a subset of C” instead of the mathematical expression “S ⊆ C” to emphasize the constraint that S be a set.

CHAPTER 2. TRANSITION SYSTEMS 9

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

(a) s −→T s if and only if s −→fun T s ;

(b) if C, τ is small, then c −→τ c if and only if c −→rel τ c.

This is all very nice, but why bother with this alternative formalization in the ﬁrst place?

To begin with, we need to understand what the informal meaning of the concept of F -coalgebra is. For this, it will help to consider the dual concept of F -algebra ﬁrst, where it is not hard to establish a connection with the more common concept of Σ-algebra, the principal object of study in the theory of universal algebra.

**Deﬁnition 2.2.4. An F -algebra is an ordered pair C, α such that the following are true:**

(a) C is a class;

(b) α is a class function from F (C) to C.

Assume an F -algebra C, α.

We call C the carrier of C, α, and α the operation of C, α.

We say that C, α is small if and only if C is a set.

We say that C, α is large if and only if C is a proper class.

Notice that the only diﬀerence between the deﬁnition of an F -algebra and that of an F -coalgebra is in the direction of the class function, which is reversed. Hence the duality.

Now, the way to think of the concept of F -algebra is as a generalization of the concept of Σ-algebra.

For example, consider a single-sorted signature Σ. We may think of Σ as a set of operation symbols, each annotated with a unique natural number, the arity of that symbol. A Σ-algebra is a semantic interpretation of Σ: a set S, the carrier set of the algebra, together with one n-ary operation fσ on S for each operation symbol σ of arity n in Σ. These operations may be combined together into a single function

then a Σ-algebra is just a small F -algebra.

Algebra is about composition of things. In a Σ-algebra, this composition takes a very speciﬁc form: things are composed according to certain rules, the operations of the Σ-algebra, and each rule determines a unique thing for every ordered n-tuple of things, where n is arbitrary but ﬁxed for that rule. There is no fundamental reason, though, why composition must be restricted to this form. One might, for example, think of a rule that determines a new composite thing for every possible set of things. And if C is the class of all things, then a rule of this kind can be represented simply as a class function from Pow C to C, which is precisely what a Pow-algebra is. In general, an F -algebra C, α will represent one or several rules for composing particular combinations of things, as speciﬁed and encoded by F, into other things, as determined by α.

We may now appeal to the duality between the concepts of F -algebra and F -coalgebra to attach a plausible informal sense to the latter: if F -algebras are generalized rules of composition, then F -coalgebras are generalized rules of decomposition.

Under this interpretation, a transition coalgebra will represent a rule for decomposing each thing in the carrier of the coalgebra to a set of other things in it. This, of course, imposes a particular view on a transition system: each state of the system is a composite thing, decomposed by the cooperation of the corresponding coalgebra to the set of all immediate successors of it in the system. And this may not be the most intuitive view to impose on a transition system. But never mind. The merit of the coalgebraic approach is not in the interpretation per se, but in the machinery available for relating the corresponding decomposition structure of one system to that of another.

Assume F -coalgebras C1, γ1 and C2, γ2.

Deﬁnition 2.2.5. A homomorphism from C1, γ1 to C2, γ2 is a class function h : C1 → C2 such that

We say that h is a monomorphism from C1, γ1 to C2, γ2 if and only if h is an injective homomorphism from C1, γ1 to C2, γ2.

We say that h is an epimorphism from C1, γ1 to C2, γ2 if and only if h is a surjective homomorphism from C1, γ1 to C2, γ2.

We say that C1, γ1 is a homomorphic image of C2, γ2 if and only if there is an epimorphism from C2, γ2 to C1, γ1.

We say that h is an isomorphism between C1, γ1 and C2, γ2 if and only if h is a bijective homomorphism from C1, γ1 to C2, γ2.

Proposition 2.2.6. If h is an isomorphism between C1, γ1 and C2, γ2, then h−1 is an isomorphism between C2, γ2 and C1, γ1.

Proof. See [56, prop. 2.3].

We say that C1, γ1 and C2, γ2 are isomorphic if and only if there is an isomorphism between C1, γ1 to C2, γ2.

We write C1, γ1 ∼ C2, γ2 if and only if C1, γ1 and C2, γ2 are isomorphic.

= Assume an F -coalgebra C, γ.

We say that h is an endomorphism on C, γ if and only if h is a homomorphism from C, γ to C, γ.

We say that h is an automorphism on C, γ if and only if h is an isomorphism between C, γ to C, γ.

The concept of homomorphism from one F -coalgebra to another is the coalgebraic counterpart of the concept of homomorphism from one F -algebra to another, which is a generalization, in the same sense as before, of the concept of homomorphism from one Σ-algebra to another. It is a structure-preserving map carrying the decomposition patterns CHAPTER 2. TRANSITION SYSTEMS 12 of one coalgebra to those of another. In particular, it establishes a similarity of structure between its domain and range.

In the case of Pow, this similarity can take a very familiar form.

** Example 2.2.**

7. Assume transition coalgebras C1, τ1 and C2, τ2.

Suppose that h is a homomorphism from C1, τ1 to C2, τ2.

Assume c1 ∈ C1.

**By extensionality, this is equivalent to the following being true:**

(i) if c1 −→τ1 c1, then h(c1 ) −→τ2 h(c1 );

(ii) if h(c1 ) −→τ2 c2, then there is c1 such that c1 −→τ1 c1 and c2 = h(c1 ).

(i) and (ii) look very much like the deﬁning clauses of the concept of bisimulation between transition systems. And indeed, if C1, τ1 and C2, τ2 are small, then, by Proposition 2.2.3(b), we may simply replace each instance of τ1 with rel τ1 and each instance of τ2 with rel τ2 in (i) and (ii), to conclude, by generalization, that graph h is a bisimulation between the transition systems C1, rel τ1 and C2, rel τ2.

From the perception of this connection between the concepts of homomorphism and bisimulation, it is a small step to a coalgebraic generalization of the latter.

Thus, B is a bisimulation between C1, γ1 and C2, γ2 just as long as it is a binary class relation between C1 and C2, and there is a class function β : graph B → F (graph B) such

**that the following diagram commutes:**

We say that B is a bisimulation on C, γ if and only if B is a bisimulation between C, γ and C, γ.

We say that B is a bisimulation equivalence on C, γ if and only if B is a bisimulation on C, γ, and an equivalence class relation on C.

So, a binary class relation between two F -coalgebras is a bisimulation just as long as we can impart it with the structure of an F -coalgebra in a way that turns the projections from the graph of the class relation to the carriers of the two F -coalgebras into homomorphisms.

In general, however, there might be more than one way to do this.

** Example 2.2.**

9. Let S = {0, 1}, and τ be a function from S to Pow S deﬁned by the

**following mapping:**

0 → S;

1 → S.

**Another is deﬁned by the following mapping:**

→{ };

0, 0 0, 1, 1, 0 →{ };

0, 1 0, 0, 1, 1 →{ };

1, 0 0, 0, 1, 1 →{ }.

1, 1 0, 1, 1, 0 In fact, there is nothing special about the graph of the class relation and its projections either.

** Theorem 2.2.**

10. B is a bisimulation between C1, γ1 and C2, γ2 if and only if there is an F -coalgebra C, γ, a homomorphism h1 from C, γ to C1, γ1, and a homomorphism h2 from C, γ to C2, γ2, such that

Proof. See [56, lem. 5.3] and [23, thm. 5.11].

Assume F -coalgebras C1, γ and C2, γ.

**The following is immediate:**

Corollary 2.2.11. If B is a bisimulation between C1, γ1 and C2, γ2, h1 a homomorphism from C1, γ1 to C1, γ1, and h2 a homomorphism from C2, γ2 to C2, γ2, is a bisimulation between C1, γ1 and C2, γ2.

**The following will come of use:**

** Theorem 2.2.**

12. For every class-indexed family {Bi }i∈I of bisimulations between C1, γ1 and C2, γ2, there is a bisimulation B between C1, γ1 and C2, γ2 such that

This coalgebraic deﬁnition of bisimulation was ﬁrst introduced in [5], and does indeed generalize the concept of bisimulation between labelled transition systems. To see this, we must ﬁrst go over the coalgebraic representation of such systems.

The functor that we are going to use is the endofunctor Pow ◦ (L × Id) on Class, namely the composite of Pow with the left product endofunctor L × Id on Class, which assigns to every class C the class

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

Assume a (Pow ◦ (L × Id))-coalgebra C, τ.

We call C, τ an L-labelled transition coalgebra.

l We write c −→τ c if and only if l, c ∈ τ (c).

Assume an L-labelled transition system S, T.

**The following is immediate:**

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

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

Let graph B, β be an L-labelled transition 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.

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

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

The following is immediate from Proposition 2.2.13(a), 2.2.14, and the deﬁnition of

**bisimulation between labelled transition systems:**

Proposition 2.2.15. B is a bisimulation between S1, T1 and S2, T2 if and only if B is a bisimulation between the L-labelled transition coalgebras S1, fun T1 and S2, fun T2.

Proposition 2.2.14 and 2.2.15 can of course be adapted for transition coalgebras and transition systems: simply replace every instance of Pow ◦ (L × Id) with Pow, and erase every instance of l.

The ﬁrst thing to note is that every bisimulation equivalence is the equivalence kernel of a homomorphism. In a theory of sets, this is straightforward. But in a theory of classes, some care is needed.

Assume a class C and an equivalence class relation E on C.

We say that q is a quotient of C with respect to E if and only if q is a surjective class function such that dom q = C and ker q = E.

In [5], existence of quotients is deduced from an assumed global form of the Axiom of Choice, and in [3], from a postulated quotient existence principle for classes. In a theory of sets, there is no such need: for every set S and every equivalence relation R on S, one can simply turn to the quotient set of S by R, namely the set

But in a theory of classes, these constructs are not, in general, well deﬁned. For example, if R is the full binary class relation on a proper class C, then for every c ∈ C,

which cannot be a member of any class.

Here, we will assume existence of quotients as a theorem of the underlying theory of classes, and not worry about its precise deduction. We only remark that in the standard von Neumann-Bernays-G¨del theory of classes, existence of quotients is readily deduced o from the Axiom of Limitation of Size.

Assume an F -coalgebra C, γ.

Proposition 2.3.1. For every bisimulation equivalence B on C, γ, and every quotient q of C with respect to B, there is exactly one F -coalgebra cod q, δ such that q is an epimorphism from C, γ to cod q, δ.

Proof. See [5, lem. 5.1 and prop. 6.1].