Denotational Set-up

The well-known trace models (not necessarily maximal) e.g., [OH86, Hoa85] are based on sets of sequences of actions from ∆ (words) and using the shuffle operator when dealing with k. These and related models can be viewed as abstractions of computations trees canonicical associated with the process expressions. In the trace models for the equivalence

corresponding to the smallest set of direct tests the abstraction would consist in taking the set of words which constitute the paths from the root to the leaves of the computation tree as illustrated in:

With these models in mind it offers it self for the generalized traces, to look for models based on sets of sequences of direct tests, i.e., subsets ofG^∗. However because immediate tests are directed towards discovering concurrency as mirrored in pomsets and in order to clear the way for the more complicated model in the next chapter we shall devise corresponding models in the pomset framework. So the idea is to obtain a similar picture as above using pomsets in stead.

Example: If we intuitively think of℘as associating pomsets to expressions andδ_w gives the linearizations of pomsets we expect:

To make this picture precise and generalize to an arbitrary set of direct tests, G, we shall at first look for pomsets which only contains multisets from G. From G ⊆ M and the definition of multiset induced pomset properties we know thatP_M⊆G are the pomsets we are looking for.

For arbitrary pomset properties, P_∗ and P_∗0, we denote P_∗∩P_∗0 by P_∗,∗0 and similar for the δ_∗-closure we for a pomset p denote δ_∗(p)∩P_∗0 by δ_∗,∗0(p).

Notice that δ_∗,∗0(p) alternatively may be written as {q∈P|qp, P_∗(p) and P_∗0(p)}. Next it seems natural to seek a pomset property reflecting the general nature of when the multisets of a pomset are in sequence, i.e., pomsets of the form A₁·A₂·. . .·A_n. Pomsets of this form can be considered as “layered” in the sense that they may be viewed as “a linear order on top of a set of completely unordered pomsets (the individual multisets, A_i’s)”. One way to formalize this property is the following:

Definition 7.3.1 P_and-Property for Pomsets

A pomset p is said to have the P_and-property, P_and(p), iff for all x, x⁰, y, y⁰ in X_p we have:

if x co_p y

then

∀z. x <p z ⇒y <p z and

∀z. y <_p z ⇒x <_p z 2

Example: a

>b

c^Z-Z~d has the Pand-property, a ^-b

c^Z-Z~d and a^-b

a has not.

Proposition 7.3.2 The P_and-property is hereditary and dot synthesizable.

Proof Because of the universal quantification ofxandyin the definition ofP_and(p) and because the partial order just is restricted in subpomsets it follows that theP_and-property is hereditary.

It is also dot synthesizable as can be seen by using proposition 6.4.7: Let a lpo p and a subset Y of Xp given such that Pand(p|X_p\Y),Pand(p|Y) and

∀x∈X_p\Y∀y∈Y. xco6 _p y (7.1)

Suppose on the contrary ¬P_and(p). By definition there must be x, y, z ∈ X_p with y co_p x <_p z and y 6<_p z. y 6<_p z cannot mean z ≤p y because we then would get x ≤p y contradicting y co_p x, so actually:

y co_p x <_p z co_p y (7.2)

If x, y and z all are in one of the two sets X_p \ Y and Y, we get a contradiction to P_and(p|X_p\Y) and P_and(p|Y). Otherwise one element must be in one of the sets and the remaining two in the other set. From (7.2) we see that at least one of the two elements belonging to the same set must be concurrent to the element in the other set—a

contra-diction to (7.1). 2

Proposition 7.3.3 The P_and-property has the following alternative characterization:

(p6=ε and P_and(p)) iff ∃n≥1∃A₁,. . ., A_n∈M. A₁·. . .·A_n=p From this and the definition of P_M⊆G,and we immediately get:

(p6=ε and P_M⊆G,and(p)) iff ∃n≥1∃A₁,. . ., A_n∈G. A₁·. . .·A_n=p

We abbreviateP_M⊆G,andby P_G. P_M⊆Dis clearly hereditary so from the propositions 6.4.8 and 7.3.2 we get:

