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