THE UNIVERSITY OF MICHIGAN COMPUTING RESEARCH LABORATORY1 Connections Between Two Theories of Concurrency: Metric Spaces and Synchronization Trees W. G. Golson and W. C. Rounds CRL-TR-3-83 JANUARY 1983 Computing Research Laboratory Room 1079, East Engineering Building Ann Arbor, Michigan 48109 USA Tel: (313) 763-000 1All correspondence should be sent to Professor W.C. Rounds. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors and do not necessarily reflect the views of the funding agencies.

Connections Between Two Theories of Concurrency: Metric Spaces and Synchronization Trees October 1982 W.G. Golson W.C. Rounds Department of Computer and Communication Sciences University of Michigan Ann Arbor, Michigan 48109

f a -N I A

Abstract We establish a connection between the semantic theories of concurrency and communication in the works of de Bakker and Zucker, who develop a denotational semantics of concurrency using metric spaces instead of complete partial orders, and Milner, who develops an algebraic semantics of communication based upon observational equivalence between processes. We endow his rigid synchronization trees (RSTs) with a simple pseudometric distance induced by Milner's weak equivalence relation and show the quotient space to be complete. We establish an isometry between our space and the solution to a domain equation of de Bakker and Zucker, presenting the solution in a conceptually simpler framework. Under an additional assumption, we establish the equivalence of the weak equivalence relation over RSTs and the elementary equivalence relation induced by the sentences of a modal logic due to Hennessy and Milner.

- 1 - 0. Introduction In this paper we establish a fundamental connection between the semantic theories of concurrency and communication in the works of de Bakker and Zucker [BaZ] and Milner [Mil]. In [BaZ] de Bakker and Zucker develop a denotational semantics of concurrency using metric spaces (see for example [Niv] or [ArN]) instead of complete partial orders as the underlying mathematical structures. They solve several reflexive domain equations, and the solutions of two equations in particular, involving nondeterministic processes, entail the abstract completion of a metric space recursively constructed from metric spaces which utilize a Ilausdorff distance between closed sets. Milner develops an algebraic semantics of communication based upon behavioral or observational equivalence between processes. We take his rigid synchronization trees (RSTs), with countable branching and arc labels from an arbitrary alphabet, and endow them with a simple pseudometric distance induced by Milner's weak observational equivalence relation to construct a concrete representation of the solution to the first domain equation above. We prove that our quotient space is complete under the corresponding metric distance, and show that it is isometric to the de Bakker-Zucker completion by identifying an appropriate dense subset. As a result, one does not necessarily have to use the complicated notions of Hausdorff distance and the attendant machinery of metric space completions; one can work directly with trees as graphs and use a simple metric defined directly on the graph structure. The structure of our metric space has additional properties of interest. For example, unlike Milner we cannot restrict ourselves to finitely branching trees, since infinitely branching trees are necessary for the completion of the metric space. This need for unbounded branching arises quite naturally, a development which we are pleased to see. In another vein, while the construction

- 2 - in this paper allows the alphabet Z to be infinite, we can prove that our metric space is compact if and only if E is finite. In this case it turns out that the weak observational equivalence relation is exactly the elementary equivalence relation induced by the sentences of a simple modal logic due to IHennessy and lilner [Hell]. The statement that our space is compact is exactly the assertion of the Compactness Theorem for the Hennessy-Milner logic (HML). Since the HML compactness theorem follows from a direct translation into first order logic, this gives us an elegant but nonconstructive proof of completeness for the case when E is finite. On the other hand, since our proof of the metric space compactness is constructive, the HML compactness theorem is true without the axiom of choice. The rest of the paper is organized as follows. Section 1 is preliminary, defining the domain of trees and establishing some necessary properties. Section 2 presents the rigid synchronization trees of Milner and defines weak equivalence. The third section constructs the metric space and proves its completeness. The fourth section recalls the necessary definitions and results from [BaZ] and establishes the isometry between the metric spaces of this paper and [BaZ]. Finally section 5 establishes the connections between HML and our metric space.

