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

In [20], Emerson called a set of paths limit closed provided that for every inﬁnite, strictly increasing chain of ﬁnite preﬁxes of paths in the set, the limit of that chain, in the standard topology of sequences, is again a path in the set. This property was apparently also ﬁrst considered in [1]. But it was Emerson in [20] who proved the independence of all three closure properties, and the equivalence of their conjunction to the existence of a transition relation generating the given set of paths. Apart from the absence of labels, which has no bearing in this particular discussion, Emerson’s setup was diﬀerent in that paths were always inﬁnite. But this too is of no importance in our examples, which, in light of Emerson’s result, appear to implicate violation of limit closure in the failure of the underlying labelled transition system to subsume all the branching information relevant to a given Abrahamson system.

Our next example is perhaps the most curious one.

**Consider the simple {l}-labelled transition system portrayed in the following diagram:**

There are exactly three Abrahamson {l}-labelled execution systems that one can lay over this labelled transition system. The ﬁrst is the one whose only execution corresponds to the only inﬁnite path in the diagram. The second is the one whose executions correspond to all ﬁnite paths in the diagram. And of course, the third is the one whose executions are all executions of the ﬁrst and second system. But s is not bisimilar with itself among any two of the three.

Informally, the second system is not limit closed, and this is one part of the problem. But the ﬁrst and third are, and so there must be something more going on here. The answer is in the diﬀerence between Emerson’s setup and ours mentioned earlier. Here, executions are not always inﬁnite. In a system that is, informally, suﬃx closed, if there is a ﬁnite execution, then there is an empty execution. And an empty execution creates a type of branching that is impossible to mimic in a labelled transition system.

In an Abrahamson system that is used to model the behaviour of a process, an empty execution can be used to model termination. But if there is another, non-empty execution starting from the same state, then termination becomes a branching choice, one that does not show up in the “possible next step” relation of the system. This feature of indeterminate termination, as we might call it, can seem a little odd at ﬁrst, but is really a highly versatile mechanism, particularly useful in modelling idling in absence of input stimuli, as we shall see in the next chapter.

CHAPTER 3. EXECUTION SYSTEMS 66

**Finally, consider the labelled transition system of the following, trivial diagram:**

There are exactly two labelled execution systems that one can lay over this labelled transition system: one that has one execution, the empty execution, and one that has no execution. And of course, s is not bisimilar with itself among the two.

This degenerate case deserves little comment. We only remark that in a suﬃx closed system, if a state has no execution starting from it, then it has no execution going through it.

At this point, we have found ﬁve possible causes of failure for the converse of Proposition 3.3.4. We have chosen our examples carefully, to examine each of the ﬁve separately and independently from one another. And we have observed how each of the ﬁrst three connects to violation of one of the three closure properties that have been shown to collectively characterize sets of inﬁnite paths generable by a transition relation. But ﬁnite paths add another dimension to the problem, rendering Emerson’s characterization result obsolete. What we will show next is that impossibility of indeterminate termination, along with a non-triviality condition guarding against the occurrence of an isolated state, can be added to the conditions of suﬃx, fusion, and limit closure, to produce a complete characterization of system generability, insensitive to the length of the executions.

First, we need to make the notion of generability precise. For generality, we transfer ourselves again to the coalgebra side of the theory.

Assume a class function τ : C → Pow(L × C).

Assume c ∈ C.

Assume e ∈ Seq(L × C).

**We say that e is a τ -orbit of c if and only if the following are true:**

(i) one of the following is true:

Here again, it is the computational interpretation that is most helpful. If we think of τ as a representation of the control ﬂow graph of a possibly indeterminate sequential program, then a τ -orbit of c corresponds to a total execution of that program starting from the node represented by c.

Now, we would like to say that a class function from C to Pow Seq(L × C)) is generated by τ just as long as it assigns to any c ∈ C the set of all τ -orbits of c. But ﬁrst, we need to make sure that this really is a set, and not a proper class.

We write Wτ (c) for a class function from ω to Pow(L × C) such that

We think of Wτ (c) as a wave emitted by c, and propagating through L × C according to τ, and Wτ (c)(n) as the wavefront at the nth time instance.

