Information Technology Reference
In-Depth Information
It follows from (
3.13
)-(
3.15
) that
ʔ
([
s
]
≡
)
=
ʘ
([
s
]
≡
)
.
as we have desired.
Remark 3.2
Note that in the above proof the equivalence classes [
s
]
≡
are not nec-
essarily
R
-closed. For example, let
S
={
s
,
t
}
,
Id
S
={
(
s
,
s
), (
t
,
t
)
}
and the relation
≡=
R
∩
R
−
1
R
=
Id
S
∪{
(
s
,
t
)
}
. The kernel of
R
is
=
Id
S
and then [
s
]
≡
={
s
}
.We
have
[
s
]
≡
. So a more direct attempt to apply Theorem
3.5
(2) to those
equivalence classes would not work.
R
(
s
)
=
S
ↆ
Theorem 3.6
For reactive pLTSs,
coincides with
∼
.
Proof
It is obvious that
∼
is included in
. For the other direction, we show that
a
−ₒ
ʔ
. There exists a
is a bisimulation. Let
s
,
t
∈
S
and
s
t
. Suppose that
s
a
−ₒ
)
†
ʘ
. Since we are considering reactive probabilistic
transition
t
ʘ
with
ʔ
(
≺
a
−ₒ
systems, the transition
t
ʘ
from
t
must be matched by the unique outgoing
a
−ₒ
)
†
ʔ
. Note that by using Proposition
3.4
it is
transition
s
ʔ
from
s
, with
ʘ
(
≺
easy to show that
≺
is a preorder on
S
. It follows from Lemma
3.3
that
ʔ
(
C
)
=
ʘ
(
C
)
)
†
ʘ
. Therefore,
for any
C
∈
S/
. By Theorem
3.1
(2) we see that
ʔ
(
is indeed
a probabilistic bisimulation relation.
3.6
Logical Characterisation
Let
(
s
)
to stand for the set of formulae that state
s
satisfies. This induces an equivalence
relation on states:
s
L
be a logic and
S
,
L
,
ₒ
beapLTS.Forany
s
∈
S
, we use the notation
L
=
L
t
iff
(
t
). Thus, two states are equivalent when
they satisfy exactly the same set of formulae.
In this section we consider two kinds of logical characterisations of probabilistic
bisimilarity.
L
(
s
)
=
L
Definition 3.7
(Adequacy and Expressivity)
1.
L
is
adequate
with respect to
∼
if for any states
s
and
t
,
=
L
t
iff
s
s
∼
t.
2.
L
is
expressive
with respect to
∼
if for each state
s
there exists a
characteristic
formula ˕
s
∈
L
such that, for any state
t
,
t
satisfies
˕
s
iff
s
∼
t.
We will propose a probabilistic extension of the Hennessy-Milner logic, showing its
adequacy, and then a probabilistic extension of the modal mu-calculus, showing its
expressivity. In general the latter is more expressive than the former because it has
Search WWH ::
Custom Search