- 3 - 1. Preliminaries We regard a tree as a directed, unordered graph on a countable set of nodes with arcs labeled from an alphabet E. The graph must have the obvious tree shape and two arcs leaving the same node may have the same label. More formally we define the set of trees, T, as follows: Definition: S is a tree (SET) iff S is a 4-tuple S=(V,E,Z,vO) where V is a set of vertices or nodes; Vo V is the root; E!CVxV is the edge relation, antisymetric and irreflexive;:'E-+Z assigns a label to each edge. In addition the following properties are satisfied: (1) all nodes are reachable from the root: VvcV-{v0} <vo,v>eE+ where E+ is the transitive closure of E; (2) each node has only one ancestor: Vu,v,wEV, <u,w>cE and <v,w>cE implies u=v. We say two trees are isomorphic if both can be transformed into the other preserving structure and labeling: Definition: S=(V,E,Z,v ) and S'=(V',E',z',vo') are isomorphic iff there is a bijection f:V-V' such that (1) f(vO)=V0 (identification of roots); (2) <v,w>EE <=> <f(v),f(w)>eE' (identification of edges); (3) V<v,w>~E, l(<v,w>)=Z'(<f(v),f(w)>) (identified edges have same label). For example, <. and v' are isomorphic under the correspondence 6. V0V1, v1-*v, v2v11, v3v2. When S and S' are isomorphic, we shall write S=S'.

- 4 - The notions of path, path length, and finite and infinite paths are the usual ones. We say a tree is bounded if there is a finite bound on all path lengths. A node is finitely branching if it has a finite number of direct descendants. A tree is finitely branching if all its nodes are. We allow countable branching at any node. The kth cross section S(k) of a tree S is just S restricted so that no path has a length exceeding k: Definition: For SET, let the kt cross section of S=(V,E,L,v0) be: ~ ~ 0 S(0) =({vO},0,0,v), k=O; S(k)=(Vk, Ekk,v) k>l; where Ek={<v,w>cElthe path <vo,w> has length at most k}; k 0' Vk=VI Ek; Examples: 1) S ) is just the root, which we call nil. 2) If s then S ()=nil, S(1)= S (2) for k>3 We have the following relationship between a tree and its cross sections: (k) Lemma 1.1: For any ScT, let {S(k)} be the set of all its cross sections, k>O. Then (a) Vk>O Ek E+ and E=UEk (b) Vk>O Vk Vk and V=UV (c) Vk>0 t ek+l and t=UZk(viewing Zk as a set of ordered pairs <eka> from Ek and E) Jk k Proof: We prove (a). EkCEkl directly from the definition, Now clearly EkE for all k so UEvkE.

- 5 - Let <v,w>cE. Then there is a path <v0,w> and therefore <v,w>eEk for any k not less than the path length of <v0,w>. Therefore <v,w>CUEk, whereby EsUEk. This lemma suggests that any tree can be represented as a union of its cross sections, leading to the following definitions: Definition: Let {Sk} T. {Sk} is a cross sectional sequence (written <Sk> a XSS) iff (1) each Sk is bounded, say with maximum path length of b(k); (2) Vm>k S b(k)=Sb(k) (writing Sb(k) for S ) m K The last condition insures that the b(k)-th cross sections of Sk,Sk... are all equal, i.e. only the leaves of Sk with path length b(k) can be extended to form k Sk+l For convenience, in any sequence <Sk>, we shall take SO to be the nil tree and b(0)=0. Definition: Let <S > be a XSS. The union tree of <Sk> is k k USk= (UVk, UEk, Ukv)' We collect some facts about XSS which will be useful later: Lemma 1.2: Let <Sk> be a XSS. (a) k<n implies b(k)<b(n) (b) Sk=Sk (c) Vm>k Vj<b(k) S (j)=Sk( m m (d) USk is a tree and (USk)b(k)=Sk Proof: omitted. We wish to define two additional operators on trees, prefixing and joining, enabling us to create complex trees from simpler ones. Notation: S[v/w] means the treeS with the node w replaced by v.

