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