Information Technology Reference
In-Depth Information
partition
we mean a set
M
consisting of pairs (
a
,
M
) where
a
∈
L
and
M
ↆ
M
a
with
M
a
=
s
∈
S
{
a
−ₒ
ʔ
|
s
ʔ
}
such that, for any action
a
, the set
{
M
|
(
a
,
M
)
∈
M
}
is
a partition of the set
M
a
.
The algorithm works as follows. We skip the first refinement step and start with
the state partition
a
−ₒ}={
a
−ₒ}
B
init
=
S/
∼
L
where
s
∼
L
t
iff
{
a
|
s
a
|
t
that identifies those states that can perform the same actions immediately. The initial
transition partition
M
init
={
|
∈
}
(
a
,
M
a
)
a
L
identifies all transitions with the same label. In each iteration, we try to refine the
state partition
B
according to an equivalence class (
a
,
M
)of
M
or the transition
partition
M
according to a block
B
∈
B
. The refinement of
B
by (
a
,
M
) is done
by the operation
Split
(
M
,
a
,
B
) that divides each block
B
of
B
into two subblocks
a
−ₒ
M
}
B
(
a
,
M
)
={
s
∈
B
|
s
and
B
\
B
(
a
,
M
)
. In other words,
Split
(
M
,
a
,
B
)
=
Split
(
M
,
a
,
B
)
B
∈
B
a
−ₒ
where
Split
(
M
,
a
,
B
)
={
B
(
a
,
M
)
,
B
\
B
(
a
,
M
)
and
B
(
a
,
M
)
={
s
∈
B
|
s
M
}
. The
refinement of
M
by
B
is done by the operation
Split
(
B
,
M
) that divides any block
(
a
,
M
)
∈
M
by the subblocks (
a
,
M
1
),
...
,(
a
,
M
n
) where
{
M
1
,
...
,
M
n
}=
M/
∼
B
and
ʔ
∼
B
ʘ
iff
ʔ
(
B
)
=
ʘ
(
B
). Formally,
Split
(
B
,
M
)
=
Split
(
B
,(
a
,
M
))
(
a
,
M
)
∈
M
(
a
,
M
)
M
∈
where
Split
(
B
,(
a
,
M
))
={
|
M/
∼
B
}
. If no further refinement of
B
and
. The algorithm is sketched in Fig.
3.9
.
See [
26
] for the correctness proof of the algorithm and the suitable data structures
used to obtain the following complexity result.
M
is possible then we have
B
=
S/
∼
Theorem 3.13
The bisimulation equivalence classes of a pLTS with n states and
m transitions can be decided in time
O
(
mn
( log
m
+
log
n
))
and space
O
(
mn
)
.
3.8.2
An “On-the-Fly” Algorithm
We now propose an “on-the-fly" algorithm for checking whether two states in a
finitary pLTS are bisimilar.
An important ingredient of the algorithm is to check whether two distributions are
related via a lifted relation. Fortunately, Theorem
3.4
already provides us a method
Search WWH ::
Custom Search