2finition: For S=(V,E,Z,v0) and azZ let aS={VU{va },EU{<va,v0>},J{<< Va, >,a>},va where v iV. a ictorially we have. We call aS a prefixed (sub)tree. Dfinition: We say (Sk} are disjoint if {Vk} are pairwise disjoint. sfinition: Let {Sk}CT, Sk=(VkEkek'O, k), Sk} disjoint. The join of {Sk} is Sk = Uk[vo/vok] o SO T becomes the tree. We view the expression S( S to be well efined, representing the joining of two disjoint isomorphic copies of S. We epresent by Sn the joining of n copies of S for l<n<w. In a similar spirit, (OT will always be taken to be well defined through an inessential relabeling of odes if necessary. emma 1.3: aS and ) Sk are trees. roof: clear. Finally we establish another representation of an arbitrary tree:,emma 1..5: For SET, there is a set {a.S.}CT such that S= a.S. roof: Clearly we can represent S as the join of its prefixed subtrees.

- 7 - 2. Rigid Synchronization Trees and Weak Equivalence In the spirit of [Mil] we regard a rigid synchronization tree (RST) as the "unfolding" of a state transition graph of a nondeterministic machine. For example, given the graph ~-~ Q~ we associate the RST: Note that that state names are no longer important; the tree nodes are nameless. The arc labels are chosen from an event alphabet E, reflecting the communication requirements of the process from its environment. We depart from [Mil] and allow the nodes to have countable branching. \q Nondeterministic choice exists in the tree b. Given an "a", the machine must choose between two paths, arriving at either a state where only a "b" is acceptable or one in which only a "c" is. Now consider the tree 8/k If viewed as acceptors, both of these trees are equivalent, accepting the language {ab,ac}. But are they equivalent behaviorally? After one step the second tree is in a state where either a "b" or "c" is acceptable, and so it never deadlocks on input from {ab,ac}. However, the first tree can deadlock on either "ab". or "ac": after "a" has been consumed, it will be in a state waiting for a specific event and will fail if the environment offers an incompatible input. Note that nondeterministic trees do not necessarily "choose correctly"; they react only to the current event, not to future ones. Since the trees behave differently on inputs from {ab,ac}, it is reasonable to maintain that they are not equivalent behaviorally. Several different equivalence relations have been proposed to describe behavioral or observational equivalence [Mil]. The relation appropriate for this paper is the weak equivalence relation and is defined as follows. a Notation: When we write S >T we mean there is some a-transition from the root of S leading to T, or that aT is a prefixed subtree of S.

- 8 - Definition: For S,TET, S is weakly equivalent to T, S - T, iff w V S-k T, where the equivalences are defined as: k a d S 0 T for all S,T; ~a-o kS -,,T <==> VacEVS T SS' S S ==>3T'T T- >T' and S' T' and k+l T, k Va~eVT'cT, T a >T' ==>3S'~T S >S' and T' E S. We write S T for S = T. w An alternate way of presenting k+l-equivalence which we shall find convenient is the following: Sk+lT <=> for every prefixed subtree aS' of S, there is a prefixed subtree aT' of T such that S' kT' (and vice versa). Examples: (1) 5 since they are 2. To see this note that nodes are 1 if the set of events which can occur next are the same. The tree is - to either b or c. 1 L (2) Let Ak be the tree. k times. Let A,= (Ak, k>l. So A* has arbitrarily long finite paths and an infinitely branching root: a Let A be the infinite tree | and let A = A, A. Note that for all W co k, A(k) = A,(k) as each k-th cross section contains one path each of lengths l,...,k-l and a countable number of paths of length k. We claim that A-k A* for all k and thus A - A,, as can be seen from the following lemma: Lemma 2.1: If S(k)=T(k) then S- T. Proof: Induction on k. For k=0 the result is immediate. Assume the lemma holds for k.

- 9 Suppose now S (+)=T l). As the prefixed subtrees of S and T are in 1-1 correspondence, we can write S(kl) aiS ()= aT )=T( ) where Si )=T. () Therefore by the induction hypothesis we have S T.. Clearly now we have i -k 1 S T. k+l but not equ We remark that the converse is false:' but not equal. Finally we collect some easy and useful facts: Lemma 2.2: (1) S k T implies Vj<k S. T (2) S k T implies Vj>k S 1. T (3) S S(k) S(n) n>k k -k — Proof: omitted.

-103. The Metric Space of RSTs In this section the completeness of the metric space on T induced by the weak equivalence relation is demonstrated. For topological definitions and related items, the reader is refered to [Dug]. We define the following metric on T: -k Definition: For STT, let d (S,T) = 2 where k = max S. T. If the maximum w J J does not exist, we take k to be infinite. As k-equivalence examines no nodes which are along paths of length greater than k from the root, we see that the larger the value of k above, the more alike the two trees are, the smaller the value of d. w Examples: d (AT,ia)=l since Si T aAa d w( I,.a)=1 since SE1T but S72T d (c AX\, La)=dw(A,,A )=0 Lemma 3.1: <T,dw> is a ultra pseudo metric space. Proof: (1) dw(S,T)=O <==>Vk S=kT <==> S-T (pseudo) (2) dw(S,T)=dw(T,S) (3) d (S,T)<max(dw(S,U),dw(U,T)) (ultra) -k -k Let dw(S,T)=2 and suppose (wlog) dw(S,U)<2. Then Sk+lU. Since both S -U and S T, we have U -T. However, U kT as S kT. k k k k+l k+1 -k Therefore dw(U,T)=2. We define the notions of Cauchy sequence and limit: Definition: <S > is a Cauchy sequence (CS) iff n Vk>0 3NVm,n>N, S = S m -k n