Corollary 7.3.4 The P_G-property is hereditary and dot synthesizable.

With the above biimplications it is not hard to see that G^∗ andP_G coincide (are isomor-phic), and as a consequence we shall often identify them in the sequel. So there is hope that we can base our models on subsets of P_G.

It only remains to establish a connection from BL-expressions to nonempty subsets of P_G. To this end we introduce a canonical map which give a natural association of sets of pomsets with BL-expressions.

Definition 7.3.5 Canonical Pomset Association

The canonical associated pomsets of a BL-expression is given by the map ℘ : BL −→

P(P\ {ε})\ ∅ defined compositionally as follows:

℘(a) ={a}

℘(E₀;E₁) =℘(E₀)·℘(E₁)

℘(E₀⊕E₁) =℘(E₀)∪℘(E₁)

℘(E₀kE₁) =℘(E₀)×℘(E₁)

Example: ℘((a⊕b) ; (akc)) =

(

a¹a

PPqc, b¹a

PPqc

)

We can then let denotations in our models go via this map:

Definition 7.3.6 [[ ]]_G :BL −→ P(P_G\ {ε})\ ∅with [[E]]_G =δ_G(℘(E)). 2 So, our G-model is finite sets of P_G-pomsets partially ordered by inclusion: ⊆.

It is easy to check that the maps of the example on page 156 are correct and that they composed correspond to the denotational map just defined.

[[ ]]_G together with the partial order induces a denotational preorder ≤_G over BL by:

E₀ ≤_G E₁ iff [[E₀]]_G ⊆[[E₁]]_G

Having models using sets of sequences from ∆^∗ in mind it is not hard to come up with:

Theorem 7.3.7 [[ ]]_G can be defined compositionally by:

[[a]]_G ={a}

[[E₀;E₁]]_G = [[E₀]]_G·[[E₁]]_G [[E₀⊕E₁]]_G= [[E₀]]_G∪[[E₁]]_G [[E₀kE₁]]_G =δ_G([[E₀]]_G×[[E₁]]_G)

Notice that δ_G here acts as the natural generalization of the shuffle/ zip operator for ∆^∗. Proof At first notice that corollary 7.3.4 enables us to apply the propositions 6.4.4 and 6.4.10 in the proof. We look at the different cases:

a: Evident by inspection of the definitions.

E₀;E₁: Follows directly from the fact thatδ_G distributes over pomset sequential compo-sition (propocompo-sition 6.4.4 and 6.4.10). See also the last case.

E₀⊕E₁: Similar because δ_G is a natural generalization to sets and therefore distributes over sets.

E₀kE₁: [[E₀ kE₁]]_G =δ_G(℘(E₀kE₁)) definition of [[ ]]_G

=δ_G(℘(E₀)×℘(E₁)) definition of ℘

=δ_G(δ_G(℘(E₀))×δ_G(℘(E₁))) proposition 6.4.4

=δ_G([[E₀]]_G×[[E₁]]_G) definition of [[ ]]_G

2

7.4 Full Abstractness

The first proposition says that ≤_G is inherited in allBL-contexts.

Proposition 7.4.1 ≤_G is a precongruence over BL.

Proof From theorem 7.3.7 we know a compositional definition of [[ ]]_Gusing⊆-monotone operators (proposition 6.3.4), and hence ≤_G is a precongruence. 2

Theorem 7.4.2 [[ ]]_G is fully abstract w.r.t. ^<_∼G, because a) ^<_∼G is a precongruence w.r.t. BL

b) E₀ ^<_∼G E₁ iff E₀ ≤_G E₁

Proof a) is a consequence of proposition 7.4.1 and b) which in turn is a direct

conse-quence of the proposition below. 2

Proposition 7.4.3 For every E₀, E₁ ∈BL we have [[E₀]]_G ⊆[[E₁]]_G iff E₀ ^<_∼G E₁ Proof In the last section we saw:

(p 6=ε and P_G(p)) iff ∃n≥1∃A₁,. . ., An∈G. A₁·. . .·An=p from which we immediately get:

