Information Technology Reference
In-Depth Information
Definition 6.28 (Simulation Preorder) Define
S
to be the largest relation in
( i p i ʔ i ), for finitely
ʱ
D
( S )
× D
( S ) such that if ʔ S ʘ then whenever ʔ
many p i with i p i =
( i p i ʘ i ) and ʔ i S ʘ i
ʱ
1, there are ʘ i
with ʘ
for
each i .
Note that, unlike for Definition 6.28 , this summation cannot be empty.
Again it is trivial to see that
S is reflexive and transitive; and again it is sometimes
easier to work with an equivalent formulation based on a state-level “simulation”
defined as follows.
Definition 6.29 (Simulation) Define
s to be the largest relation in S
× D
( S ) such
ʱ
−ₒ
ʱ
ʔ there is some ʘ such that ʘ
ʘ and
that if s
s ʘ then whenever s
ʔ (
s ) ʘ .
Remark 6.5 Definition 6.29 entails the same simulation given in Definition 5.4 when
applied to finite processes. It differs from the analogous Definition 6.21 in three ways:
it is missing the clause for divergence, and for refusal; and it is (implicitly) limited
to
ʱ
-transitions that simulate by producing full distributions only. 2 Without that
latter limitation, any simulation relation could be scaled down uniformly without
losing its simulation properties, for example, allowing counter-intuitively a. 0 to be
simulated by a. 0 2
ʵ .
Lemma 6.43 The above preorder and simulation are equivalent in the following
sense: for distributions ʔ , ʘ we have ʔ
S ʘ just when there is a distribution ʘ match
s ) ʘ match .
Proof The proof is as for the failure case, except that in Theorem 6.12 we can assume
total distributions, and so do not need the second part of its proof where divergence
is treated.
ʘ match
with ʘ
and ʔ (
6.8.1
Soundness
In this section, we prove that simulations are sound for showing that processes are
related via the may-testing preorder. We assume initially that we are using only one
success action ˉ , so that
1.
Because we prune our pLTS s before extracting values from them, we will be
concerned mainly with ˉ -respecting structures, and for those we have the following.
Lemma 6.44
|
ʩ
|=
Let ʔ and ʘ be two distributions. If ʔ is stable and ʔ (
s )
ʘ,
then
V
( ʔ )
Ho V
( ʘ ) .
Proof
We first show that if s is stable and s s ʘ then
V
( s )
Ho V
( ʘ ). Since s is
stable, we have only two cases:
2
Even though for simplicity of presentation in Definition 6.2 the relation
−ₒ
was defined by using
subdistributions, it can be equivalently defined by using full distributions.
 
Search WWH ::




Custom Search