- 11 - Definition: S is a limit of a CS <S > (written Sc 1 im S ) n n iff Vk>O 3NVn>N, S k S - k n Remarks: (1) The above definitions are equivalent to the more usual presentations, e.g., Vc >03NVm,n>N, dw(Sm,S )<c. (2) We must deal with equivalence classes of CS limits. Recall that <T,d > is a pseudometric space, and for example, if S =j. Aj, w nn jl j' a.T^ e.g., S3= ~ q1 l, we have that <S > is a CS and sofor all n A 1 A, - S AoA and therefore {A*,A }l.im S. n n n c* n Proceeding to the completeness proof, we will establish that any XSS <S > n in <T,d > is a CS with awell defined constructible limit, the union tree, w US clim SL. An operator on trees, C, yielding a fully expanded countably branching tree in a sense made precise below, will be defined and shown to possess the following special properties: (1) weak equivalence is the same is isomorphism, i.e. C(S) = C(T) <==> C(S) - C(T), for bounded S,T; (2) for any bounded S, S - C(S). By standard argument, given a CS <S >, we can select a subsequence <S' >'n n n such that <S' (n)> has the same limit as <S >, if indeed such a limit exists. n n Now since <C(S' (n)> is a XSS (implied by (1)) and therefore has a limit n which by (2) is the same as <S >, the completeness of <T,d > will follow directly. n w Lemma 3.2: If <S > is a XSS, then it is also a CS in <T,d >. n w Proof: Recall <S > a CS <==> Vk>03NVm,n>N, S S n - m k n We have two cases: (a) <S > is bounded (i.e. {b(n)} is bounded). Then after some NO, Vm,nN, S =S. Then for any k,S )=S ) and so S S (Lemma 2.1). 0 m n m n mkn

- 12 - (b) <S > is not bounded. Choose N such that b(N)>k. Then as S=Sb(N) n k) N (Lemma 1.2.b) we have Vm,n>N S (k)=S (k) (Lemma 1.2.c) and therefore m n S ES (Lemma 2.1). m k n Theorem 3.3: Let <S > be a XSS. Then,lim S, exists and US ~,lim Sn n' n n Proof: US exists by Lemma 1.2.d. The reader may now proceed in a fashion similar to the proof of Lemma 3.2. Our C operator is defined as Definition: For any bounded tree S, let C(S) be: C(nil)=nil C( O aiSi) =[ aiC(Si) ] To aid the intuition, C(S) can be constructed for any bounded tree S as follows: (1) mark all leaf nodes as ready; (2) repeat until the root is marked ready if all of a node's descendants are ready then replace each prefixed subtree of the node by X copies of the subtree and mark the node ready; For example, if S =, then C(S) where = Lemma 3.4: For S bounded, C(S) is a tree. Proof: omitted. The utility of C-trees becomes evident in the theorem and corollary below, in which weak equivalence is seen to be the same as isomorphism.

- 13 - Theorem 3.5: Let C=C(S) and D=C(T) for some bounded S,T. Then C-kD<==>C )=Dk) Proof: (<==) Lemma 2.1. (==>) Induction on k: case k=O: immediate. Assume for k. case k+l: Suppose CEk+ D. Partition the prefixed subtrees of both C and D into k+1-equivalence classes. As C k+l-equivalence classes. As C-k+lD, these equivalence classes of C and D are in 1-1 correspondence. By the induction hypothesis, the representatives of corresponding classes have isomorphic k+l cross sections, so the two trees obtained by the joining of the representatives are k+l-isomorphic. As C and D are C-trees, each equivalence class represents at most w prefixed subtrees. Now as every prefixed subtree of C or D contributes w copies of itself to C or D, the number of subtrees represented by any class is w. Therefore we have C(k+l) =D(k+l) Corollary: C-D <=> C=D for bounded C,D. Proof: As C,D bounded, the isomorphisms constructed above will stabilize. The last result we need prior to priving completeness is the following: Lemma 3.6: For S bounded, SEC(S). Proof: We show Vk S-k C(S) by induction on k. case k=O: immediate. Assume for k. case k+l: Let S= Q aiSi, C(S)=[ aiC(Si)]W Now SE C(S) <=> VaVS' S —>S' implies C' C(S) ->C' and S' C' and vice versa.

