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