Proposition 3.4.1. If e is a τ -orbit of c, then for every n ∈ ω, if tailn e =, then head tailn e ∈ Wτ (c)(n).

Proof. We use induction.

If n = 0, then tailn e = e. Thus, if tailn e =, then there is l, c, and e such that l, c ∈ τ (c) and

Proposition 3.4.2. For every n ∈ ω, Wτ (c)(n) is a set.

Proof. We use induction.

If n = 0, then Wτ (c)(n) = τ (c), which, by deﬁnition of Pow, is a set.

Otherwise, there is m ∈ ω such that n = m + 1. By the induction hypothesis, Wτ (c)(m) is a set. Then clearly, Wτ (c)(m + 1) is a set, and so Wτ (c)(n) is a set.

Therefore, for every n ∈ ω, Wτ (c)(n) is a set.

Proposition 3.4.3. {e | e ∈ Seq(L × C) and e is a τ -orbit of c} is a set.

Proof. By Proposition 3.4.1, for every e ∈ Seq(L × C), if e is a τ -orbit of c, then

is a set.

Proposition 3.4.2 and 3.4.3 will be taken for granted in the sequel.

We write gen τ for a class function from C to Pow Seq(L × C) such that for any c ∈ C,

Assume a class function ε : C → Pow Seq(L × C).

We say that τ generates ε if and only if gen τ = ε.

We say that ε is generable if and only if there is a class function from C to Pow(L × C) that generates ε.

Now, suppose that ε is indeed generable. Can there be more than one class function from C to Pow(L × C) that generates ε?

We could perhaps use the following tentative argument to convince ourselves that this cannot be the case: if τ1 and τ2 are two diﬀerent class functions from C to Pow(L × C), then there must be c ∈ C and l, c ∈ L × C such that either l, c ∈ τ1 (c) and l, c ∈ τ2 (c), or CHAPTER 3. EXECUTION SYSTEMS 69 l, c ∈ τ1 (c) and l, c ∈ τ2 (c); and assuming, without any loss of generality, the former, we can preﬁx any τ1 -orbit of c with l, c to get a τ1 -orbit of c that cannot be a τ2 -orbit of c. But how do we know if there is a τ1 -orbit of c to preﬁx with l, c ?

If τ1 (c ) = ∅, then is a τ1 -orbit of c. If τ1 (c ) = ∅, then we would again expect that there is at least one τ1 -orbit of c. For we could imagine constructing one by ﬁrst choosing a pair l, c in τ1 (c ), then a pair l, c in τ1 (c ), then a pair l, c in τ1 (c ), and so on forever, or until we reach a point where there is no pair to choose. If we never reach such a point, then this construction will involve an inﬁnite number of choices. This suggests that the Axiom of Choice, or some other, weaker form of it, might be necessary to prove the statement that for every suitable τ and c, there is a τ -orbit of c. And indeed, this statement is equivalent to the Axiom of Dependent Choice.

**We will need the following lemma:**

** Lemma 3.4.**

4. For every n ∈ ω, if there is l, c ∈ Wτ (c)(n) and e ∈ Seq(L × C) such that e is a τ -orbit of c, then there is e ∈ Seq(L × C) such that e is a τ -orbit of c.

(a) for every class C, every class function τ : C → Pow(L × C), and any c ∈ C, there is e ∈ Seq(L × C) such that e is a τ -orbit of c;

(b) for every non-empty set S and every binary relation R on S, if for every s ∈ S, there is s such that s R s, then there is an inﬁnite sequence d over S such that for every n ∈ ω, head tailn d R head tailn+1 d.

Let s be a member of S.

Since (a) is true, there is e ∈ Seq(L × S) such that e is a τ -orbit of s. And by an easy induction, for every n ∈ ω, tailn e =.

Let d be an inﬁnite sequence over S such that for every n ∈ ω,

Then for every l, c ∈ S, there is l, c such that l, c R l, c, and thus, since (b) is true, there is an inﬁnite sequence d over S such that for every n ∈ ω, head tailn d R head tailn+1 d. And clearly, there is n ∈ ω and l, c ∈ Wτ (c)(n) such that