- 14 - If a.S. is a prefixed subtree of S, then aiC(Si) is a prefixed subtree of C(S). We have Si-kC(Si) by the induction hypothesis and so the required C' exists. A similar argument for the reverse direction establishes the lemma. We are now ready to prove Theorem 3.7: <T, d > is complete. Proof: Let <S > be any arbitrary CS in <T,d >, ln w i.e. Vk>O 3N Vm,n>N S - S m-k n' By passing to a subsequence if necessary, we can assume Vn:>k Sk S Consider k k n now the sequence <S(k)>. Clearly < (k)> is a CS as Sk)S >k. k eary k k n n Since S(k) is bounded, Sk)C(S(k)) by Lemma 3.6. Therefore <Sk(k)> has a limit iff <C(Sk(k))> does. But <C(Sk(k))> is a XSS (by Theorem 3.5) and has a limit (Theorem 3.3). Finally we observe that by construction <Sk> has the same limit as <Sk)>, k k completing the proof of the theorem. At this point we would like to remark that our construction not only incorporates countably branching trees, but requires them for our space to be complete. That arbitrary finite branching is not enough can be seen from the following. Recall that ^1 A. is the tree j times. Now suppose that S= A.. for j<k. Then both the minimum and ~i) iitme.No upsetatSk 3 maximum path lengths in S have size j, so that all the paths in S have length j. Now suppose S-k+1 A,, where we now write A*,= aA. for j a natural number. Then for all j<k there is a prefixed subtree aS. of S such that A kS.. Therefore, for each j<k, S. has path lengths of exactly j and Sk has path lengths of at least k. So we have established that Lemma 3.8: If S- A, then S has at least a k-way branching root. k+l I

- 15 - Theorem 3.9: <T,d > is incomplete if trees cannot have countable branching. w Proof: <A1,A1 A2,...> is a finitely branching CS with limit A,, which by the lemma is not equivalent to any finitely branching tree.

