THE UNIVERSITY OF MICHIGAN COMPUTING RESEARCH LABORATORY APPLICATIONS OF TOPOLOGY TO SEMANTICS OF COMMUNICATING PROCESSES Wlllam C. Rounds CRL-TR-32-84 July 1984 Room 1079, East Engineering Building Ann Arbor, Michigan 48109 USA Tel: (313) 753-8000

APPLICATIONS OF TOPOLOGY TO SEMANTICS OF COMMUNICATING PROCESSES William C. Rounds * Computer Science and Engineering Division University of Michigan Ann Arbor, Michigan 48109 1. Introduction In this paper we point out some general principles which underlie proofs of correctness for communicating processes. We are concerned with those properties of processes which can be defined with reference to the possible finite behaviors of a process. These include safety properties: those assertions which say that nothing undesirable will ever happen. Hoare, Brookes, and Roscoe, in their paper on CSP [HBR], define buffers by means of a collection of safety assertions about buffer behavior. They state some general theorems about properties of processes which can be established using a rule of proof called fized-point induction. We generalize these results to a more refined semantic model than theirs. In doing so, we are led to an interesting application of the compactness theorem from first-order logic. This result can be interpreted as saying that the so-called Stone topology on a class of mathematical structures is compact. This topology is induced by defining the closed sets to be classes of structures which satisfy every assertion in a given (consistent) collection of assertions. Our structures represent the possible behaviors of a process, and we show that the definition of buffers can be rephrased as a consistent collection of assertions. Therefore the class of buffers is closed. We also prove that the Stone topology is definable by a metric given naturally in terms of Miner's observational equivalence relations. Convergence in the metric is guaranteed by the hypothesis of the rule of fixed-point induction; in fact, this rule is seen to be nothing more or less than the Banach fixed-point theorem for the space in question. We view this work as a synthesis of the methods of Hoare, Brookes, and Roscoe with those of de Bakker and Zucker [BaZ], and also those of Milner [M]. Our examples confirm the validity of the idea of specification semantics in [OH]. Moreover, the suggestions of Smyth [S] are confirmed because the general notions of topology serve as a guide to formulating theorems about all these models. The paper is organized into four sections, of which this is the first. Section 2 introduces the basic model of processes-the transition system- and presents the logical system used to describe these models. Section 3 is devoted to buffers and CSP. The final section gives another application of the compactness theorem which solves a problem left open, in [Rou] concerning transition systems over a countable alphabet. 2. The operational model The underlying framework for expressing the behavior of processes will be the familiar transition system. This is a tuple S =(Q,q, I: ~EU{T}}) where Q is a countable set of states; q E Q is the initial state; S is an alphabet of event names; r is a special event, not in A, and denoting the silent transition. The relations --- are binary relations on Q which for each a event, denote the possible changes of state which may take place during that event. The elements of S are * Research supported by NSF grant BSR-8301022. 1