P_G(p) iff ∃n≥1∃A₁,. . ., A_n∈Gε. A₁·. . .·A_n =p

Recalling our convention to identify G^∗ and P_G we then from lemma 7.4.4 below get for E ∈BL:

[[E]]_G={A₁·. . .·A_n∈G^∗_ε |n≥ 1, E =^A⇒¹ . . .=^A⇒ †}ⁿ ={s ∈G^∗ |E ⇒ †}^s (7.3)

with ⇒^∅ interpreted according to the convention below.

The proof is now a simple matter: [[E₀]]_G ⊆ [[E₁]]_G iff {s ∈ G^∗ | E₀ ⇒ †} ⊆ {^s s ∈ G^∗ |

E₁ ⇒ †}^s iff E₀ ^<_∼G E₁. 2

For simplicity of the following lemmas we shall temporarily adopt the notation E −→^∅ E⁰ to mean E = E⁰ wherefore E ⇒^∅ E⁰ also means E >−→^∗ E⁰. For the same reason the lemmas are formulated slightly stronger than needed where they are used.

Lemma 7.4.4 Given E ∈BL and multisets A₁,. . ., A_n ∈Gε (n≥1). Then E =^A⇒¹ . . .=^A⇒ †ⁿ iff ∃p∈℘(E). A₁·. . .·Anp

Proof Before proving each implication separately notice that p ∈ ℘(E) implies p 6= ε for E ∈BL and that every subexpression of E ∈BL belongs toBL too..

If: By induction on the structure ofE.

E =a: ℘(a) = {a} and we have p = a. Clearly A₁ ·. . .·An a implies that exactly one Ai ={a}, the rest of them equal to ∅. The result then follows from a ⇒^∅ . . .⇒^∅ a−→ †^a ⇒^∅ . . .⇒ †^∅ .

E =E₀;E₁: From ℘(E) = ℘(E₀)·℘(E₁) we then see p = p₀·p₁ where p_i ∈ ℘(E_i) for i = 0,1. By lemma 7.4.7 A₁ ·. . .·A_n p₀·p₁ implies n ≥ 2 and the existence of a 1≤j < n such that A₁·. . .·A_j p₀ and A_j+1·. . .·A_n p₁. By hypothesis of induction then E₀ =^A⇒¹ . . . =^A⇒ †^j and E₁ ^A=^j+1⇒ . . . =^A⇒ †ⁿ . By proposition 7.2.3 then E₀;E₁ =^A⇒¹ . . .=^A⇒ †^j ;E₁. Since†;E₁ >−→E₁ we get E₀;E₁ =^A⇒¹ . . .=^A⇒^j E₁ ^A=^j+1⇒ . . .=^A⇒ †ⁿ as desired.

E =E₀⊕E₁: p ∈ ℘(E) = ℘(E₀)∪℘(E₁) implies p ∈ ℘(E₀) or p ∈ ℘(E₁). Suppose w.l.o.g. p ∈ ℘(E₀). By hypothesis of induction E₀ =^A⇒¹ . . .=^A⇒ †ⁿ so from the rules of >−→ then also E₀⊕E₁ >−→E₀ =^A⇒¹ . . .=^A⇒ †ⁿ .

E =E₀kE₁: p ∈ ℘(E) = ℘(E₀)×℘(E₁) implies p =p₀ ×p₁ for some p₀ ∈ ℘(E₀) and p₁ ∈ ℘(E₁). According to proposition 7.4.10 A₁ ·. . .·A_n p₀ ×p₁ implies the existence of multisets A⁰₁,. . ., A⁰_n, A¹₁,. . ., A¹_n such thatAⁱ₁·. . .·Aⁱ_n pi fori= 0,1 and A_j = A⁰_j ×A¹_j for j = 1,. . ., n. This means Aⁱ_j ,→ A_j, so because G has the closure property:

B ,→C, C ∈G⇒B ∈Gε

