k∈nj
¯
wjk>), wjk∈W fork ∈nj,1≤njwithj ∈n,1≤ n
where ¯w simply is the string w with every a inw exchanged with ¯a. 2 By a) – d) of proposition 3.2.14 it gives sense to use the notational convenience of & and
∇ in the definition of a normal form.
Proposition 3.2.16 For every t ∈T L there is a normal formt0 ∈T L such that t∼=t0. Proof We can transform t into a normal formt0 by using a) – h) of proposition 3.2.14.
At first we use e) and f) to get all &’s of t out on the outmost level such that we obtain a t00 = &j∈ntj, where tj is built from ∇, ¯a ∈Act and > forj ∈n.
Then for every j ∈ n transform tj by g) into t0j = ∇k∈njwjk>. By the congruence h) it
should be clear that t0 = &j∈nt0j ∼=t. 2
By inspection of definition 3.2.9 the following corollary is evident.
Corollary 3.2.17 For all p∈CL, w∈W we have:
∃q. p−→w¯ q iff w¯> ∈T L,( ¯w>, p)→∗ >
Proposition 3.2.18 Let t be on the normal form: &j∈n(∇k∈njw¯jk>). Then for all p∈ CL:
(t, p)→∗ > iff ∀j ∈n∃k ∈nj.( ¯wjk>, p)→∗ >
Proof Follows immediately from lemma 3.2.11. 2
3.3 Full Abstractness
The aim of this section is to show that the denotational and operational semantics corre-sponds or rather that ≤δ, ≤υ and ≤χ are fully abstract w.r.t. <∼a, <∼r and <∼ respectively.
Formally we want to prove:
Theorem 3.3.1 Operational Characterization TheoremIf p, q ∈ P Lthen <∼a, <∼r and <∼ are (relative) precongruences and
δ) [[p]]δ≤δ[[q]]δ iff p<∼a q υ) [[p]]υ≤υ[[q]]υ iff p<∼rq χ) [[p]]χ≤χ[[q]]χ iff p<∼q
As for Hennessy [Hen85a] it will prove convenient to introduce some more plain relations, ∗, on processes from P L, which are entirely defined on basis of the lts, and which coincide with the three testing preorders.
The rest of this section is devoted to definitions and intermediate results necessary to prove the Semantic Characterization Theorem of these relations and the Operational Charac-terization Theorem.
At first we define a map, ¯θ, on configurations which associates in a natural way a tree-semiword with the “barred” part of a configuration. I.e., for a configuration,p, ¯θ(p) gives a tree-semiword which reflects the causal order in which initiated actions can signal there completion.
Definition 3.3.2
a) Let ¯θ :CL−→T SW be defined inductively as follows:
p7→ε if p∈P L
¯
a.p7→a.θ(p)¯
pkq 7→θ(p)¯ kθ(q) if either¯ p6∈P Lor q6∈P L
b) Let ¯Θ :P L−→ P(T SW) be defined by: ¯Θ(p) :={θ(q)¯ | ∃w∈W. p−→w q}
2
For arbitrary sets of semiwords we use the following notation:
S <a T iff ∀s ∈S∃t ∈T. st S <rT iff ∀s ∈S∃t ∈T. ts S < T iff S <a T and S <r T We can now formulate the three alternative preorders.
Definition 3.3.3 Let p, q∈P L. Then a, r and are defined as follows:
p∗ q iff Θ(p)¯ <∗ Θ(q)¯
where ∗ as usual is either left out or one ofa, r. 2
In the future we will mostly omit the comment about ∗.
Theorem 3.3.4 Semantic Characterization TheoremFor all p, q inP L:
p<∼∗q iff p∗ q
The first step in the prove of this theorem is a rewriting ofp<∼∗ q.
Lemma 3.3.5 For∗= a (∗= r) and oa =>(or=⊥) we have:
p<∼∗ q iff
∗)∀(A, t)∀p0 ∈D(A, p)∃q0 ∈D(A, q).(t, p0)→∗ o∗ ⇒(t, q0)→∗ o∗
Proof We only prove the case ∗ = a, since the case ∗ = r follows in exactly the same way.
We prove p<∼a q iff a) by proving p6<∼a q iff ¬a).
p6<∼a q iff (by definition)
¬(∀(A, t)(∃p0 ∈D(A, p).(t, p0)→∗ >)⇒(∃q0 ∈D(A, q).(t, q0)→∗ >)) iff
∃(A, t)(∃p0 ∈D(A, p).(t, p0)→∗ >)∧(∀q0 ∈D(A, q).(t, q0)→∗ ⊥)iff
∃(A, t)∃p0 ∈D(A, p).((t, p0)→∗ > ∧ ∀q0 ∈D(A, q).(t, q0)→∗ ⊥) iff
∃(A, t)∃p0 ∈D(A, p)∀q0 ∈D(A, q).(t, p0)→∗ > ∧(t, q0)→∗ ⊥ iff
¬a).
In these derivations we used (t, p) →∗ > iff (t, p) 6→∗ ⊥ which was a consequence of
proposition 3.2.12. 2
The next step is to prove that the ∀t-quantifier can be moved past ∃q0 ∈ D(A, q) in ∗) of the last lemma.
Lemma 3.3.6 For∗= a (∗= r) and oa =>(or=⊥) we have:
i)∗ ∀(A, t)∀p0 ∈D(A, p)∃q0 ∈D(A, q).(t, p0)→∗ o∗ ⇒(t, q0)→∗ o∗ iff
ii)∗ ∀A∀p0 ∈D(A, p)∃q0 ∈D(A, q)∀t0.(t0, p0)→∗ o∗ ⇒(t0, q0)→∗ o∗ Proof We prove¬i)∗ iff ¬ii)∗ for the two cases of ∗. I.e.,
¬i)∗ ∃(A, t)∃p0 ∈D(A, p)∀q0 ∈D(A, q).(t, p0)→∗ o∗∧(t, q0)6→∗ o∗ iff
¬ii)∗ ∃A∃p0 ∈D(A, p)∀q0 ∈D(A, q)∃t0.(t0, p0)→∗ o∗∧(t0, q0)6→∗ o∗
If D(A, q) =∅ the result is trivial, so assume D(A, q)6=∅ in the following.
∗= a: The only if part is trivial since one just have to chose A, p0 as in ¬i)a and t0 =t for every q0 ∈D(A, q).
if: Given is ¬ii)a =∃A∃p0 ∈ D(A, p)∀q0 ∈D(A, q)∃t0.(t0, p0) →∗ > ∧(t0, q0) →∗ ⊥. From here we use theAandp0 in¬i)a. Now lett0q0 be thet0which¬ii)a ensures exists for q0 ∈D(A, q) such that (t0, p0)→∗ > ∧(t0, q0)→∗ ⊥. Then for all q0 ∈ D(A, q) we have:
(t0q0, p0)→∗ > and (t0q0, q0)→∗ ⊥ (3.1)
Sincet0q0 ∈T Lfor everyq0 ∈D(A, q) andD(A, q) is finite, we havet = &q0∈D(A,q)t0q0 ∈ T L too. By lemma 3.2.11.a),c) and (3.1) we have (t, p0) →∗ > and for every q0 ∈ D(A, q).(t, q0)→∗ ⊥, thereby establishing ¬i)a.
∗= r: Proved similar as the ∗ = a case, just with the difference in the if-part that t is constructed as ∇q0∈D(A,q)t0q0 and lemma 3.2.11.b), d) is used in proving (t, p0)→∗ ⊥, and for every q0 ∈D(A, q).(t, q0)→∗ >.
2 As seen from the proof we could not have moved the ∀t-quantifier if our test language did not contain & and ∇.
Lemma 3.3.7 LetZ = (Act∪Act)∗. For p1, p2 ∈CLwe have for z∈Z: p1kp2 −→z q
iff
∃zi ∈Z, qi. pi −→zi qi fori∈2 and q=q1kq2, z z1kz2
Notice that W ⊆Z and W ⊆Z, but Z 6⊆W ∪W.
Proof Both of the implications in this lemma is proved by induction on the length ofz.
if:
z =ε: z = ε z1 kz2 implies z1 = ε = z2, so qi = pi for i ∈ 2 and q = p1 kp2. By definition p1kp2 −→ε p1kp2 =q, so ok.
z 6=ε: Then z = a.z0 for some a ∈ Act∪Act and z0 ∈ Z. By propositionT 1.3.31 this implies ∃z01. a.z01 = z1, z0 z10 kz2 or ∃z20. a.z20 = z2, z0 z1 kz02. W.l.o.g. assume the former is true. Then p1 −→z1 q1 is the same as p1 −→a.z01 q1, so there exists some p01 such that p1 −→a p01 −→z01 q1. Since |z0|<|z| we can use the inductive hypothesis to get p01 kp2 −→z0 q1 kq2 =q. From the inference rule 5) of definition 3.2.2 we obtain p1kp2 −→a p01kp2 from p1 −→a p01, so p1 kp2 −→a.z0 q or equivalently p1kp2 −→z q.
only if:
z =ε: Then q =p1kp2 and the result should be clear.
z 6=ε: Then z =a.z0 for some a ∈Act∪Act and p1 kp2 −→a q0 −→z0 q for some q0 ∈ CL.
Looking at definition 3.2.2 we see that 5) must have been used to ensurep1kp2 −→a q0. W.l.o.g. assume this is obtained from p1 −→a p01 such that q0 = p01 kp2. By
hypothesis of induction we have that there exists z10, z2 ∈ Z and q1, q2 such that p01 z
10
−→q1, p2 −→z2 q2, q=q1 kq2, z0 z10 kz2. Let z1 =a.z10. From p1 −→a p01 we then see p1 −→z1 q1 and from propositionT 1.3.31 we get z z1kz2. This completes the inductive step.
2
Lemma 3.3.8 For all p∈CL and w∈W we have:
w∈πλθ(p)¯ iff ∃p0. p−→w¯ p0
Proof We will prove w∈πλθ(p)¯ ⇔ ∃p0. p−→w¯ p0 by induction on the structure of p.
p∈P L: We split this case out in two depending of whetherw =ε or not.
w=ε: Since p∈ P L we have ¯θ(p) = ε, so w= ε ∈ {ε}= λ(ε) = πλ(ε) =πλθ(p).¯ Also∃p0. p−→ε¯ p0, sinceε = ¯ε and p−→ε p by definition.
w6=ε: We neither have a w0 ∈ πλθ(p) with¯ w0 6= ε nor any p0 such that p −→w¯ p0, when p∈P L and w6=ε.
To see the latter assume on the contrary∃p0. p−→w¯ p0. w6=ε impliesw=a.w0 for some w0 ∈ W and a ∈ Act. So ¯w = ¯a.w¯0. Then p −→w¯ p0 can be written p−→¯a.w¯0 p0 and implies p −→¯a p00 −→w¯0 p0 for some p00 ∈CL. But it is easely seen that p∈P L, p −→y impliesy∈Act, which contradicts p−→a¯ p00,¯a∈Act.
The former is seen fromπλθ(p) =¯ {ε} as shown in the casew=ε.
p= ¯a.p00, a∈Act: At first notice πλθ(p) =¯ πλθ(¯¯a.p00) = (by definition of ¯θ) πλa.θ(p¯ 00) = (deduced from propositionT 1.3.13)πa.λθ(p¯ 00) = (corollaryT 1.3.36)a.πλθ(p¯ 00)∪{ε}. We show the implications separately.
⇒: w ∈ πλθ(p) implies¯ w ∈ a.πλ(p00) or w = ε which again implies w = a.w0 or w = ε, where w0 ∈ πλθ(p¯ 00). By definition p −→ε p = p0 which handles the former case. In the latter we use the hypothesis of induction to get∃p0. p00−→w¯0 p0. Using 3) of definition 3.2.2 we havep=a.p00−→a¯ p00. Hencep−→w¯ p0.
⇐: Looking at definition 3.2.2 we see that p = ¯a.p00 −→w¯ p0 implies ¯w = ε or
¯
w = ¯a.w¯0 for some ¯w0 such that p00 −→w¯0 p0. If ¯w = ε we have w = ¯ε = ε, so w ∈ a.πλθ(p¯ 00)∪ {ε}= πλθ(p). In the other case ¯¯ w= ¯a.w¯0, the hypothesis of induction gives usw0 ∈πλθ(p¯ 00), so w=a.w0 ∈a.πλθ(p¯ 00)∪ {ε}=πλθ(p).¯ p=p1kp2: At first notice that by lemma 3.3.7 we have:
p1 kp2 −→w¯ p0 ⇔ ∃p01, p02 ∈ CL,w¯1,w¯2 ∈ W such that p1 −→w¯i p0i for i ∈ 2,w¯
¯
w1kw¯2, p=p01kp02.
Clearly we also have ¯ww¯1kw¯2 iffww1kw2. The two implications:
⇒: We have πλθ(p¯ 1kp2) = (by propositionT 1.3.38 and definition of ¯θ)λπ(¯θ(p1)k θ(p¯ 2)) = λ(πθ(p¯ 1)kπθ(p¯ 2)), so using propositionT 1.3.13 we get w ∈ πλθ(p)¯ implies ∃wi ∈ λπθ(p¯ i), i∈ 2 such that w w1kw2. Since λπθ(p¯ i) = πλθ(p¯ i) for i ∈ 2 we can use the hypothesis to get ∃p0i. pi −→w¯ p0i for i ∈ 2. Then, as noticed, p=p1kp2 −→w¯ p01kp02 =p0.
⇐: Using the noticed againp=p1kp2 −→w¯ p0impliespi w¯i
−→p0i,i∈2. By hypothesis of inductionwi ∈πλθ(p¯ i) =λπθ(p¯ i). So sincew∈W implies6 ∃w0. w0 ≺wand ww1kw2 we get from propositionT 1.3.13w ∈λ(πθ(p¯ 1)kπθ(p¯ 2)) which, as seen above, is the same as w∈πλθ(p).¯
2 Lemma 3.3.9 Forp, q∈CL we have
θ(p)¯ θ(q)¯ iff Aθ¯(p) =Aθ¯(q) and ∀t.(t, p)→∗ > ⇒(t, q)→∗ >
Proof
if: Assume Aθ¯(p) =Aθ¯(q) and ∀t.(t, p)→∗ > ⇒ (t, q)→∗ >. We shall prove ¯θ(p) θ(q).¯ By propositionT 1.3.5 it is enough to prove λθ(p)¯ ⊆ λθ(q). Let¯ w ∈ λθ(p) be given.¯ Then also Aw = Aθ¯(p) and w ∈ πλθ(p),¯ w ∈ W, so by lemma 3.3.8 ∃p0. p −→w¯ p0 and from corollary 3.2.17 ¯w> ∈ T L,( ¯w>, p) →∗ >. By the assumption then ( ¯w>, q) →∗ >. Using the same lemmas in the opposite direction we get w∈πλθ(q). We cannot conclude¯ w∈λθ(q) directly. Assume on the contrary¯ wis a proper prefix of somew0 ∈λθ(q). Then¯ Aw ⊂Aw0. In general ∀s ∈λ(t). As =At, so Aθ¯(p) =Aw ⊂Aw0 =Aθ¯(q) which contradicts the assumption Aθ¯(p) =Aθ¯(q). Hence w∈λθ(q).¯
only if: Assume ¯θ(p) θ(q). By definition¯ Aθ¯(p) =Aθ¯(q). Let t∈T L be given such that (t, p)→∗ >. We shall prove (t, q)→∗ >. By proposition 3.2.16t can be chosen to be on normal form. I.e.,
t= &
j∈n( ∇
k∈nj
¯
wjk>), wjk∈W for k ∈nj and j ∈n
Then by proposition 3.2.18 (t, p) →∗ > implies ∀j ∈ n∃k ∈ nj.( ¯wjk>, p) →∗ > and by corollary 3.2.17 ∀j ∈ n∃k ∈ nj∃pjk. p −→w¯jk pjk. By lemma 3.3.8 wjk ∈ πλθ(p) for¯ j ∈ n, k ∈nj. Now ¯θ(p)θ(q)¯ ⇒(by propositionT 1.3.5) λθ(p)¯ ⊆λθ(q)¯ ⇒πλθ(p)¯ ⊆πλθ(q),¯ so wjk ∈ πλθ(q) and using lemma 3.3.8 again¯ ∃qjk. q −→w¯jk qjk. Reversing the arguments
from above we get (t, q)→∗ >. 2
Lemma 3.3.10 For all p∈P L and w∈W we have p−→w q implies w∈λθ(q).¯
For the proof of the lemma we shall temporarily assume to work with semiwords and not just tree-semiwords.
Proof Actually we prove the stronger result:
for all p∈CL and w∈W. p−→w q ⇒θ(p)w¯ θ(q)¯ (3.2)
from which the lemma follows since p ∈ P L ⇒ θ(p) =¯ ε and w θ(q), w¯ ∈ W ⇒ w ∈ λθ(q). Notice that though ¯¯ θ(p) ∈ T SW we do not necessarily have ¯θ(p)w ∈ T SW. However this does not change the truth of (3.2).
To prove (3.2) we first prove:
for all p∈CL, a∈Act. p−→a q⇒θ(p)a¯ θ(q)¯ (3.3)
by induction on the structure ofp considered as a member of P L.
p∈P L: Then ¯θ(p) =ε, so we shall proveaθ(q). This again will be proved by induction¯ on the structure of p.
p=N IL: Looking at definition 3.2.2 we see p−→6 b for all b, so we are done for this case.
p=b.p0: Recalling p ∈ P L when inspecting definition 3.2.2 we see that only 1) can could have been used to obtain p −→a q and b = a, so q = ¯a.p0. Since p=a.p0 ∈P L⇒p0 ∈P Lwe have ¯θ(q) = ¯θ(¯a.p0) =a.ε=a.
p=p1+p2: Only 4) could have been used. W.l.o.g. assumep1 −→a q. By hypothesis of induction aθ(q).¯
p=p1kp2: Here only 5) can come under discussion. W.l.o.g. assume p1 −→a p01, q = p01 kp2. By hypothesis of induction a θ(p¯ 01). Since p2 ∈ P L we have a θ(p¯ 01) = ¯θ(p01)kε = ¯θ(p01)kθ(p¯ 2) = ¯θ(p01kp2) = ¯θ(q). This concludes the inductive step in the proof of ¯θ(p)a θ(q) for¯ p∈P L.
p= ¯b.p0: Inspecting definition 3.2.2 we see p = ¯b.p0 −→a q, a ∈ Act implies p0 −→a q0, where q = ¯b.q0. By induction ¯θ(p0)a θ(q¯ 0). By congruence of we then have θ(p)a¯ = ¯θ(¯b.p0)a=b.θ(p¯ 0)ab.θ(q¯ 0) = ¯θ(¯b.q0) = ¯θ(q).
p=p1kp2: Only 5) could have been used. W.l.o.g. assume p1 −→a p01, q = p01 k p2. Then by hypothesis ¯θ(p1)a θ(p¯ 01). Since L(p1)∩L(p2) = ∅ and we in general for r ∈ CL have: L(¯θ(r)) ⊆ L(r) and r −→b r0 ⇒ b ∈ L(r), L(r0) ⊆ L(r) it follows that ¯θ(p1)a and ¯θ(p2) are disjoint so as ¯θ(p01) and ¯θ(p2). Therefore (¯θ(p1)kθ(p¯ 2))a, θ(p¯ 01)kθ(p¯ 2) and ¯θ(p1)akθ(p¯ 2) are well-defined and members of T SW. So we can use propositionT 1.3.29 to get (¯θ(p1)kθ(p¯ 2))aθ(p¯ 1)akθ(p¯ 2). From the congruence of and ¯θ(p1)a θ(p¯ 01) we get ¯θ(p1)akθ(p¯ 2) θ(p¯ 01)kθ(p¯ 2). By transitivity of : (¯θ(p1)kθ(p¯ 2))a θ(p¯ 01)k θ(p¯ 2). So ¯θ(p)a = ¯θ(p1 kp2)a = (¯θ(p1)kθ(p¯ 2))a θ(p¯ 01)kθ(p¯ 2) = ¯θ(p01kp2) = ¯θ(q) thereby finishing the inductive step in the proof of (3.3).
Having established (3.3) it is easy to prove (3.2) by induction on the length of w.
w=ε: Then q =p. Clearly ¯θ(p)w= ¯θ(q)εθ(q).¯
w=a.w0 for some a∈Act, w0 ∈W: Then p−→a p0 −→w0 qfor some p0 ∈CL. By hypothe-sis of induction p0 −→w0 q ⇒θ(p¯ 0)w0 θ(q). From (3.3) we have¯ p−→a p0 ⇒θ(p)a¯ θ(p¯ 0). Hence ¯θ(p)a.w0 θ(p¯ 0)w0 and by transitivity ¯θ(p)w= ¯θ(q)
2
Lemma 3.3.11 For∗= a (∗= r) and oa => (or =⊥) and allp, q∈P L we have:
∗)∀A∀p0 ∈D(A, p)∃q0 ∈D(A, q)∀t.(t, p0)→∗ o∗ ⇒(t, q0)→∗ o∗ iff
Θ(p)¯ <∗ Θ(q)¯ Proof
∗ = a: if: Let a multiset A over Act and a p0 ∈ D(A, p) be given. We shall find a q0 ∈D(A, q) such that
∀t.(t, p0)→∗ > ⇒(t, q0)→∗ >
(3.4)
By definitionp0 ∈D(A, p) implies∃w∈W. p−→w p0, Aw ∼=A and then from the definition of ¯Θ we have ¯θ(p0)∈Θ(p). The assumed premise is ¯¯ Θ(p)<a Θ(q), so¯ ∃sq ∈Θ(q).¯ θ(p¯ 0) sq. Again by definition of ¯Θ we know that there existsw0 ∈W and aq0 such thatq −→w0 q0, θ(q¯ 0) = sq. By lemma 3.3.9 ¯θ(p0) θ(q¯ 0) implies (3.4) and Aθ¯(p0) = Aθ¯(q0). So if we can prove q0 ∈D(A, q) we have proved this implication. From lemma 3.3.10 we see w0 ∈ W, q −→w0 q0 implies w0 ∈λθ(q¯ 0). Hence Aw0 =Aθ¯(q0) =Aθ¯(p) ∼=A. All in all we have w0 ∈ W, Aw0 ∼=A and q −→w0 q0, so q0 ∈D(A, q).
only if: Let sp ∈ Θ(p) be given. By definition of¯ <a we shall find an sq ∈ Θ(q) such¯ that sp sq. sp ∈ Θ(p) means¯ ∃w ∈ W∃p0. p −→w p0, ¯θ(p0) = sp. By definition of ∼= we have A ∼= Aw for the multiset A over Act defined by |A|a = ψ(w, a) for all a ∈ Act.
So p0 ∈ D(A, p). Assuming the premise of the implication to be true there exists a q0 ∈D(A, q) such that (3.4) holds. q0 ∈ D(A, q) implies ∃w0 ∈ W. q −→w0 q0, Aw0 ∼= A, so for all a ∈Act. ψ(w0, a) =|A|a, wherefore for alla ∈Act. ψ(w0, a) =ψ(w, a) and thereby Aw0 =Aw. By lemma 3.3.10 we see w0 ∈λθ(q¯ 0) and w ∈λθ(p¯ 0), so Aθ¯(q0) =Aw0 =Aw = Aθ¯(p0). This and (3.4) together with lemma 3.3.9 gives ¯θ(p0)θ(q¯ 0). Defining sq := ¯θ(q0) this reads sp = ¯θ(p0)θ(q¯ 0) =sq. Now sq ∈ Θ(q) since¯ q −→w0 q0, w0 ∈W by definition of Θ implies ¯¯ θ(q0)∈Θ(q).¯
∗= r: The proof is similar as for the case ∗= a, with the difference that another version of lemma 3.3.9 is used:
θ(q)¯ θ(p)¯ iff Aθ¯(q) =Aθ¯(p) and
∀t.(t, p)→∗ ⊥ ⇒(t, q)→∗ ⊥ (3.5)
To see this from lemma 3.3.9 notice that by proposition 3.2.12 we in general have
¬((t, r)→∗ >) iff (t, r)→∗ ⊥
wherefore (3.5) is equivalent to ∀t.(t, q)→∗ > ⇒(t, p)→∗ >. 2 Proof of Semantic Characterization Theorem
Since for ∗ = a and ∗ = r we have ¯Θ(p) <∗ Θ(q)¯ iff p ∗ q we get the theorem from lemma 3.3.5, lemma 3.3.6 and lemma 3.3.11 in the cases ∗= a and ∗= r.
Finally: p<∼q iffp<∼a q and p<∼r q iff pa q and pr q iff pq. 2 We have already seen the close connection between the operators of Aπ and A? for ? in {δ, υ, χ}and soon we shall investigate how the interpretations ofP Lin A? are related to the interpretation of P LinAπ which we now define in exactly the same way as we did in definition 3.1.13 for the A? algebras.
Definition 3.3.12 [[ ]]π :P L−→Cπ is recursively defined as follows:
[[N IL]]π =N ILπ [[a.p]]π =a.π[[p]]π [[p+q]]π = [[p]]π +π [[q]]π
[[pkq]]π = [[p]]π kπ[[q]]π
2 Recalling definition 3.1.8 where the interpretations in the Σ-po algebraAπ of the operator symbols where defined, we see that definition 3.3.12 can be read as:
[[N IL]]π ={ε}
[[a.p]]π =a.[[p]]π ∪ {ε} [[p+q]]π = [[p]]π ∪[[q]]π
[[pkq]]π = [[p]]π k[[q]]π
Lemma 3.3.13 For all p∈P L: ¯Θ(p) = [[p]]π Proof Induction on the structure ofp.
p=N IL: Since N IL6→ we have ¯Θ(N IL) ={θ(N IL)¯ }={ε}= [[N IL]]π.
p=a.p0: ¯Θ(p) = ¯Θ(a.p0) ={θ(q)¯ | ∃w∈W. a.p0 −→w q}={θ(q)¯ | ∃w∈W. w 6=ε, a.p0 −→w q} ∪ {θ(p)¯ }= (since p∈P L)
{θ(q)¯ | ∃w∈W. w 6=ε, a.p0 −→w q} ∪ {ε} (3.6)
Inspecting definition 3.2.2 we see a.p0 −→w q, w 6= ε iff w = a.w0, p0 −→w0 q0 and q = ¯a.q0 for some w0 ∈ W. So (3.6) = {θ(¯¯a.q0) | ∃w0 ∈ W. p0 −→w0 q0} ∪ {ε} = (by definition of ¯θ)a.{θ(q¯ 0)| ∃w0 ∈W. p0 −→w0 q0} ∪ {ε}=
a.Θ(p¯ 0)∪ {ε} (3.7)
By hypothesis of induction ¯Θ(p0) = [[p]]π, so (3.7) equals [[a.p0]]π. p=p1+p2: ¯Θ(p) = ¯Θ(p1+p2) =
{θ(q)¯ | ∃w∈W. p1+p2 −→w q} (3.8)
Again from definition 3.2.2 we see p1 +p2 −→w q iff either p1 −→w q orp2 −→w q, so (3.8) equals{θ(q)¯ | ∃w∈W. p1 −→w q} ∪ {θ(q)¯ | ∃w∈W. p2 −→w q}. The result then follows directly from the hypothesis.
p=p1kp2: ¯Θ(p) = ¯Θ(p1kp2) =
{θ(q)¯ | ∃w∈W. p1kp2 −→w q} (3.9)
The next to see is that (3.9) equals
{θ(q¯ 1kq2)| ∃w1, w2∈W∃q1, q2 ∈CL. p1 −→w1 q1, p2 −→w2 q2} (3.10)
⊆: Follows directly from lemma 3.3.7.
⊇: Let s in (3.10) be given. Then there exists wi ∈ W, qi ∈ CL. pi wi
−→ qi for i ∈ 2. Since p1 kp2 is well-defined we have L(p1)∩L(p2) = ∅. By corollary 3.2.3 then q1kq2 and w1 kw2 are well-defined too, so we can define q := q1kq2. From propositionT 1.3.5.b) we knowλ(w1kw2)6=∅, so there exists aw∈W. w w1kw2. Then we can use lemma 3.3.7 to get p1 kp2 −→w q. Hence s = ¯θ(q1 kq2) = ¯θ(q) in (3.9). Clearly (3.10) equals {θ(q¯ 1)| ∃w1 ∈W. p1 −→w1 q1} k {θ(q¯ 2)| ∃w2 ∈W. p2 −→w2 q2} = ¯Θ(p1)kΘ(p¯ 2) from which the result follows directly from the hypothesis of induction.
2
Lemma 3.3.14 For all S ⊆SW (hence also for S ⊆T SW) we have δS <aS <aδS
υS <rS <rυS χS < S < χS
Proof δS <a S and υS <r S follows directly from the definition of δ and υ. S <a δS, S <r υS and S < χS follows from the reflexivity of and S⊆δS, υS, χS.
χS < S: We shall prove χS <a S and χS <r S. But this is evident since by definition
s∈χS impliest st0 for some t, t0 ∈S. 2
Combining the last two lemmas we immediately have:
Corollary 3.3.15 For all p, q∈P L:
pa q iff δ[[p]]π <a δ[[q]]π prq iff υ[[p]]π <rυ[[q]]π pq iff χ[[p]]π < χ[[q]]π
Lemma 3.3.16 For? in{δ, υ, χ}and all p∈P L:
?) [[p]]? =?[[p]]π
Proof If we for ?S∈C? have:
?opπ(?S) =?opπ(S) (3.11)
then ?) is easely proved by induction on the structure of p as indicated here: [[op(p)]]? = op?([[p]]?) = (by proposition 3.1.9) ?opπ([[p]]?) = (hypothesis of induction) ?opπ(?[[p]]π) = (by (3.11)) ?opπ([[p]]π) =?[[op(p)]]π.
In proving (3.11) we use the properties of (sets of) tree semiwords, the fact that δ and υ distributes over ∪and the closure properties of ?:
??S =?S (3.12)
for arbitrary sets of semiwords S.
The proof of (3.11):
opπ =N ILπ: Trivial.
opπ =a.π: ?a.π?S = ?(a.?S∪ {ε}), which by the ∪-distributivity of δ, υ and for ? = χ:
PropositionT 1.3.24.a) equals ?a.?S ∪?{ε}. By corollaryT 1.3.19.b) in the case of
? = υ and (3.12), corollaryT 1.3.16.a), corollaryT 1.3.25 in the other cases we see that this quantity is the same as ?a.S∪?{ε}. With the same arguments as above this equals?(a.S∪ {ε}) = ?a.πS.
opπ = +π: ?(?S+π?T) = ?(?S∪?T) = (by (3.12),∪-distributivity of δ, υand in the case
?=χ: corollaryT 1.3.23.c)) ?(S∪T) =?(S+π T).
opπ =kπ: ?(?Skπ ?T) = ?(?S k?T). Using corollaryT 1.3.16.b) when ? = δ, (3.12) and propositionT 1.3.18.d) in the case ?=υ and finally for ?=χ: corollaryT 1.3.23.b), we see ?(?Sk?T) =?(SkT) =?(Skπ T).
2
Lemma 3.3.17
δ) ∀S, T ∈Cδ. S <a T iff S≤δT υ) ∀S, T ∈Cυ. S <r T iff S≤υT χ) ∀S, T ∈Cχ. S < T iff S≤χT
Proof Recall at first corollary 3.1.4 that for ?in {δ, υ, χ}: ?) ∀T ∈C?. ?(T) =T. δ) if: Assume S≤δT or equivalently S⊆T. We shall show ∀s ∈S∃t ∈T. st. Let
s∈S be given. Since S ⊆T and is reflexive we can chose t =s.
only if: Assume S <a T. We shall show S ⊆ T. Let a s ∈ S be given. By assumption there exists a t∈T such thats t. SinceδT =T we have s∈T too.
υ) Similar.
χ) if: Assume S≤χT. We shall prove S <a T and S <r T. This follows as forδ) and υ).
only if: Assume S < T. We shall prove S ⊆ T. Let s ∈ S. From S <a T we see
∃t0 ∈ T. s t0 and from S <r T: ∃t ∈ T. t s. Hence ∃t, t0 ∈ T. t s t0 and thereby s ∈χT. Since for χT =T the result follows.
2
From the last two lemmas and corollary 3.3.15 it follows:
Corollary 3.3.18 For all p, q∈P L:
δ) pa q iff [[p]]δ≤δ[[q]]δ υ) prq iff [[p]]υ≤υ[[q]]υ χ) pq iff [[p]]χ≤χ[[q]]χ
We are now in a position to prove the operational characterization theorem on page 75.
Proof (ofOperational Characterization Theorem)
From the Semantic Characterisation Theoremand corollary 3.3.18 it follows that e.g., <∼a and ≤δ agrees onP L. By corollary 3.1.11 the different operators of Σδ are (relative) ≤δ -monotone, so from the compositional definition of [[ ]]δ we deduce that ≤δ is a (relative) precongruence. Because of the agreement between <∼a and ≤δ this must be the case for
<∼a too. Similar for the other preorders. 2
Before ending the section we shall prove that the denotational maps can denote any element of the relevant domain—a fact which will be used in the next chapter.
Proposition 3.3.19 [[ ]]? :P L−→C? is surjective for ? in{δ, υ, χ}.
Proof Given aS ∈C?. We shall find ap∈P Lwith [[p]]? =S. S ∈C?implies that there exists a T ∈ Pf(T SW)\ ∅such that ?πT =S. Because by lemma 3.3.16 [[p]]? =?[[p]]π we see that it is enough to find a p such that [[p]]π =πT since then [[p]]? =?[[p]]π =?πT =S.
Now π is ∪-distributive, so πT = ∪t∈Tπ(t). Hence we are done if we for every t ∈ T can find a pt ∈ P L such that [[pt]]π = π(t), because then we can chose p to be Σt∈Tpt (T is finite) and get [[p]]π = (by definition of +π and propositionT 1.3.35.c)) ∪t∈T[[pt]]π =
∪t∈Tπ(t) =πT.
We will now find such a pt for a given t by induction on the size of t.
Basis: Clearly t=ε. Let pt=N IL. Then [[p]]π =N ILπ ={ε}=π(ε) = π(t).
Inductive step: Then γ(t) 6= {ε} and t = εk(kγ(t)\ {ε}) = kγ(t)\ {ε}. By corollaryT 1.1.8.f)t0 ∈RT SW for every t0 ∈γ(t)\ {ε}.
If γ(t) \ {ε} only consists of one rooted tree semiword, t0, propositionT 2.2.15.a) gives us ∃t00 ∈ T SW. t0 = a.t00. By hypothesis of induction we can find a p00 ∈ P L such that [[p00]]π =π(t00). Let p=a.p00. Then [[p]]π =a.π[[p00]]π =a.π(t00)∪ {ε}= (by corollaryT 1.3.36) π(a.t00) =π(t0) =π(kγ(t)\ {ε}) =π(t).
Ifγ(t)\{ε}consists of more than one rooted tree-semiword we clearly can writet as t1 kt2, where t1, t2 are nonempty tree-semiwords of size less than t. By hypothesis we find pi ∈ P L.[[pi]]π =ti for i∈ 2. Let p =p1kp2. Then [[p]]π = [[p1]]π kπ[[p2]]π = π(t1)kπ(t2) = (by propositionT 1.3.35) π(t1kt2) =π(t).
2 Finally we will briefly compare the equivalences. Since <∼ is defined as the intersection of
<∼a and <∼r it is immediate from the full abstraction results of this section, that both [[ ]]δ and [[ ]]υ is as abstract as [[ ]]χ. By the two process terms:
p1 =a.b.N IL+a.N ILkb.N IL and p2 =a.N ILkb.N IL
it follows that [[ ]]δ is strictly more abstract than [[ ]]χ (identified by [[ ]]δ but not by [[ ]]χ).
That [[ ]]υ also is strictly more abstract than [[ ]]χ is seen from p1 and p3 =a.b.N IL
The same examples can be used to see that in general [[ ]]δ is not as abstract as [[ ]]υ and vice versa; p1 and p2 are identified by [[ ]]δ but not by [[ ]]υ and conversely withp1 and p3.
Chapter 4
Algebraic Characterization
The purpose of this chapter is to introduce two proof systems which on a purely syntactical level enables us to reason about how processes of P Lcan be interrelated via the different operational precongruences. The idea will be that if a certain relation between two process terms can be shown in the proof system then they will be related via the corresponding test preorder in the same way.
As for the previous chapter most of the concepts are as described in [Hen85a] and we shall also use some of the results.
Given a set of variables, X, and an arbitrary Σ-po algebra, A = (CA,≤A,ΣA), an A-assignment is a mapping ρA : X −→ CA, and from the proof of the freeness theorem we know a structural defined unique extension of ρA to the term algebra for Σ(X). If BL is extended to the term algebra for the signature with variables, the corresponding extensions of the different A?-assignments would not always be well-defined. Some modifications are therefore necessary.
For a set of variables, X, BL is extended to include terms with variables from X simply by extending the signature Σ to Σ(X) by augmenting Σ0 with X. The so obtained term algebra is denoted BL(X). We shall assume that each variable, x∈X, has an associated sort/ label set, Lx and furthermore that there is an infinite number variables for every possible sort (finite subset of Act). Extending the map L from BL to BL(X) by letting L(x) =Lxfor everyx∈Xwe can similarly asP Lwas extracted fromBLdefineP L(X)—
the open process terms—to be those terms of BL(X) where every subterm of form tkt0 satisfies L(t) ∩L(t0) = ∅. To emphasize the possibility of variables we shall often use t, t0,. . . to denote terms fromP L(X).
AnA?-assignment, ρA?, is now defined to be a mappingX −→C? such that for allx∈X we have:
ρA?(x) =S⇒L(x) =L(S)
IfρA? is extended toP L(X) in the same way as in the freeness theorem,ρA? is in this way ensured to be well-defined (and unique). Notice that [[p]]? =ρA?(p) for allA?-assignments, ρA?, if p∈P L.
The same goes for syntactic substitutions, i.e., P L(X)-assignments. That is ρ : X −→
P L(X) is aP L(X)-assignment if for every x∈X:
ρ(x) =t⇒L(x) =L(t)
The extension of a P L(X)-assignment to syntactic substitution will be written postfix.
4.1 Proof Systems
In this section we are going to formulate two proof systems DEDδ and DEDπ respec-tively. These proof systems DEDδ and DEDπ will contain the (usual) inference rules for (relative) precongruence, instantiation, transitivity, reflexivity as well as the inference rule for basic inequations:
Reflexivity:
t≤t
Transitivity: t≤t0, t0 ≤t00 t≤t00 Substitutivity: t≤t0
a.t≤a.t0
t1 ≤t01, t2 ≤t02 t1+t2 ≤t01+t02 t1 ≤t01, t2 ≤t02
t1kt2 ≤t01kt02 provided L(t1)∩L(t2) = ∅=L(t01)∩L(t02) Instantiation: t≤t0
tρ≤t0ρ for every P L(X)-assignment ρ Inequations:
t≤t0 for every (π-)δ-inequation t≤t0
The δ-inequations and π-inequations respectively are as displayed below:
π-inequations:
+1 x+ (y+z) = (x+y) +z +2 x+y =y+x
+3 x=x+N IL
+4 x=x+x
k1 xk(ykz) = (xky)kz k2 xky=ykx k3 x=xkN IL .+ a.(x+y) =a.x+a.y k+ xk(y+z) =xky+xkz
+5 x≤x+y
δ-inequations: π-inequations and δ.k a.(xky)≤a.xky
So the inequations are just relations between terms of P L(X).
More generaly for a proof system DED(E) of inequations as described by Hennessy [Hen85a], where E is the set of basic inequations we have the following notions.
The inequations inference rule gives a statement t ≤ t0 for every t ≤ t0 in E. These statements together witht ≤tobtained by the reflexivity inference rule (with no premise) will be denoted the axioms.
A proof, P, is a sequence of statements
t1 ≤t01, t2 ≤t02,. . ., tn ≤t0n
where each statementti ≤t0i, i∈n, is derived by applying the inference rules to statements earlier in the sequence. Clearly each ti ≤t0i, i∈n has it’s own proof which is a part of P. We denote it by Pti≤t0
i.
We will say that a proof has the simple instantiation property if instantiation only is used on the axioms.
Later in section 4.3 we shall see that if P is a proof of t ≤t0 then there is another proof P0 of r≤t0 with this property.
Notice that DEDδ andDEDπ just are special cases of DED(E) with E =δ-inequations and E =υ-inequations respectively.
If the statement t ≤ t0 can be proved in DEDπ we shall write this as `π t ≤ t0. Similar for the statements of DEDδ. Since the π-inequations are contained in the δ-inequations it follows that `π t ≤ t0 implies `δ t ≤t0. As mentioned in the beginning to the chapter the proof systems can be used to deduce how processes can be operationally related. This will be more accurately addressed in the next two sections.