Information Technology Reference
In-Depth Information
2. It is not the case that at least one coefficient is negative and the other coefficients are
either negative or 0. Otherwise, by summing up all the coefficients, we would get
ʔ
(
S
)
<
0
ʔ
(
S
)
−
that contradicts the assumption that
ʔ
and
ʔ
are distributions over
S
.
Therefore the only possibility is that all the coefficients in (
3.24
) are 0, that is
ʔ
(
V
i
)
ʔ
(
V
i
) for any equivalence class
V
i
∈
=
S/
R
. It follows from Theorem
3.1
†
ʔ
. So we have shown that
(2) that
ʔ
R
R
is indeed a bisimulation.
Corollary 3.2
Let s and t be two states in a finite state pLTS. Then s
∼
t if and
only if m
max
(
s
,
t
)
=
0
.
Proof
(
⃒
) Since
∼
is a bisimulation, by Theorem
3.11
there exists some state-metric
m
such that
s
∼
t
iff
m
(
s
,
t
)
=
0. By the definition of
m
max
we have
m
m
max
.
Therefore
m
max
(
s
,
t
)
≤
m
(
s
,
t
)
=
0.
(
⃐
) From
m
max
we construct a pseudometric
m
as follows.
⊧
⊨
0 f
m
max
(
s
,
t
)
=
0
m
(
s
,
t
)
=
⊩
1
otherwise
.
Since
m
max
is a state-metric, it is easy to see that
m
is also a state-metric. Now we
construct a binary relation
s
,
s
s
iff
m
(
s
,
s
)
R
such that
∀
:
s
R
=
0. It follows
from Theorem
3.11
that
R
is a bisimulation. If
m
max
(
s
,
t
)
=
0, then
m
(
s
,
t
)
=
0
and thus
s
R
t
. Therefore we have the required result
s
∼
t
because
∼
is the largest
bisimulation.
3.8
Algorithmic Characterisation
Bisimulation is useful for verifying formal systems and is the foundation of state-
aggregation algorithms that compress models by merging bisimilar states. State
aggregation is routinely used as a preprocessing step before model checking [
58
]. In
this section we present two algorithms for computing probabilistic bisimulation.
3.8.1
A Partition Refinement Algorithm
We first introduce an algorithm that, given a pLTS (
S
,
L
,
) where both
S
and
L
are
finite, iteratively computes bisimilarity. The idea is originally proposed by Kanellakis
and Smolka [
59
] for computing nonprobabilistic bisimulation and commonly known
as a
partition refinement
algorithm (see Fig.
3.6
). The point is to represent the state
space as a set of
blocks
, where a block is set of states standing for an equivalence
class, and the equivalence of two given states can be tested by checking whether
ₒ
Search WWH ::
Custom Search