the Aⁱ_j’s actually belongs to G_ε. Hence we can use the hypothesis of induction to see E_i =^A⇒ⁱ¹ . . .=^A⇒ †ⁱⁿ for i= 0,1. By proposition 7.2.3 then E₀kE₁ =^A⇒¹ . . .=^A⇒ † k †ⁿ and the result follows from † k †>−→ †.

Only if: We shall also prove this implication by induction on the structure of E.

E =a: Since a >6−→ and a −→^A F implies A= a and F =† there is exactly one A_i =a and the rest equal to ∅. Recalling ∅(= ε) neutral to · we see from a a and

℘(a) ={a} that we are done.

E =E₀;E₁: BecauseE₀ ∈BL we cannot haveE₀ >−→^∗ †. For purely structural reasons we cannot for any E₀⁰ and E₁ have E₀⁰ ;E₁ = † neither, so using lemma 7.4.5 on E₀ ;E₁ =^A⇒¹ . . . =^A⇒ †ⁿ we deduce n ≥ 2 and the existence of a 1 ≤ j < n such that E₀ =^A⇒¹ . . . =^A⇒ †^j and E₁ ^A=^j+1⇒ . . .=^A⇒ †ⁿ . By hypothesis then A₁·. . .·A_j p₀

and A_j+1. . .A_n p₁ where p_i ∈ ℘(E_i) for i = 0,1. By -monotonicity of · then A₁·. . .A_j·A_j+1·. . .·A_n p₀·A_j+1·. . .·A_n p₀·p₁ ∈℘(E₀)·℘(E₁).

E =E₀⊕E₁: Inspecting the definition of>−→and −→^A1 one easely sees thatE₀⊕E₁ =^A⇒¹ . . . =^A⇒ †ⁿ implies E₀ ⊕E₁ >−→ F =^A⇒¹ . . . =^A⇒ †ⁿ where F = E₀ or F = E₁. The result then follows from the hypothesis of induction and definition of ℘.

E =E₀kE₁: Then E₀ kE₁ =^A⇒¹ . . . =^A⇒ †ⁿ . Chosing E = † in lemma 7.4.6 we see that there areA⁰₁,. . ., A⁰_n, A¹₁,. . ., A¹_n∈ Gε such that A_j = A⁰_j ×A¹_j for j = 1,. . ., n and E_i =^A⇒ⁱ¹ . . .=^A⇒ †ⁱⁿ for i= 0,1. Using the hypothesis of induction together with (6.3):

(p×q)·(p⁰×q⁰)(p·p⁰)×(q·q⁰)

the desired result is then obtained similarly as in the case E =E₀ ;E₁.

2

Notice that we only used the closure property ofG in theif part of the proof.

Lemma 7.4.5 Suppose n ≥ 1 and E₀ ; E₁ =^A⇒¹ . . . =^A⇒ⁿ E for A₁,. . ., A_n ∈ Gε and E₀;E₁ ∈CL. Then either

a) E₀ >−→^∗ †, E₁ =^A⇒¹ . . .=^A⇒ⁿ E or

b) E₀ =^A⇒¹ . . .=^A⇒ †^j ,E₁ ^A=^j+1⇒ . . .=^A⇒ⁿ E for a 1≤j < n or c) E₀ =^A⇒¹ . . .=^A⇒ †ⁿ ,E₁ >−→^∗ E or

d) E₀ =^A⇒¹ . . .=^A⇒ⁿ E₀⁰, E₀⁰ ;E₁ =E for some E₀⁰ ∈CL

Proof At first we prove by natural induction for arbitrary m and F, E₀;E₁ ∈CL:

E₀;E₁ >−→^m F

⇓

i) E₀ >−→^∗ †, E₁ >−→^∗ F or ii) E₀ >−→^∗ F₀⁰, F₀⁰;E₁ =F (7.4)

m= 0: Here E₀;E₁ =F and we can choose F₀⁰ =E₀.

m > 0: Then for some H ∈ CL we have E₀;E₁ >−→H >−→^m−1 F. According to the definition of >−→ there are two cases:

E₀ =†and H =E₁: I.e., E₁ >−→^m−1 F and i) holds.