and tail d is a τ -orbit of c. Thus, by Lemma 3.4.4, there is e ∈ Seq(L × C) such that e is a τ -orbit of c.

Thus, by generalization, (a) is true.

We can now make our tentative argument formal.

Assume class functions τ1, τ2 : C → Pow(L × C).

Proposition 3.4.6. If τ1 = τ2, then gen τ1 = gen τ2.

Proof. Suppose that τ1 = τ2.

Then there is c, l, and c such that either l, c ∈ τ1 (c) and l, c ∈ τ2 (c), or l, c ∈ τ1 (c) and l, c ∈ τ2 (c).

Without any loss of generality, assume the former.

Let e be a sequence in Seq(L × C) that is a τ1 -orbit of c.

·e.

Let e = l, c Then e ∈ (gen τ1 )(c), but e ∈ (gen τ2 )(c). Thus, gen τ1 = gen τ2.

If we think of gen as an operator from cooperations of L-labelled transition coalgebras to cooperations of L-labelled execution coalgebras, then we can read Proposition 3.4.6 as saying that that operator is injective. So it must have a left inverse. The following shows that that left inverse is the composition on the left with the image of the carrier of the

**corresponding L-labelled execution coalgebra under η:**

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

(a) η(C) ◦ gen τ = τ ;

(b) if ε is generable, then ε = gen(η(C) ◦ ε).

Thus, (b) is true.

Before we move on to our characterization theorem, we have one last stop to make. We have built our notion of generability around the idea of a τ -orbit. And we have tried to formalize the latter in the most conceptually direct way. But as eﬀective as that formalization has been, there is still reason to consider another one. First, it is ugly. And second, there is a very simple but powerful proof rule that it is entirely oblivious to.

We say that ε is consistent with τ if and only if for any c ∈ C and any e ∈ ε(c), one of the

**following is true:**

(b) there is a class function ε : C → Pow Seq(L × C) such that ε is consistent with τ, and e ∈ ε(c).

Proof. Suppose that (a) is true.

Let ε be a class function from C to Pow Seq(L × C) such that for every c and e, e ∈ ε(c )

**if and only if one of the following is true:**

Then, by (ii), e ∈ ε(c ). Thus, clause (ii) of the consistency property is true.

Therefore, ε is consistent with τ.

Thus, (b) is true.

Conversely, suppose (b) is true, Then clause (i) of the property of being a τ -orbit of c is true.

By an easy induction, for every n ∈ ω, if tailn e =, then there is l and c such that

Thus, by generalization, clause (ii) of the property of being a τ -orbit of c is true.

Therefore, (a) is true.

**The following is immediate:**

Corollary 3.4.9. If ε is consistent with τ, then for any c ∈ C,

**The following is now straightforward:**

Corollary 3.4.10. gen τ is consistent with τ.

Proof. Assume c ∈ C and e ∈ (gen τ )(c).

By Theorem 3.4.8, there is a class function ε : C → Pow Seq(L × C) such that ε is consistent with τ, and e ∈ ε(c).

If τ (c) = ∅ and e =, then there is nothing to prove.

Otherwise, there is l, c, and e such that l, c ∈ τ (c), e ∈ ε(c ), and

And by Corollary 3.4.9, e ∈ (gen τ )(c ).

Thus, by generalization, gen τ is consistent with τ.

Corollary 3.4.9 is the proof rule that we referred to earlier, which is basically an instance of the coinduction proof technique described in [42]. This deserves a brief digression.

We write Gτ (ε) for a class function from C to Pow Seq(L × C) such that for any c ∈ C,

the inclusion class relation on Pow Seq(L × C): for every class function ε1, ε2 : C → Pow Seq(L × C), if for any c ∈ C, ε1 (c) ⊆ ε2 (c), then for any c ∈ C, Gτ (ε1 )(c) ⊆ Gτ (ε2 )(c).

What is more, ε is consistent with τ if and only if ε is a post-ﬁxed point of Gτ, or equivalently, for any c ∈ C, ε(c) ⊆ Gτ (ε)(c).