Information Technology Reference
In-Depth Information
Our first task is to show that the interpretation of the logic is consistent with the
operational semantics of processes.
F ʔ.
Theorem 6.15
If ʘ
FS ʔ then ʘ
Proof
We must show that if ʘ
FS ʔ then whenever ʔ
|=
˕ we have ʘ
|=
˕ . The
proof proceeds by induction on ˕ :
The case when ˕
=
is trivial.
Suppose ˕ is div . Then ʔ
|=
div means that ʔ
ʵ and we have to show
ʘ
ʵ , which is immediate from Lemma 6.20 .
a
ʔ for some ʔ that satisfies
Suppose ˕ is
a
˕ a . In this case we have ʔ
ʔ |=
˕ a . The existence of a corresponding ʘ is immediate from Definition 6.19
Case 1 and the induction hypothesis.
The case when ˕ is ref ( X ) follows by Definition 6.19 Clause 2, and the case ˕ 1
˕ 2
by induction.
When ˕ is ˕ 1 p
˕ 2 we appeal again to Definition 6.19 Case 1, using ʱ :
=
˄ to
infer the existence of suitable ʘ 1 and ʘ 2 .
We proceed to show that the converse to this theorem also holds, so that the failure
simulation preorder
F .
The idea is to mimic the development in Sect. 5.7, by designing characteristic
formulae that capture the behaviour of states in a pLTS. But here the behaviour is not
characterised relative to
FS coincides with the logical preorder
FS , but rather to the sequence of approximating relations
FS .
Definition 6.27
, the k th characteristic formulae
˕ s , ˕ ʔ of states s S and subdistributions ʔ D sub ( S ) are defined inductively as
follows:
In a finitary pLTS
S , Act ˄ ,
˕ s =
and ˕ ʔ =
,
˕ k + 1
s
=
div , provided s
ʵ ,
a
s
˄
˕ k + 1
s
˕ ʔ where X
=
ref ( X )
−ₒ ʔ
a
={
a
Act
|
s
−ₒ}
, provided s
−ₒ
,
a
= s
˕ ʔ s
˕ k + 1
s
ʔ ˕ ʔ otherwise,
ʔ
a
a
−ₒ
˄
−ₒ
( s ʔ
and ˕ k + 1
ʔ
ʔ ( s )
| ʔ | ·
˕ k + 1
s
=
( div ) 1 −| ʔ |
) .
˕ s and
Lemma 6.37
For every k
0 , s
S and ʔ
D sub ( S ) we have s
|=
˕ ʔ .
ʔ
|=
Proof
0 being trivial. The inductive case
of the first statement proceeds by an analysis of the possible moves from s , from
which that of the second statement follows immediately.
By induction on k , with the case when k
=
Lemma 6.38
Fo r k
0 ,
FS ʘ,
|=
˕ s implies s
(i) ʘ
˕ ʔ implies ʘ
FS ) ʘ match ,
(ii) ʘ
|=
ʘ match
such that ʔ (
(iii) ʘ |= ˕ ʔ implies ʘ
FS ʔ.
 
Search WWH ::




Custom Search