Information Technology Reference
In-Depth Information
Fig. 2.
An automaton and its incorrect reduction according to [3]
The idea is that in the beginning (
i
= 0) accepting states have colour 1 and non-
accepting states have colour 2, and in each step, the colour of a state is obtained
by its old colour and a combination of the successor state colours and the cor-
responding edge labels. This means that if two states have the same colour but
they differ in the colours of their successors (taking into account the edge labels),
then those two states must be distinguished; we say that the colouring is
refined
.
In the end, states with the same colour can be joined.
The algorithm initialises not only
C
0
but also
C
−
1
(we might call this “pre-
initialisation”) which is a trick making the formulation of the algorithm more
concise, by allowing for a loop condition that makes a comparison between the
current and the previous colouring, even for
i
=0.
However, our formalisation of the reduction algorithm, to be shown later, has
revealed that there is a mistake in this pre-initialisation. This is illustrated in
Figure 2. Here we have
Q
=
,F
=
Q,C
0
(
q
0) = 1
,C
0
(
q
1) = 1
,C
−
1
(
q
0) =
1
,C
−
1
(
q
1) = 1. Just before the
while
we have
{
q
0
,q
1
}
|
C
0
(
Q
)
|
|
C
−
1
(
Q
)
|
=
=1;even
stronger, we have
C
0
(
Q
)=
C
−
1
(
Q
)=
{
}
. What matters is that the loop
condition is false and hence the loop is not entered at all. Therefore the result
C
=
C
0
is computed, yielding the automaton shown on the right in Figure 2.
Our explanation is as follows: The pre-initialisation
∀q ∈ Q. C
−
1
(
q
):=1is
conceptually wrong. It expresses that “pre-initially” (
i
=
1
1), there is only one
colour. If by coincidence the input automaton has only accepting or only non-
accepting states, then “initially” (index
i
= 0), there is also just one colour. The
loop condition will then wrongly say “we have done enough refinement steps”.
The problem really manifests itself for the case that
F
=
Q
, i.e., all states are
accepting: each refinement step takes into account the edge labels and not just
whether a state is accepting or not. The initialisation however only considers
whether a state is accepting or not, and so not doing any refinement wrongly
results in identifying all states (
q
0and
q
1 in the example).
The conceptual mistake happens to cause no harm in the case
F
=
−
∅
,since
the initialisation of the algorithm establishes the property
F
=
and trivially
maintains it since no refinement is done. The accepted language is then empty.
Our solution is to replace the condition
∅
C
i
(
Q
)
C
i−
1
(
Q
)
|
|
=
|
|
with
i
≤
0
∨
C
i
(
Q
)
C
i−
1
(
Q
)
C
i
(
Q
)
C
i−
1
(
Q
)
|
|
=
|
|
(in the actual formalisation:
i>
0
−→ |
|
=
|
|
)
