Information Technology Reference
In-Depth Information
Proposition 5.3
S
and
FS
are preorders, i.e. they are reflexive and transitive.
Proof
By combination of Lemma
5.6
and Proposition
5.2
, we obtain that
S
is a
preorder. The case for
FS
can be similarly established by proving the counterparts
of Lemma
5.6
and Proposition
5.2
.
5.5.2
The Simulation Preorders are Precongruences
In Theorem
5.1
of this section we establish that the
pCSP
operators are monotone
with respect to the simulation preorders, i.e. that both
FS
are precongru-
ences for
pCSP
. This implies that the
pCSP
operators are compositional for them
or, equivalently, that
S
and
FS
are congruences for
pCSP
. The following two
lemmas gather some facts we need in the proof of this theorem. Their proofs are
straightforward, although somewhat tedious.
S
and
Lemma 5.7
˄
⃒
˄
⃒
˄
⃒
Φ
, then Φ
Φ
Φ
.
(i) If Φ
ʔ
ʔ and ʔ
Φ
ʔ
a
−ₒ
a
−ₒ
a
−ₒ
Φ
, then Φ
Φ
and ʔ
Φ
.
(ii) If Φ
ʔ
Φ
(iii)
(
j
∈
J
p
j
·
(
k
∈
K
q
k
·
=
j
∈
J
k
∈
K
(
p
j
·
Φ
j
)
ʔ
k
)
q
k
)
·
(
Φ
j
ʔ
k
)
.
R
ↆ
R
ʔ when-
(iv) Given two binary relations
R
,
sCSP
×
D
(
sCSP
)
satisfying s
†
ʔ
i
ever s
=
s
1
s
2
and ʔ
=
ʔ
1
ʔ
2
with s
1
R
ʔ
1
and s
2
R
ʔ
2
. Then Φ
i
R
R
†
for i
=
1, 2
implies
(
Φ
1
Φ
2
)
(
ʔ
1
ʔ
2
)
.
Lemma 5.8
˄
⃒
˄
⃒
˄
−ₒ
(i) If Φ
Φ
, then Φ
|
A
ʔ
Φ
|
A
ʔ and ʔ
|
A
Φ
ʔ
|
A
Φ
.
a
−ₒ
a
−ₒ
a
−ₒ
Φ
and a
Φ
|
A
ʔ and ʔ
|
A
Φ
.
(ii) If Φ
∈
A, then Φ
|
A
ʔ
|
A
Φ
ʔ
a
−ₒ
a
−ₒ
˄
−ₒ
Φ
, ʔ
ʔ
and a
ʔ
|
A
Φ
.
(iii) If Φ
∈
A, then ʔ
|
A
Φ
(iv)
(
j
∈
J
p
j
·
Φ
j
)
|
A
(
k
∈
K
q
k
·
ʔ
k
)
=
j
∈
J
k
∈
K
(
p
j
·
q
k
)
·
(
Φ
j
|
A
ʔ
k
)
.
R
ↆ
R
ʔ when-
(v) Let
R
,
sCSP
×
D
(
sCSP
)
be two binary relations satisfying s
ever s
=
s
1
|
A
s
2
and ʔ
=
ʔ
1
|
A
ʔ
2
with s
1
R
ʔ
1
and s
2
R
ʔ
2
. Then Φ
i
R
†
ʔ
i
R
†
for i
=
1, 2
implies
(
Φ
1
|
A
Φ
2
)
(
ʔ
1
|
A
ʔ
2
)
.
Theorem 5.1
Let
∈{
S
,
FS
}
. Suppose P
i
Q
i
for i
=
1, 2
. Then
1. a.P
1
a.Q
1
2. P
1
P
2
Q
1
Q
2
3. P
1
P
2
Q
1
Q
2
4. P
1
p
↕
P
2
Q
1
p
↕
Q
2
5. P
1
|
A
P
2
Q
1
|
A
Q
2
.
Search WWH ::
Custom Search