Information Technology Reference
In-Depth Information
s
s'
a
a
a
a
1/2
1/2
1/2
1/2
1/2
1/2
1/2
1/2
t
u
v
w
t
v
u
w
b
c
d
e
b
d
c
e
(a)
(b)
Fig. 3.8
Nonbisimilar states
s
(
a
) and
s
(
b
)
The Partitioning Technique for Reactive pLTSs
Let
S
,
L
,
ₒ
be a reactive pLTS.
For any
a
∈
L
and
B
ↆ
S
, we define the equivalence relation
∼
(
a
,
B
)
by letting
a
−ₒ
a
−ₒ
s
ʘ
(
B
). We still use the schema
shown in Fig.
3.6
and the refinement operator in (
3.25
), but change the splitting
procedure as follows
∼
(
a
,
B
)
t
if
s
ʔ
and
t
ʘ
with
ʔ
(
B
)
=
Split
(
B
,
a
,
B
)
=
Split
(
B
,
a
,
C
) where
Split
(
B
,
a
,
C
)
=
C/
∼
(
a
,
B
)
.
(3.26)
C
∈
B
An implementation of the algorithm using some tricks on data structures yields the
following complexity result.
Theorem 3.12
The bisimulation equivalence classes of a reactive pLTS with n states
and m transitions can be computed in time
The splitter technique in (
3.26
) does not work for general pLTSs when we use the
obvious modification of the equivalence relation
O
(
mn
log
n
)
and space
O
(
mn
)
.
∼
(
a
,
B
)
where
s
∼
(
a
,
B
)
t
iff for any
a
−ₒ
a
−ₒ
transition
s
ʔ
there is a transition
t
ʘ
with
ʔ
(
B
)
=
ʘ
(
B
) and vice versa.
s
because the
Example 3.2
Co
n
sider the pLTS described in Fig.
3.8
,wehave
s
∼
a
−ₒ
2
u
cannot be matched by any transition from
s
. However,
s
and
s
cannot be distinguished by using the above partitioning technique. The problem
is that after one round of refinement, we obtain the blocks
1
1
transition
s
2
t
+
s
,
s
}
{
,
{
t
}
,
{
u
}
,
{
v
}
,
{
w
}
{
s
,
s
}
and then no further refinement can split the block
.
The Partitioning Technique for pLTSs
To compute bisimulation equivalence
classes in general pLTSs, we can keep the schema sketched in Fig.
3.6
but use two
partitions: a partition
B
for states and a partition
M
for transitions. By a
transition
Search WWH ::
Custom Search