E₀ >−→H₀andH₀;E₁ =H: From the hypothesis of induction used onH₀;E₁ >−→^m−1 F we get either (H₀ >−→^∗ †, E₁ >−→^∗ F) or (H₀ >−→^∗ F₀⁰, F₀⁰;E₁ =F). In the former case i) is established because E₀ >−→H₀ >−→^∗ † and in the latter case we get ii).

Using (7.4) we can now prove the lemma by induction on n.

n = 1: If A₁ =∅ we haveE₀;E₁ >−→^∗ E and we can use (7.4) to see that c) or d) holds.

So assume A₁ 6= ∅ and we have E₀;E₁ >−→^∗ F −→^A1 F⁰ >−→^∗ E for some F, F⁰ ∈ CL.

We consider two case according to (7.4):

i) Here we have E₀ >−→^∗ †, E₁ >−→^∗ F −→^A1 F⁰ >−→^∗ E and a) holds.

ii) E₀ >−→^∗ F₀⁰, F₀⁰ ;E₁ −→^A1 F⁰ >−→^∗ E. Since A₁ 6= ∅ we must have F⁰ = F₀⁰⁰ ;E₁ where F₀⁰ −→^A1 F₀⁰⁰. Using (7.4) on F₀⁰⁰;E₁ >−→^∗ E we see F₀⁰⁰ >−→^∗ †, E₁ >−→^∗ E or F₀⁰⁰ >−→^∗ E₀⁰, E₀⁰ ;E₁ = E. In the former case we have E₀ >−→^∗ F₀⁰ −→^A1 F₀⁰⁰>−→^∗ †, E₁ >−→^∗ E and c) holds. In the latter caseE₀ >−→^∗ F₀⁰ −→^A1 F₀⁰⁰>−→^∗ E₀⁰, E₀⁰ ;E₁ =E so here d) holds.

n > 1: Then E₀ ;E₁ =^A⇒¹ F =^A⇒² . . . =^A⇒ⁿ E. From the case n = 1 we know that for E₀;E₁ =^A⇒¹ F there are the following three main possibilities:

E₀ >−→^∗ †, E₁ =^A⇒¹ F: Then alsoE₁ =^A⇒¹ . . .=^A⇒ⁿ E and a) holds.

E₀ =^A⇒ †¹ , E₁ >−→^∗ F: Here we get E₁ =^A⇒² . . .=^A⇒ⁿ E and b) is established with j = 1.

E₀ =^A⇒¹ F₀⁰, F₀⁰ ;E₁ =F: The hypothesis of induction used onF₀⁰;E₁ =^A⇒² . . .=^A⇒ⁿ E yields:

a’) F₀⁰ >−→^∗ †,E₁ =^A⇒² . . .=^A⇒ⁿ E or

b’) F₀⁰ =^A⇒² . . .=^A⇒ †^j , E₁ ^A=^j+1⇒. . .=^A⇒ⁿ E for a 2≤j < nor c’) F₀⁰ =^A⇒² . . .=^A⇒ †ⁿ , E₁ >−→^∗ E or

d’) F₀⁰ =^A⇒² . . .=^A⇒ⁿ E₀⁰, E₀⁰ ;E₁ =E

Clearly we have E₀ =^A⇒ †¹ in the case a’) thereby getting b) for j = 1. In the remaining cases b’), c’) and d’) we directly get b), c) and d) respectively.

2 Lemma 7.4.6 Suppose n ≥ 1 and E₀ kE₁ =^A⇒¹ . . . =^A⇒ⁿ E for A₁,. . ., A_n ∈ G_ε and E₀kE₁ ∈CL. Then there areE₀⁰, E₀⁰ ∈CLand A⁰₁,. . ., A⁰_n, A¹₁,. . ., A⁰_n ∈Gε such that

Aj =A⁰_j×A¹_j forj = 1,. . ., n and E_i =^A⇒ⁱⁱ . . .=^A⇒ⁱⁿ E_i⁰ for i= 0,1 and E₀⁰ kE₁⁰ =E or E₀⁰, E₁⁰ ={†, E}