called visible events. Typically these might represent the instantaneous transmission of a value along a wire or channel. Generally we will compare and combine systems over the same alphabet. 2.1. Operators on transition systems. There are several familiar ways of combining transition systems to form new ones. We concentrate on those needed in our examples. 2.1.1. Prefixing. Let A C E, and let S, be a transition system for o E A. then:A -' Sa is the system with a new initial state go, and a transition on a from this state to the initial state of Sa for each C7 E A. (It is presumed that the state sets in question are disjoint.) The event a is bound in this construction. A simple special case occurs when A is the singleton {a}. This system is denoted a -+ S. 2.1.2. Synchronized parallel composition. Again, let A C S, and let S and T be transition systems over E. This time, the alphabet A is regarded as specifying a collection of events which must occur simultaneously in S and T. It is called the synchronization alphabet. Other events ( in E \ A) may occur independently in S or T. We define S I[a T to be the system (Qs x QT, (qs, qT), { }) where (q, r) - (q', r') iff either a E Ai, q -- q, and r - r or a A, and either q q with r =r' or r - r' with q = q Notice that if A is empty we get the "shuffle" of the two systems, while if A = E we get the direct product. 2.1.3. Hiding or concealment. Often we wish to ensure that an action a is not available to the environment of a process for synchronization purposes. This is accomplished by renaming the event a to be the silent event r. This operation will be denoted hidea, and is formally given by letting the -- relation be empty and adding those pairs to the - relation. 2.1.4. Renaming. This operation is used in our examples to direct information being sent on a particular channel to some other channel. It is specified by a renaming map r: E -- A. The result of applying this to a transition system is another system over the alphabet A which will allow a transition q --- q' iff there is some a with r(a) = b and q -a- q (the state set of the new system is unchanged.) 2.2. Logic for process description. We employ a modal logic L of Hennessy and Milner [HM] modified slightly for our present purposes. The formulas of L are defined to be the least set containing the Boolean constants tt and ff, closed under the usual Boolean operations, and under the rule stating that (a)+ and (A)+ are formulas whenever a E E and ( is a formula. Intuitively, the meaning of these modal formulas is that it is possible to execute a single a event and then be in a state satisfying 4; or that it is possible to execute a sequence of silent events and then to satisfy b. To explain the semantics precisely we need to define some auxiliary relations. Let the relation == be the reflexive, transitive closure of the - - relation. Let the relations =, for a E E, be 2

(For u E E* we also have the natural relations ==.) We next define the satisfaction predicate =. Let S be a system and q E Qs. The predicate H is the least relation between Qs and L satisfying: q = tt always; q = ff never; q Hd v biff q = 0 or q = b; (Similarly for the other Boolean operations) q (a)+ iff (3q')(q = q' A q' H ); q = (A)> similarly. Definition 2.2.1 (modal rank.) Let tt = ff i= 0; |1 V |I= 1| A t] = maz(|l, lip |); Is-I 11='I; l(a)I|= 1(A)|= 1+ 141. Definition 2.2.2. Let L(n, A) be the set of all X with 11t < n and modalities (a) with a E A. Two states q and r are nelementarily equivalent iff Th,(q)= Th,(r), where Th,(q)= { E L(n, E): q t= } Let E, be the relation just defined. Let q E r iff q E, r for all n. Similarly let E~ and E' be these relations induced by formulas with modalities restricted to A. Example. Consider the two systems where the initial state is at the root of the tree. These systems are E1 but not E2-equivalent. We also have another useful and closely related definition of equivalence. Definition 2.2.4. Two states p and q are 0-behaviorally equivalent trivially. They are (n + )-behaviorally equivalent iff for all a E E U {r}, and for all p' such that p == p', we have (3q')(q ~ q' A q' is n-behaviorally equivalent to p') and vice versa. Let B, denote the relation of n-behavioral equivalence, and let B be the intersection of all the B,. Lemma 2.2.5. If A is finite, then among the formulas of L(n, A), there are only finitely many logically distinct ones. Proof. This is found in [GR]; one merely has to put the formulas of L(n, A) into a normal form. Lemma 2.2.6. (Master formula theorem for L.) For each finite A, and each stat q, there is a "master formula" M4(n, A, q) such that (i) q H= Md(n, A, q), and (ii) for all r, if r = M4(n, A, q) then r EA q. Proof. Let 01,..., k be the logically distinct representatives of the set of (n, A)-formulas satisfied by q. Then we may take k M A(n,gq)=- A,. = —1 3

Theorem 2.2.7. If E is finite, then B,- = En for all n. Proof. It is easy to show that B, equivalence implies E, equivalence. The other direction is by induction on n. This is trivial for n = 0. Assume it for n, and let p En+1 q. We want to show p Bn+1 q. Let p =a4 p' and let 0 = M4(n, A, p'). Then p = (a)=. So therefore does q, and Lemma 2.2.6 and the induction hypothesis complete the proof. Theorem 2.2.8. If E is finite, then the E, relations are congruences with respect to the operations in Section 2.1, except hiding. Proof. The result is straightforward to show if we use Bn instead of E,, by induction on n. Applying 2.2.7 then gives the desired conclusion. The relationship between En and Bn is more interesting when E is infinite; in this case the relations do not agree. However, we can characterize the distinction as follows. Definition 2.2.9. For A C E, let RUN(A) be the transition system with one state q, and a transition q a== q for each a E A. Let p be a state in an arbitrary.transition system over E. We define P 11 A = P Ie RUN(A). This operator disallows any transitions of p which are not in the set A. (By the transition system p we understand the transition system in which p occurs, redefined to have p as its initial state.) Lemma 2.2.10. For any finite A, and any n > 0, we have for all states p and q, p E. q (p I| A) Bn (q 1 A). Proof. (=.) We proceed by induction on n to show that p E~ q implies (p II A) Bn(q j1 A) for all p and q. The case n = 0 is trivial. Assume the result for n. Let (p 11 A) a (q 11 A). The proof is the same whether or not a is visible. We know from Def. 2.2.9 that a, if visible, is in A, and that there is some p' such that p == p'. Therefore p h (cr)M(n, A,p'). Since p E^+j q, there is a state q' such that q =e q' and q' 1= M4'(n, A, p'). By Lemma 2.2.6, q' EA p'. By induction hypothesis, (p' 11 A) Bn (q' 11 A). Since (q 11 A) = (q' 1t A), we have the result for the case n + 1. (<.) The converse is another induction on n. We show: for all p and q, (p II A) Bn (q I A) implies p E. q. Again the basis is trivial. For the inductive step, assume that (p II A) Bn+1 (q 11 A). The conclusion requires p E~+1 q. This is established by another induction over L(A, n + 1) formulas. For each X in L(A, n + 1) we must establish P qd < > q =. This is clear when < is tt or ff. If 0 is a Boolean combination of smaller formulas, the result follows easily from the induction hypothesis for those formulas. Suppose, therefore, that < is (a)o. Let p l= >. Then there is a p' such that p = p' and p' H= b. If a is visible then of course a E A, and therefore (p II A) == I (p' II A). This gives a q' such that (q 11 A) ==* (q' II A), and (p' I1 A) Bn (q' II A). The overall induction hypothesis applies, showing that p' E~ q'. Thus q' H= b, and so q = (a)tb. The reverse implication is the same, so that we have proved the whole lemma. Theorem 2.2.11. For any states p and q in a transition system over E, p En q if for every finite A C E, we have (p 11 A) Bn (q 11 A). The same holds for B and E. Proof. This is immediate from Lemma 2.2.10. Theorem 2.2.12. The conclusions of Theorem 2.2.8 hold without the hypothesis of finite E. Proof. We show that En is a congruence for synchronized parallel composition, leaving the other operators as an exercise. Let r be the synchronization alphabet. Suppose p En q. We want: for all r, (p flr r) En (q |ir r). 4

Let A be a finite subalphabet of S. Then (p 11 A) B, (q 11 A). These systems can be regarded over the finite alphabet A, and so by 2.2.8, we have (p A) lr r Bn (q ll A) llr r for any r. It is easy to see that (P llA) )irr Bn (p lIr r) II A, so we have the desired conclusion for all finite A. Applying 2.2.11 gives the result. 2.3. The metric space of transition systems. Using the equivalences in 2.2 we can define the distance between two states in a transition system, and therefore also the distance between two transition systems. Definition 2.3.1. Let p and q be states in a transition system. The E-distance dE(p, q) is inf{2-: p En q}. It is easy to check that dE makes T/E into a metric space, where T is the class of (countable) transition systems over some fixed countable alphabet, and T /E is the quotient by the E equivalence relation. The same remark holds for the relation B. We wish, however, to introduce yet another topological structure on transition systems. This is done by using the Stone topology associated with the logic L. The points of this space are the elementary equivalence classes p/E. We choose as a basis for the space the sets of the form Mod(O) = { p/E: p H= e} where 0 E L. This collection of sets is closed under the Boolean operations and so by itself forms a base for some topology. It will be convenient to consider the closed sets in this topology, which by definition are of the form Mod(r) = N Mod(@). er If E is finite, the Stone topology is the same as that given by the metric dE. Theorem 2.3.2. A subset K of T /E is closed iff it is metrically closed in the E-metric, provided E is finite. Proof. Suppose K = Mod(r) for some set of formulas F. Let p, E K and suppose d(p,, p) -- 0. (The relation E will be suppressed from now on.) If p, K, then for some 0 E F, p = — O. Choose n bigger than 1 1, and Pm so that d(p,, p) < 2-". Then Pm = 0 and pm = -8, a contradiction. Conversely, let K be a closed set in the metric sense. Define Th(K) = {: (Vs E K)(8s= 0)}. Claim: K = Mod(Th(K)). The inclusion of left in right is trivial. For the other inclusion, suppose t E Mod(Th(K)). We will construct a sequence s, E K such that d(sn, t) -- 0, which will prove t E K. Fix the value of n. Consider the formulas MO(n, E, a) as s ranges over K. By Lemma 2.2.5, there are only finitely many logically distinct such formulas. Set on= V MO(nE, 8). KEK Now s = On for each s E K, -hich implies pn E Th(K). Since t E Mod(Th(K)), we have t H= On. Thus for each n, there is an an E K with t = MA(n, E, s,). Therefore t En n,, which implies d(sn, t) -a 0, and the proof is complete. We can now state and apply the Compactness Theorem for L. Its use will be in the next sections, and principally in Section 4. 5

Theorem 2.3.3 (Compactness). Let r be a subset of L. If every finite subset F of r has a countable model (i.e. a p such that p E Mod(F)), then so does r.: Proof. This proof is given in [GR], where it is shown how to translate L into first-order logic. Only minor modifications to that proof are necessary to deal with silent transitions. Corollary 2.3.4. If E is finite, then the space T /E with the metric dE is a compact metric space. Proof. It is a standard fact from logic that the Compactness Theorem states that the Stone topology is compact. Since the Stone topology agrees with the E-topology, the result follows. Remark. The compactness theorem itself does not depend on the finiteness of E. This will be important in Section 4. 3. Applications to buffer specifications We present the definition of buffers appearing in Hoare, Brookes, and Roscoe. Their explanation goes roughly as follows. A buffer is a process which accepts messages on its input channel, and emits them in the same order on its output channel. The buffer should not have any other events allowed in its behavior. For the actual specification, we need to impose some structure on the set of events E. Let T be a set of values. For example, T might be the set of integers. Let C be a set of channel names (e.g., C = { in, out }.) A pair (c, t), to be written c.t, denotes the event of passing the message with value t along channel c. For buffer specifications, the channel names will be in the set { in, out }. We will also use a renaming operator which maps the event c.t to t. This operator is called restriction to c, and we write r(c.t, c) = t. If an event a is not in C x T, then r(a, c) = a. This operation is extended to strings of events in the usual way. One other concept is needed about transition systems: for a state q, we define Initials(q) {a E E: (3q')(q:= q')}. Now we can formalize buffers. Definition 3.1. A buffer is a transition system over E = in. T U out. T, with initial state b, such that for all s E E* and states q such that b == q, we have (i.) r(s,out) < r(s,in); (< is the prefix relation) (ii.) if r(s, out) = r(s, in) then Initials(q) = in. T; (iii.) if r(s, out) # r(s, in) then Initials(q) n out. T # 0. The first condition states that outputs appear in the order in which they came in, and that no output appears before it has been input. The second clause states that an empty buffer must be prepared to accept any input in the set T, and the third states that a nonempty buffer must be prepared to output some value in the set T. Note that the condition stating that every value which has come in must eventually come out is not explicitly expressed in this definition; it is possible to input values forever, provided that the buffer has unbounded capacity. We are going to prove that the class of buffers is a closed set in the Stone topology defined in Section 2. This will have the consequence that the rule of fixed-point induction works to establish properties of buffers. These conclusions appear in [HBR] and [Ros]; what is new here is the topology and the method of proof using logical specifications. Lemma 3.1.2. Let K be a closed set in the Stone topology, and let L C E*. Then the set K1 of (equivalence classes of) systems p such that for all s E L and all q such that p =-= q, we have q E K, is also closed. Proof. We know that K = Mod(F) for some set F of formulas. Let (s)0 be the formula (ol)... (an)+, where s = a... an, and let [s] be -5(s)}-. Then K1 = {[s]: E L and < E r}. 6

Corollary 3.1.3. The set K1 of processes p such that for all q, if p q, then s E L, where L C S*, is also closed. Proof. Let K = 0 and let L be replaced by the complement of L in Lemma 3.1.2. Lemma 3.1.4. The set K2 of processes q such that Initials(gq)= A, where A C E, is a closed set. Proof. Define r=={(a) tt: a E A} U {-(a) tt: a A}. It is clear that K2 = Mod(r). Lemma 3.1.5. If A is finite, then the set K = {q: Initials(q) n A - 0} is closed. Proof. Let r consist of the single formula (al) tt V... V (a,) tt, where A = {al,...,a,,}. Then K3 = Mod(F). Theorem 3.1.6. If T is finite, then the class of buffers over T is closed in the Stone topology. Proof. This is now immediate from Definition 3.1.1 and the foregoing lemmas. Remark. Lemma 3.1.5 is false for infinite A and the Stone topology. This is the only lemma that fails, however. We shall assume that the event set is finite for the remainder of the section. 3.2. Examples in CSP. Let c be a channel name. We define the operator hide, to be the renaming of each c.t event to the silent transition T, and otherwise the identity. Now let p and q be processes over the buffer alphabet. We define the chaining of p and q, written p > q, as follows. Let c be a new channel name. Let p(out -- c) be the process p except that all output events out.t have been renamed to c.t. Similarly, let q(in -- c) be the process where all input events in.t have been renamed to c.t. Then we define p > q = hidec( p(out - c) 11i q(in - c) ) where A = c. T. This has the effect of connecting the output of p directly to the input of q, and then hiding the communications on the new channel. It allows the interaction of p with the environment by means of the input channel, and of q with the environment by means of the output channel. One can prove, as do Hoare, Brookes, and Roscoe, that if p and q are buffers, then so is p ~ q. Now we want to consider the effect of recursive applications of the chaining operator. This will allow the definition of buffers with unbounded capacity. First, consider the one-place buffer B1, which inputs a value of type T, then outputs it, and repeats the process. It is easy to describe B1 as a transition system. In CSP, the process Bi would be expressed *(?z.T -.!z). As an example of a recursive definition, consider the equation p =?z. T -(p >> (!x - B1 )). Let F(p) be the function of p denoted by the right-hand side of this equation. In the notation of Section 2, F would be defined F(p)= a:in.T - S(p,a) where S(p, in.t) = p > (out.t - B1 ). Definition 3.2.1. A function F on transition systems is said to be constructive iff whenever p En q, it follows that F(p) E.+1 F(q). Lemma 3.2.2. The function F defined above is constructive. Furthermore, if p is a buffer, so is F(p). 7

Proof. Omitted here, but see [HBR] for some details. It should be noted that the chaining operator involves hiding, which is in general a nonconstructive operation. Special properties of the function F must be used in the proof. The significance of constructive functions lies in their metric space formulation. Definition 3.2.3. Let F be a map from a metric space to itself. F is said to be contractive iff there is a number a with 0 < a < 1 such that for all z and y, d(F(z), F(y)) a< d(z, y). Corollary 3.2.4. A function F is contractive in the E-metric iff it is constructive. Now we recall the well-known Banach fixed-point theorem. Theorem 3.2.5. Let F be a contractive mapping of a complete metric space to itself. Let B be a nonempty closed subset of the space. Suppose further that whenever b E B, we have F(b) E B. Then F has a unique fixed point which also belongs to B. Putting all the above results together, and remembering that the space T/E is compact, and therefore complete, we deduce that the function F defined above has a unique fixed point, up to E-equivalence, and this fixed point is also a buffer. Many other examples of recursive constructions of buffers can be found in [HBR], and they can all be treated in this way. 4. A cpo for processes over an infinite alphabet In [Rou] it is shown that the class of synchronization forests forms a complete partial order (in fact, a Scott domain) under reverse set inclusion. A synchronization forest is a collection of synchronization trees, and a synchronization tree is just a transition system whose graph is a tree. It is required in [Rou] that a synchronization forest be closed in the B-metric, and that a synchronization tree be over a finite alphabet with no silent transitions. Here we remove the latter two restrictions on synchronization trees, and we state our results for general transition systems. One of the technical contributions in [Roul was the construction of cpo-continuous functions from metrically continuous functions in the topology of synchronization trees. Specifically, it was shown that whenever F is a metrically continuous operation (unary, binary, etc.) on a compact metric space X, then the direct image map XK.F[K] is a cpo-continuous operation on the class of all nonempty closed subsets of X, ordered by reverse set inclusion. The topology used in [Rou] was the B-metric topology, which is compact if the alphabet is finite. This topology is not compact in the case of an infinite alphabet, and so the question arises about the existence of a suitable extension theorem for the direct image mapping in the infinite alphabet case. Our approach is to use the weaker Stone topology in order to retain the compactness property of the underlying space. Although this topology is metrizable, it is not necessary to use the metric! The topological definition of continuity (the inverse image of a closed set is closed) will suffice for our application, and in fact is extremely natural when used in conjunction with logical specifications. As an example, we will use the synchronized composition operator. In what follows, the space X will be T /E with the Stone topology. Let A C E and let F(p, q) = p I q. It follows from Theorem 2.2.12 that E is a congruence with respect to this operation, and so F is well-defined on the space X x X. Lemma 4.1. The function F is a continuous map from X x X to X. Proof. Recall that a basis for the topology of X is given by the collection of sets Mod(O), where 0 E L. Let B be the collection of finite unions of sets of the form Mod(0,) x Mod(0j) as 0, and Oj range over L. Then 8

B is a closed basis for the product space. It suffices to show that the inverse image of a basis set for X is a member of B. We define, for a formula b in L, the set K() = {(t, ): F(t, ) ). We are required to show that K(+) E B for all 4. This we do by induction on formulas. The result is clear for = tt, and if it holds for ) and b then it clearly holds for 4 V t. Consider the set K( —). By induction hypothesis, this is the complement of a set in B. Therefore this set can be written as a finite intersection of sets of the form Ui U Uj, where, = {(, u): t -i,} and = {(t, u): u -)}. By distributivity, the set can be rewritten as a finite union of sets of the form Ui n Uj. But Ui n Uj = Mod( —O) x Mod(-,Oj), and so K( —)) e B. Finally, consider the case ( = (a))b. Suppose that a E A. Then F(t, u) t (a)tp iff 3(t', u'): t = t', u = u', and F(t', u'). Let sK(b)= U Mod(O) x Mod(Oj) (iij)EG where G is a finite set of pairs. Then K((a)b) = U Mod((a)6i) x Mod((a)#j). (ij)E G Consider the case where a C A. Then F(t, u) = (a)+b iff one of two subcases occurs: 3(t', u'): t = t' and u =. u', and F(t, u') H ~, or the subcase with the roles of t and u reversed. Let K = U Mod((a)Oi) x Mod((A)O,) (s;j)EG to account for the first subcase, and K2= U Mod((A)Oi) xMod((a),j) (i,i)EG to account for the second. Then K()) = K1 U K2. This completes the proof of Lemma 4.1. We now state a general extension theorem. The proof is standard. Theorem 4.2. Let F be a continuous function from a compact Hausdorff space Z to a space Y. Define, for a closed subset K of Z. F[K]= {F(z): z K). Let Ki be a decreasing sequence of closed nonempty subsets of Z. Then the intersection of all the Ki is nonempty, and F[n Ki]=nF[. 9

This result gives us a way to construct continuous functions on the cpo of closed subsets of a compact space like X. For binary operations like parallel composition, we can simply define F(K1, K2)= F[K1 x K2] Since the space X x X is compact, the extension theorem applies with Z = X x X together with Lemma 4.1 to give cpo-continuous mappings. We have thus generalized the results of [Rou] to the infinite alphabet case. References [BaZ] J. W. de Bakker and J. F. Zucker, "Processes and the denotational semantics of concurrency," Proc. 14th ACM Symp. on Theory of Computing, 153-158. [GR] W. Golson and W. Rounds, "Connections between two theories of concurrency: metric spaces and synchronization trees," Tech. Rep. CRL-TR-3-83, Computing Research Laboratory, University of Michigan, 1983 (to appear in Inf. Control) [HM] M. Hennessy and R. Milner, "On observing Nondeterminism and Concurrency," Proc. 7th ICALP, LNCS 85 (1980). [HBR] C. A. R. Hoare, S. D. Brookes, amd W. Roscoe, "A mathematical model for communicating processes," Report PRG-16, Programming Research Group, Oxford (1981). Also to appear in JACM. iM] R. Milner, "A calculus of communicating systems," LNCS 92, (1980). IOH] E. Olderog and C. A. R. Hoare, "Specification-oriented semantics for communicating processes," Proc. 10th ICALP, LNCS 154 (1983), 561-572. [Ros] W. Roscoe, "A mathematical theory of communicating processes," D.Phil. thesis, Oxford (1982). [Rou] W. Rounds, "On the relationships between Scott domains, synchronization trees, and metric spaces," Tech. Rep. CRL-TR-25-83, Computing Research Laboratory, University of Michigan (1983). [S] M. Smyth, "Power domains and predicate transformers: a topological view," Proc. 10th ICALP, LNCS 154 (1983), 662-675. 10