Information Technology Reference
In-Depth Information
Fig. 3.6 Schema for the partition refinement algorithm
Fig. 3.7 Splitting a block
they belong to a same block. The blocks form a partition of the state space. Starting
from the partition
, the algorithm iteratively refines the partition by splitting each
block into two smaller blocks if two states in one block are found to exhibit different
behaviour. Eventually, when no further refinement is possible for a partition, the
algorithm terminates and all states in a block of the partition are bisimilar.
Let
{
S
}
B ={
B 1 , ... , B n }
be a partition consisting of a set of blocks. The algorithm
tries to refine the partition by splitting each block. A splitter for a block B
B
is
the block B B
L , into B
and others do not. In this case B splits B with respect to a into two blocks B 1 and
B 2 , where B 1 ={
such that some states in B have a -transitions, for a
a
−ₒ
s
B : s
s }
s
B
|∃
and B 2 =
B
B 1 . This is illustrated
in Fig. 3.7 .
The refinement operator Refine (
B
) yields the partition
B
=
B
Refine (
)
Split ( B , a ,
)
(3.25)
B
B
, a
L
where Split ( B , a ,
B
) is the splitting procedure that detects whether the partition
B
with respect to action a L . If such
splitter exists, B is split into two blocks B 1 and B 2 . Otherwise, B itself is returned.
We will introduce a partition refinement algorithm for pLTSs that was presented
in [ 26 ]. Before that we briefly sketch how the above partitioning technique can be
modified for reactive pLTSs and explain why this method fails for general pLTSs.
contains a splitter for a given block B B
 
Search WWH ::




Custom Search