Proof At first we by natural induction prove for arbitrary m and E₀, E₁ ∈ CL that E₀kE₁ >−→^m E implies the existence of some E₀⁰, E₁⁰ ∈CLsuch that:

E₀ >−→^∗ E₀⁰, E₁ >−→^∗ E₁⁰ and E₀⁰ kE₁⁰ =E or {E₀⁰, E₁⁰}={†, E} (7.5)

m= 0: Then E =E₀kE₁ and we can choose E_i⁰ =Ei.

m > 0: This means E₀ kE₁ >−→ F >−→^m−1 E. According to the definition of >−→

there are four cases:

E₀ =†and E₁ =F: Choose E₀⁰ =†, E₁⁰ =E and we are done.

E₁ =†and E₀ =F: Symmetric.

E₀ >−→F₀⁰ and F₀⁰ kE₁ =F: Use the hypothesis of induction on F₀⁰kE₁ >−→^m−1 E to find E₀⁰, E₁⁰ such that F₀⁰ >−→^∗ E₀⁰, E₁ >−→^∗ E₁⁰ and (E₀⁰ kE₁⁰ = E or {E₀⁰, E₁⁰} = {†, E}). The result then follows becauseE₀ >−→^∗ F₀⁰ >−→^∗ E₀⁰ or equallyE₀ >−→^∗ E₀⁰.

E₁ >−→F₁⁰ and E₀ kF₁⁰ =F: Symmetric to the last case.

Next we prove the lemma by induction on n:

n = 1: We haveE₀kE₁ >−→^∗ F −→^A1 H >−→^∗ E. We can now use (7.5) onE₀kE₁ >−→F

n = 1: The situation is A₁ = p₀·p₁. The premise cannot hold since p₀,p₁ 6= ε implies that there are at least two ordered elements of p₀ ·p₁, but this contradicts A₁ =p₀ ·p₁ because the elements of A₁ are unoredered (A₁ ∈Mε).

n > 1: Equally n ≥ 2. Since p₀ 6= ε we can apply proposition 7.4.8 below to find a p⁰₀ such that A₁·p⁰₀ =p₀ and A₂·. . .·A_n=p⁰₀·p₁.

If p⁰₀ =ε we have p₀ =A₁ and A₂·. . .·A_n=ε·p₁ =p₁ wherefore we can choose j = 1.

Otherwise if p⁰₀ 6=εwe can use the induction to find 2≤j < n such thatA₂·. . .·A_j =p⁰₀ and A_j+1·. . .·A_n=p₁. Since p₀ =A₁·p⁰₀ =A₁·A₂·. . .·A_j we are done. 2 Proposition 7.4.8 For A∈M_ε and a pomsetp₀ 6=ε we have

A·q=p₀·p₁

⇓ ∃p⁰₀. A·p⁰₀ =p₀,q=p⁰₀ ·p₁

Proposition 7.4.9 Suppose p·q r₀ ×r₁. Then there exists p₀,p₁,q₀,q₁ such that pi·qi ri for i= 0,1 and pp₀×p₁ and qq₀×q₀.

Proof We prove it for lpos and the proposition follows immediately.

p·q r₀ ×r₁ means that there exists a bijection f : X_r0×r1 −→ X_p·q which also is a morphism of lpos.

By definition of · and × we have X_p·q ={0} ×X_p∪ {1} ×X_q and X_r0×r1 ={0} ×X_r0 ∪ {1} ×Xr₁. So define pi asp restricted to{x∈Xp | h0, xi ∈f({i} ×Xr_i)} for i= 0,1 and similar forq₀ and q₁.

p₀·q₀ r₀: Considerg :X_r0 −→X_p0·q0 given by g(x) =f(h0, xi). It is easy to see that g in- and surjective.

g order preserving: From f being order preserving and x ≤r₀ y ⇒ h0, xi ≤r₀×r₁ hy,0i we see f(h0, xi) ≤p·q f(h0, yi). f(h0, xi) is of the form hi, x⁰i and f(h0, yi) is of the form hj, y⁰i, so hi, x⁰i ≤p·q hj, y⁰i. According to the definition of ≤p·q then

