The first relation on pomsets we are going to present is used to compare the “concurrency”
of two pomsets.
Definition 6.2.1 -ordering on Pomsets
The preorder, , on lpos is defined: p q iff there exists bijective functionXq −→ Xp which also is a morphism of lpos.
This preorder induce a partial order, ambiguously denoted , on pomsets as follows:
p q iff pq
p q can be read: the pomset p is smoother than [Gra81]/ subsumed by [Gis88]/less
nonsequential than the pomset q. 2
Notice that for lpos pand q, pq does not imply p∼=q. It is also useful to observe that pq impliesmp=mq.
Example: a -b -c a c
PPq
1b a-b
c and a
>b
cZ-Z~d a -b c -d The -downwards closure of a pomset p,{p0 ∈P|p0 p}, is denoted δ(p).
Suppose P∗ is a property of pomsets then δ∗(p) will be a shorthand for the semi -downwards closure {p0 ∈ P | p0 p and P∗(p0)}. E.g., δw(p) = {p0 ∈ P | p0 p and Pw(p0)}={p0 ∈W | p0 p}. Though we might have p 6∈δ∗(p) for some pomset property P∗, we call it the δ∗-closure.
From the definition of p.ref. we directly see:
Proposition 6.2.2 Let lpos p and q be given with q =hXp,≤q, `pi and ≤q ⊆ ≤p. Fur-thermore suppose π and π0 are p.ref.’s for both p and q (Xp = Xq) such that ∀x ∈ Xp. Xπ0(x) =hXπ(x),≤, `π(x)i,≤ ⊆ ≤π(x). Then
p<π>q<π>
p<π>p<π0>
The following alternative characterization of will often be more convenient to work with.
Proposition 6.2.3 For pomsets p and qwe have:
a) pq iff p=hXq0,≤p, `q0i and ≤p ⊇ ≤q0 for someq0 ∈q b) pq iff hXp0,≤q, `p0i=q and ≤p0 ⊇ ≤q for somep0 ∈p
Proof Observe at first that in general pq ∼=r⇒pr and p∼=qr ⇒pr.
a) if: idXq0 is a label preserving bijective function fromXq0 to Xp because Xp =Xq0 and
`p = `q0. By ≤p ⊇ ≤q0 it is also order preserving. Hence p q0 and since q0 ∈ q means q0 ∼=q we get pq and so pq.
only if: By definition p q implies the existence of a bijective function f :Xq −→ Xp which also is a morphism of lpos. Then define q0 to be hXp,≤q0, `pi where≤q0 is given by
x≤q0 y iff f−1(x)≤q f−1(y)
Clearlyq0 ∼=qand q0 ∈q. Also p=hXq0,≤p, `q0i so it remains to show≤q0 ⊆ ≤p. Assume x ≤q0 y. Then f−1(x) ≤q f−1(y) by definition of q0 and because f is bijective and a morphism of lpos therefore x=f ◦f−1(x)≤p f◦f−1(y) =y.
b) is proved similar. 2
With the alternative characterization of , proposition 6.2.2 above and the observations made by the definition of particular refinement we get:
(6.2) · and × are -monotone in their left and right arguments Similar we with appropriate p.ref.’s deduce from the above example that:
(p×q)·(p0×q0)(p·p0)×(q·q0) (6.3)
We now turn to the second partial order on pomsets.
Definition 6.2.4 v-ordering on Pomsets
Given two pomsets p and q. Then p is a prefix of q, pvq, if pis a subpomset of qand the elements of p only dominates the elements of p inq. Formally:
The lpo preorder, v, is definedpvq iff there exists a ≤q-downwards closed set Y such that p is isomorphic to the restriction of q to Y. I.e.,
pvq iff ∃Y. p∼=q|Y and {x∈Xq | ∃y∈Y. x≤q y} ⊆Y The partial order,v ⊆P×P, is induced from the lpo preorder by:
pvq iff pvq
π is defined to be the function which for a pomsetp gives the v-downwards closure ofp:
π(p) ={p0 ∈P|p0 vp}. 2
That p v q implies p ,→ q follows from p∼= q|Y. Notice that p v p and p v q implies mp ≤mq. Also observe that {x∈Xq | ∃y∈Y. x≤q y} ⊆Y just is a formalization of: Y is ≤q-downwards closed.
Example: a1b
PPqc v a1b
PPqc
PPq
1d , but a-b-d 6v a1b
PPqc
PPq 1d
As for the partial order there is an alternative characterization of v: Proposition 6.2.5 For pomsets p and qwe have:
a) pvq iff p0 =q|Xp0 for some p0 ∈p with {x∈Xq | ∃y∈Xp0. x≤q y} ⊆Xp0
b) pvq iff p=q0|Xp for some q0 ∈q with {x∈Xq0 | ∃y∈Xp. x≤q0 y} ⊆Xp Proof a), b)if: Immediate because =⊆ ∼=.
For the only if direction of a) and b) we by definition have
∃Y. p∼=q|Y and {x∈Xq | ∃y ∈Y. x≤q y} ⊆Y W.l.o.g. we can assume Y ⊆Xq (because q|Y =q|(Xq∩Y)).
a) only if: Define p0 to be q|Y. Obviously p0 is a representative of p and because Y is a subset of Xq we have Y =Xq|Y =Xp0. Hence p0 =q|Y =q|Xp0 and Xp0 is ≤q-downwards closed.
b)only if: Here we shall find a representative of qwhich pis a part of. The idea will be to find a representative q00 of q which has no elements in common with p and then just replace that part of q00 which is isomorphic to p with p to obtain q0. The elements of p are from the ground set which are composed of two-tuples. Clearly the “size”, |x|, of an element x can be determined as follows
|x|=
(|x0|+|x1| if x=hx0, x1i
1 otherwise (x∈IN or x∈∆)
Ifpis empty we can just chooseq0 =qso assume it is not. Then since we work with finite pomsets/ lpos it make sense choose a z ∈Xp with maximal size according to the measure above. Define q00 =hX,≤, `iwhere
X is the set {hx, zi |x∈Xq}
≤ is the partial order defined by hx, zi ≤ hy, zi iff x≤q y
` is the function hx, zi 7→`q(x)
Evidently q00 is a representative of q and p is a lpo isomorphic to q00|Yz where Yz is the
≤q00-downwards closed set {hx, zi |x∈Y}. By construction all elements of Xq00 have size greater than those ofXp and so they cannot have any elements in common. The required q0 is then obtained by replacing all elements from Xq00 which under the lpo isomorphism equals the elements ofXp with these corresponding elements ofXp. 2 With this alternative characterization it is useful to observe for lpos pand q:
• {0} ×Xp =Xp·ε=Xp×ε and {1} ×Xp =Xε·p =Xε×p
• Y ⊆Xp·ε implies (p·q)|Y = (p·ε)|Y
• Xp·ε⊆Y implies (p·q)|Y ∼=p·(ε·q)|Y
• Y ⊆Xp×ε implies (p×q)|Y = (p×ε)|Y (symmetric for ε×p)
• Xp×ε⊆Y implies (p×q)|Y ∼=p×(ε×q)|Y (symmetric for ε×p)
Then evidently a pomset is a prefix of two parallel composed pomsets iff it itself is the parallel composition of two prefixes of the two parallel composed pomsets. It is also easy to see pvqimpliesp vq·randr·pvr·q. It takes more effort to prove the “reverse”:
Proposition 6.2.6 If pvq·r then either pv qor there exists a pomsets r0 such that p=q·r0 and r0 vr.
Proof Let p0,q and r be given such that p0 vq·r. q·r= [q·r] so by the alternative characterization of prefix we know there is a representative pofp0 such thatp= (q·r)|Xp
and Xp is≤q·r-downwards closed.
IfXp ⊆ {0}×Xqthen as observedp= (q·r)|Xp = (q·ε)|Xp. Of courseXpis≤q·ε-downwards closed and by the alternative characterization of prefix then p0 =pv[q·ε] =q.
So assume Xp 6⊆ {0} ×Xq. We show at first {0} ×Xq ⊆ Xp. Let an x ∈ {0} ×Xq be given. Fromp= (q·r)|Xp we have Xp ⊆ {0} ×Xq∪ {1} ×Xr, so because Xp 6⊆ {0} ×Xq there must be a y of Xp in {1} ×Xr. By definition of q·r then x ≤q·r y wherefore the
≤q·r-downwards closure of Xp yields x ∈Xp. Now since Xε·q = {0} ×Xq ⊆ Xp we have p ∼= (q·r)|Xp ∼= q·(ε·r)|Xp. That Xp is ≤ε·r-downwards closed is a simple consequence of Xε·r ⊆ Xq·r and the ≤q·r-downwards closure of Xp. Defining r0 = (ε ·r)|Xp we get r0 v [ε·r] = ε·r = r by using the alternative characterization of prefix again. From p0 3p= (q·r)|Xp ∼=q·(ε·r)|Xp =q·r0 then p0 = [q·r0] = q·r0 as desired. 2 The next proposition will prove extremely useful in proving various connections between the two partial orders over pomsets.
Proposition 6.2.7 Given two pomsets p and q. Then pvq⇒ ∃r∈P.p·rq
Proof Assume p v q. By the alternative characterization of prefix we can find a representative p0 of p such that p0 =q|Xp0 and Xp0 is ≤q-downwards closed. Define r to be q|(Xq\Xp0) and q0 =hX,≤, `i, where
X is the set {0} ×Xp0 ∪ {1} ×(Xq\Xp0)
≤ is the partial order defined by hi, xi ≤ hj, yi iff x≤q y
` is the function hi, xi 7→`q(x)
Clearly q0 ∼= q—i.e., q0 is a representative of q, and from the definition of p0, r and lpo sequential composition we see Xp0·r = Xq0 and `p0·r = `q0. To see ≤q0 ⊆ ≤p0·r assume hi, xi ≤ hj, yi. Then x ≤q y and if i = 0 =j we have x, y ∈ Xp0 so x ≤p0 y then follows from ≤p0 = ≤q|Xp02. Similar if i = 1 = j. If i = 0 and j = 1 then hi, xi ≤p0·r0 hj, yi by the definition of p0·r. We are left with the case i= 1 and j = 0. This is meansx ≤q y, x∈Xq\Xp0 and y∈Xp0—but this is impossible because Xp0 is≤q-downwards closed and we can exclude this case. So we actually have q0 =hXp0·r,≤q0, `p0·ri and ≤p0·r ⊇ ≤q0. The alternative characterization of then gives usp0·r= [p0 ·r]q0 =q as we wanted. 2 With this result it is easy to prove:
Proposition 6.2.8 For pomsets p and qwe have
∃r.pr vq iff ∃s.p vsq
In [Pra86, page 49] Pratt outlines an alternative proof. He defines prefix in another, but equivalent way: p is a prefix ofqif ∃Y. p∼=q|Y and Xq\Y is ≤q-upwards closed. So this proposition can be seen as just a reformulation of his theorem.
Proof only if: Assume p r v q. By the previous proposition we know there is a pomset r0 such thatr·r0 q. From p r and -monotonicity of · then p·r0 q. But pvp·r0 so we can just choose s=p·r0.
if: Suppose pv sq. Then there are representatives p0 and q0 of p and qrespectively such that p0 = s|Xp0, Xp0 is ≤s-downwards closed and q0 = hXs,≤q0, `si with ≤s ⊇ ≤q0.
Sets of pomsets and operators on them are used extensively in the models we shall present, so we briefly treat them here. The two operations on pomsets·and×generalize to sets in the natural way e.g., P·Q={p·q|p∈P,q∈Q}. We shall use∪ to denote the normal set union and P( ) the powerset operator. Also for a pomset property P∗, δ∗ generalize to sets: δ∗(Q) =Sq∈Qδ∗(q).
The previously mentioned refinement operator for pomsets is defined using the particular refinement construction for lpos.
Definition 6.3.1 Refinements
A P(P)-refinement is a mapping %: ∆−→ P(P).
We say that a P(P)-refinement, %, is ε-free iff ∀a∈ ∆. ε 6∈%(a) and % is image finite if %(a) is finite for every a∈∆.
A particular refinement πp for a lpo pis consistent with aP(P)-refinement % iff
∀x∈Xp.[πp(x)]∈%(`p(x))
The mapping associated with % is now defined as <%> : P −→ P(P) with p<%> = {[p<πp>]|πpis a%-consistent p.ref. forp}and generalized to sets of pomsets byP <%> =
Sp∈Pp<%>.
For a finite lpo pand image finite refinement %we notice that there is only finitely many different %-consistent p.ref. for p (up to ∼= in each x ∈ Xp) and consequently in general p<%> is a finite set of pomsets because we only work with finite pomsets. Also P <%>
must be finite ifP is a finite set of pomsets and % is a image finite refinement.
Example: Consider the same pomset as in the example for particular refinement on page 135. Suppose % is a P(P)-refinement such thata 7→
(b