- 164. An Isometry with a Metric Space of de Bakker and Zucker En route to their denotational semantics of concurrency, de Bakker and Zucker [BaZ] wish to find a metric space <P,d > which solves B P={pO}UP (Z x P) (4.1) where P refers to the set of all subsets closed with respect to dB. Their solution turns out to be isometric to a quotient space of <T,d >. In this w section we shall describe their solution <P,dB> and establish the isometry. Definition: Let <P,d > be a series of metric spaces defined by n n = {p}, PO is the nil process, Pn+l = {pO}UP(E x Pn P is the power set operator, and dO(p,q) = 0 for all p,qEPo, 0 for p=q=PO d (p,q) = 1 for p=pO or q=P O, but not both max(supinf d+(pq'), sup inf d' (p' q)) P'ep ql'q nq'q' n+ for both p,qCZ x P n where 0 for p'=q'=p 1 for p'=pO or q'=po, but not both dn+1 ) d (p",q")/2 for p'=<a,p">, q'=<b,q"> and a=b 1 above, except afb. Note that d is the Hausdorff metric distance between the subsets of Pn n+l n+l induced by the metric d' on the points of Pn+l. n+l n+l Definition: Let <P,dB> be the completion of <UP,US >. Theorem 1 [BaZ]: <'B satisfies (4.1).

- 17 - The quotient space through which the isometry will be established is the space of reduced trees. We need a preliminary definition: Definition: For S bounded let US be: 0 (nil)=nil ( ai.Si)= )a!S! where {a!S!) is the maximal collection of pairwise 0(0 ais i)si i 1 "-i ii nonisomorphic prefixed subtrees of S. We shall write for convenience Qa.S. for L( a.S.). Examples: (1) S = /, US = la (2) S=, rS= f (3) S= k, = S Lemma 4.2: US is a tree. Proof: We must verify that US is well defined. If {a!S!} and {at'St'} are two ~'___ -LI 11 11 maximal collections of nonisomorphic prefixed trees of S, then the sets must necessarily be in 1-1 correspondence and so O a!S! = Oa'S'. 1 1 1 1 Definition: (reduction operator) For S bounded let R(S) be: R(nil) = nil R( OaiSi) = aiR(Si). Example: For S =, R(S) = (see example 3 above). I c/ b For convenience, let R ={R(S) I S bounded by n}. Lemma 4.3: (1) R(S) is a tree; (2) R is the set of all reduced trees of height S. n ni

- 18 - Proof: omitted. We shall now establish an isometric bijection between <UR,d > and<UPn,Udn>. Definition: Let (:UR -UP by 4(R(nil))=P(nil)=po n n (R(S))= (laiRa(Si) )={<ai,(R(Si))>} Theorem 4.3: |IR is a bijection between R and P n n n Proof: Induction on n: case n=O: immediate. Assume for n. case n+l: 4 is 1-1: Let R(S), R(T) eR1 and suppose 4(R(S))=P(R(T)) Now if U(R(S))=((R(T))=p0, then by the induction hypothesis, R(T)=R(S)=nil Suppose R(S)= aiR(Si) and R(T)= bjR(Tj) where R(Si), R(Tj)~R {<a i,(R(Si))>}={<bj,.(R (Tj))>} V.j3 <ai,(RK(Si))>= <bj,((R(Tj))> and vice versa ai=b. and ~(R(Si))=4(R(T)) R(Si)=R(Tj) by the induction hypothesis aiR(Si)=bjR(Tj) 1..~ is I O aiR(Si)=bjR(T). is 1-1 is onto: Let pcP If p=po, choose -l(p)=nil. Else p={<ai pi> PiE - By the induction hypothesis 4 is onto P. Denote by d (pi) the unique (4 is 1-1) element of R such that 4(-l(pi))=pi. Let - l(p)=D ai.l(pi ) Because -l (pi)zR we have a.-l(p.i)eR and therefore 4 l(p)eR Furthermore (+ 1 (p))={<a.,p>=p p is onto.

- 19 - Corollary: Q is a bijection between UR and UP n n The following will be useful in establishing the isometry: Lemma 4.4: For S,T UR, SET <=> S=T, i.e. <UR,d > is a metric (not pseudometric) space. Proof: (<=) immediate. (=>) standard induction argument on Ek Theorem 4.5: c is an isometry between UR and UP n n Proof: We shall establish that VS,TeRn, dw(S,T)=dn( (S),4(T)) from which the conclusion follows. Induction on n: case n=O: d (S,T)=0 since S=T=nil w and do ((S),(T))=d0(pO,p)=0' Assume for n. case n+l: we shall establish VS,TERn+ d (S,T)=2k <==> dn+l(S),(T))=2 Induction on k: case k=O: d (S,T)=0 <==> S=T (Lemma 4.4) <==> (S)=~(T) <==> d n+l((S). (T))=0 n+l Assume for k. case k+l: We know d (S,T)=2(k+l) <=> Sk T and S kT. We claim that w k+l k+2 S +iT <=> dn+ (~(S),k(T))<2(k+l) If the claim is established, then lv~i t n+i the induction and theorem follow as <=> d (k2(S) (T))=2-(k+l n+) ( The first inequality above arises from the claim and the fact that S k+2T. It remains to establish the claim. k+2

- 20 - Claim: Sk T <=> d (~(S) (T))<2k+l n+l Proof: (=>) S-k T <=> VaVS' S ->S' => T' T- >T' and S'E T' and vice versa k+l k -k d (. (S'),P(T'))<2 by the induction hypothesis for n and k * d'n ((aS')(aT))<2-(k+l) n+l n+l jj Since S T, Vi inf d' ((a.S.), (a.T.a<2(+ k+l ((aiS) (ajT n))2(+l) 1' n+ l i'-(k+l). sp inf d' ( (ai.S), (ajT ))<2 +l) 1 ~j n+l i i'' j -- A similar argument establishes sup inf d' n )<( ) J, n+l' - -(k+l). dn (t(S),P(T))<2 ~n+l'(<=) Suppose now dn+l(S),(T))<2(k+l) Then sup inf d' ((a Si), (biT ))<2(k+l) j n+l i jj.Vi3j d' (P(aiSi),(bj.T ))<2(k+l) Vi- ~' n+l i ij.Vi3j a.=b and d (p(Si),(T.))<2 By applying the induction hypothesis for the claim for each prefixed suhtree aS. there is a corresponding aT. such that S kTj 1 j 1ik one half of the definition of k+l-equivalence is satisfied. We obtain the other half from sup inf d' (, -)<2 ( 1 n+l' - This completes the proof of the claim and the theorem. Since URn T, the completion <P,dB> of <UP,Ud > is isometric to a complete subspace of <T,d > (modulo E), say <R,d >. We need to demonstrate that UR w w n is dense in T, i.e. that [R/-]=[T/-], so that <P,d > will be isometric to <T,d >/-. B W We need a preliminary lemma. Lemma 4.6: For S bounded, S-R(S).

- 21 - Proof: Induction on k: case k=O: immediate. Assume for k. case k+l: Let S=()a.S., R(S)=ta.R(S.) Suppose aiSiis a prefixed subtree of S. Then aiR(Si) is a prefixed subtree of R(S) (or there is some a.R' branch of R(S) such that R'=R(Si)). Then by the induction hypothesis, R(Si)kSi and we are done in one direction. The reverse direction is similar. Theorem 4.7: For any SET, there is some TeR such that SET. Proof: Recall that S=US n) Since S(n) bounded, S(n)R(S(n)) by Lemma 4.6.' <RS(n))> is a CS in <R,d > and therefore has a limit TER. Clearly TES. ~~@^ w

- 22 - 5. A Connecton with Programming Logic. In this section we treat the case when our RST's are labeled from a finite set Z. We introduce the small modal logic HML (Hennessy-Milner logic). It turns out that for any trees S,T, that SET iff for every 4IHML, S t= <=> T 4). We exploit this fact to show that completeness of the space <T,d > is a consequence of the Compactness Theorem for HML. This theorem in turn follows from the Compactness Theorem for first-order logic, so we have an alternative proof of completeness in this case. Finally, we observe that if our metric space is compact, then the HML Compactness Theorem follows as a consequence. These results are in a sense already known in model theory. The relation E can be defined on arbitrary first order structures, and the equivalence AEB iff for all sentences ), A = 4 <=> 3B g is part of the Ehrenfeucht-Fraisse' characterization of elementary equivalence [Mon, p. 408]. HML can be considered as a fragment of first-order logic and the general theory applied. However, the proofs in the HML case are simple and revealing, so we think it worth while to present them here. Definition: The set of formulas HML is given by the following inductive clauses: tt, ffc HML (two Boolean constants) ),i ~HML imply ^ 4 ) HML and - 4 HML (Boolean operations) 4 E HML and acZ imply a<4>cHML ("possible" modality) The formula a<4> is to be read: "From the initial state (root) it is possible to execute the atomic action a and arrive in a state satisfying ". Note: Z is henceforth finite.

- 23 - Definition (semantics of HIML): Let S be an RST over Z, and let {cHML. We say S satisfies { (S F {) in case we can apply the following inductive clauses: S f tt always; S = ff never; S \ (^A iff S t d and S l q; S - i iff not (S = ); S a a<{> iff (3S')(S->S' and S' V (). We proceed to develop some facts about HML and the relation =. Definition: The depth 1I1 of an HML formula is given by: Ittl =Iffl = O; I (A1 = max (I 1,{ I1); 1 = ml; Ia<> = 1 + 11H. Let tML = { <1 Iln}. Lemma 5.1: For all T,U, and n, if TE U then for all (EHML (T t= <=> U N )). n n Proof: easy induction on n. The converse of 5.1 requires a little work, and is false unless Z is finite. Definition: Two HML formulas -,i are logically equivalent iff for all T, T = iff T l= 4. Lemma 5.2: For each n, the relation of logical equivalence restricted to HML has only finitely many equivalence classes. Proof: Use induction on n; the proof amounts to finding a DNF for the formulas in HM4L. Here the finiteness of Z must be used. n

- 24 - Lemma 5.3: For any n, and any T,U, if for all (eHMLn, T 1 $ <=> U = $, then T- U. n Proof: Again, by induction on n. The result is clear when n=O. Assume it for k, and all T',U', and {eHMLk. Suppose T a >T'. Let'p Fk={Ol,.., } be a set of representatives of the equivalence classes of logical equivalence restricted to HMLk, and suppose 0,...i are the formulas in Fk satisfied by T'. Then T t a<Ol.. AO.A 0 l A... O >. This is a formula in HMLkl, so by hypothesis, U satisfies it too. This gives a tree U' with U a>U' and T' and U' satisfying exactly the same formulas in Fk. Since Fk is a complete set of representatives for logical equivalence, T' and U' satisfy exactly the same IMLk formulas. By inductive hypothesis, T'-U'. The case U a > U' is of course exactly similar, so the proof of 5.3 is complete. Corollary 5.4: SET iff V$EHML, S = q <=> T t. Corollary 5.5 ("Master formula" theorem for HML): For each n>O and each T, there is a formula 4(n,T) such that (i) T = (n,T); (ii) For any U, if U = P(n,T) then U- T. n Proof: As in 5.3 let F be a representative system for logical equivalence in n n(n,T)=A{PFnIT n )}. A {/\{1l-eF and not T t }. Clearly T t f(n,T). Further if U # P(n,T) then U and T agree on all formulas in F and thus on IIML. The result follows from Lemma 5.3. n n

- 25 - Theorem 5.6 (Compactness theorem for HML): Let'-1-HML. If for any finite AcF there is a tree T such that T l= for all AcA, then there is a tree U such that for all cEF, U ). Proof: We translate (the semantics of) HML into first-order logic. For each aEc let a be a binary relation symbol, and let A be a constant symbol. Let L be the first-order language determined by these symbols. For each #~HML, we define a formula ~*cL with at most one free variable. Let tt* be some fixed tautological sentence in L, and let ff*= 1-(tt ). Further define (fA$)* = f*A9*; (-)* =(9*); (a<p>)* = y(a(x,y),^ *(y)), where y is the free variable in ~* (if one exists) and x is a new free variable. For any set F of formulas in HML, let r*={f*(k) I qr}. The F* is a set of sentences in L, and it is easy to show that r* has a model if and only if r has a tree model. Now 5.6 follows immediately from the Compactness Theorem for first-order logic. We can now prove that <T,d > is a complete metric space. Let <Tk> be a w k Cauchy sequence of trees. By passing to a subsequence if necessary, we may assume that for all k, T T Now define k k k+l r={(k,Tk)' k>l} where the P(k,Tk) are given by 5.5. We claim that for any U, if U D= (k,Tk) then for any j<k, U t 4(j,Tj). The proof is by induction on k, and k=O is trivial. Now if U = 4(k+l,T ) then by 5.5, U-k+ T Since T we k+l k+l k+l1 k+l-kTk' have U-kTk. But I (k,Tk) I<k, so by Lemma 5.1 U t O(k,Tk). The claim follows by induction.

- 26 - From the claim, if A is a finite subset of F, then A has a tree model. IBy 5.(), F has a tree model T; i.e. T ~ P(k,Tk) for all k. By 5.5 again, we have'T-kTk for all k; i.e., dw(T,Tk)+O as desired. Finally, we observe that from the compactness of <T,d > we can derive the Compactness Theorem for HML. Let r be an arbitrary set of formulas such that every finite subset has a tree model. Enumerate F={(1,2,...}. For each i let A. be the set {1'..i.}. Then each A. has a tree model T.. Since <T,d > i l 1 1 w is compact, the sequence <T.> has a convergent subsequence, say to some tree T. It is easy to see that T is a tree model for r. (The compactness of <T,d > can be proved directly. One need only show completeness as in the previous sections, and the use the fact that Z is finite to show that for any E, a finite number of c-spheres cover T.)

References [ArN] Arnold, A. and Nivat, M., "Metric Interpretations of Infinite Trees and Semantics of Nondeterministic Recursive Programs", Theoretical Computer Science 11, 1980, pp. 181-205. [BaZ] de Bakker, J.W. and Zucker, J.I., "Denotational Semantics of Concurrency", Proceedings of the 14th STOC, May 1982, pp. 153-8. [Dug] Dugundji, J., Topology, Allen & Bacon, Boston, 1966. [IteM] Hennessy, M., and Milner, R., "On Observing Nondeterminism and Concurrency", 7th ICALP, Automata, Languages and Programming, LNCS 85, Springer-Verlag, New York, 1980, 299-309. [Mil] Milner, R. A Calculus of Communicating Systems, LNCS 92, Springer-Verlag, New York, 1980. [Mon] Monk, J.D., Mathematical Logic, Springer-Verlag, New York 1976. [Niv] Nivat, M., "Infinite Words, Infinite Trees, Infinite Computations", Foundations of Computer Science III, 2, (J.W. de Bakker and J. Van Leeuwen, eds.), Mathematical Centre Tract 109, 1979.

UNIVERSITY OF MICHIGAN 3 9015 03127 3116