(i= 0 =j, x⁰ ≤p y⁰) or (i= 1 =j, x⁰ ≤q y⁰) or (i= 0, j = 1)

In the case x⁰ ≤p y⁰ we have x⁰ ∈ X_p, so we must have x⁰ ∈X_p0. Also y⁰ ∈ X_p0. Similar considerations in the case x⁰ ≤q y⁰ leads us to:

(i= 0 =j, x⁰ ≤p₀ y⁰) or (i= 1 =j, x⁰ ≤q₀ y⁰) or (i= 0, j = 1) But then g(x) =f(h0, xi) = hi, x⁰i ≤p₀·q₀ hj, y⁰i=f(h0, yi) =g(y).

g is directly seen to be label preserving: `<sub>r0</sub>(x) = `_r0×r1(h0, xi) = `_p·q(f(h0, xi)) =

`_p0·q0(g(x)).

p₁·q₁ r₁: similar as above.

p p₀×p₁: Let g :X_p0×p1 −→ X_p be given by g(hi, xi) = x. This time it is easy to see that g is a morphism of lpos.

g injective: Assume hi, xi 6= hj, yi. We are done if x = y and i 6= j is impossible.

So suppose on the contrary x = y, i 6= j. Now hi, xi ∈ X_p0×p1 ⇒ x ∈ X_pi ⇒ h0, xi ∈

f({i}×X_ri)⇒ ∃hi, x⁰i ∈X_r0×r1.f(hi, x⁰i) =h0, xiand similarhj, xi ∈X_p0×p1 ⇒ ∃hj, x⁰⁰i ∈ X_r0×r1. f(hj, x⁰⁰i) = h0, xi. But since i 6= j and thereby hi, x⁰i 6= hj, x⁰⁰i this is a contra-diction to f being injective.

g surjective: x∈X_p ⇒ h0, xi ∈X_p·q ⇒(sincef is surjective) (∃hi, yi ∈X_r0×r1. f(hi, yi) = h0, xi) ⇒ (∃i ∈ {0,1}. x ∈ X_pi) ⇒ ∃i ∈ {0,1}.hi, xi ∈ X_p0×p1. From g(hi, xi) = x the result then follows.

qq₀×q₁: Similar as the last case. 2

Proposition 7.4.10 Ifn ≥1 andA₁,. . ., An ∈Mε andA₁·. . .·Anp₀×p₁ then there exists multisets A⁰₁,. . ., A⁰_n and A¹₁,. . ., A¹_n such thatA_j =A⁰_j ×A¹_j for j = 1,. . ., n, and Aⁱ₁·. . .·Aⁱ_np_i fori= 0,1.

Proof By induction on n.

n = 1: A₁ p₀×p₁ clearly implies p₀ and p₁ are multisets and A₁ =p₀×p₁. Chose A⁰₁ =p₀ and A¹₁ =p₁.

n >1: A₁ ·(A₂ ·. . .·A_n) p₀ ×p₁ implies by the previous proposition the existence of pomsets q₀,q₁,r₀,r₁ such that q₀ · r₀ p₀,q₁ · r₁ p₁, A₁ q₀ ×q₁ and A₂ ·. . .·A_n r₀ ×r₁. The last implies by hypothesis of induction that there are multisets A⁰₂,. . ., A⁰_n and A¹₂,. . ., A¹_n with A⁰₂ ·. . .·A⁰_n r₀, A¹₂·. . .·A¹_n r₁ and A⁰_i ×A¹_i =A_i for i= 2,. . ., n. From the casen = 1 we see that there existsA⁰₁ and A¹₁ with A⁰₁ q₀, A¹₁ q₁ and A₁ =A⁰₁×A¹₁. By monotonicity and transitivity of we now get

A⁰₁·(A⁰₂·. . .·A⁰_n)q₀·(A⁰₂·. . .·A⁰_n)q₀·r₀ p₀ and similar for the A¹_i’s.

2

In document View of Partial orders and fully abstract models for concurrency (Sider 163-173)