Information Technology Reference
In-Depth Information
T
2
=(
{
q
0
,
q
1
,
q
2
,
q
3
}, {
B
}, {
a
,
b
,
c
}, {
a
,
b
},
μ
2
,
q
0
, {
q
3
}
)
,
where
a
−→
(
a
/
ba
−→
(
a
/
b
ba
−→
(
/
A
2
μ
1
=
{
(
p
0
,
A
)
p
1
,
A
)
,
(
p
1
,
A
)
p
1
,
)
,
(
p
1
,
A
)
p
2
,
ε
)
,
b
/
ε
−→
(
c
/
a
−→
(
ε
/
ε
−→
(
(
p
2
,
A
)
p
2
,
ε
)
,
(
p
2
,
A
)
p
3
,
A
)
,
(
p
3
,
A
)
p
3
,
ε
)
}
and
a
2
−→
(
ab
−→
(
a
/
/
ε
−→
(
b
ε
/
B
2
=
{
(
,
)
,
)
,
(
,
)
,
ε
)
,
(
,
)
,
ε
)
,
μ
q
0
B
q
0
q
0
B
q
1
q
1
B
q
2
2
/
ε
−→
(
b
/
ε
−→
(
c
(
q
2
,
B
)
q
2
,
ε
)
,
(
q
2
,
B
)
q
3
,
ε
)
}.
Successive application of branching steps yields an intermediate tree containing
early nodes numbered
1
in Fig. 2 (a) and (b). When
19
(
A
3
B
2
-
19
p
3
,
)
≡
(
q
3
,
)
in
Fig. 2 (b) is visited, stack reduction is applied to yield its son
20
(
A
3
p
3
,
)
≡
(
q
3
,
B
)
.
And then, when
22
(
A
4
B
5
p
1
,
·
A
)
≡
b
(
q
0
,
·
B
)
is visited first, skipping is applied with
respect to
15
(
A
4
B
5
to yield skipping-ends
23
(
p
1
,
)
≡
b
(
q
0
,
)
p
3
,
A
·
A
)
≡
(
q
3
,
ε
·
B
)
A
4
B
5
and
24
(
. When the same node
26
(
is
visited again afterwards, the tree is not changed any more by this step. Then the
algorithm halts with the correct conclusion that “
T
1
≡
p
3
,
ε
·
A
)
≡
(
q
3
,
B
·
B
)
p
1
,
·
A
)
≡
b
(
q
0
,
·
B
)
T
2
”. (In fact, TRANS
(
T
1
)=
a
i
b
j
c
i
a
2
(
)=
{
/
(
)
|
>
≥
}
TRANS
T
2
ab
i
j
1
.)
By using the proof similar to Ref. [10], we have the following theorem.
Theorem 1.
For the given two droct's which accept by final state, our equivalence
checking algorithm halts in a polynomial-time with respect to the cardinalities of
states, input symbols, output symbols, and transition-output rules with the correct
conclusion.
5
Conclusions
By extending the technique in Ref. [10], we have presented an algorithm for check-
ing the equivalence of non-real-time droct's (i.e. droct's with possible
-moves)
which accept by final state. The worst-case time complexity of our algorithm is
polynomial with respect to the description length of these droct's.
ε
Acknowledgements.
This work was supported in part by Grants-in-Aid for Scientific Re-
search Nos.20500007 and 23500011 from the MEXT of Japan.
References
1. Higuchi, K., Tomita, E., Wakatsuki, M.: A polynomial-time algorithm for checking the
inclusion for strict deterministic restricted one-counter automata. IEICE Trans. Inf. &
Syst. E78-D(4), 305-313 (1995)
2. Higuchi, K., Wakatsuki, M., Tomita, E.: A polynomial-time algorithm for checking the
inclusion for real-time deterministic restricted one-counter automata which accept by
final state. IEICE Trans. Inf. & Syst. E78-D(8), 939-950 (1995)
3. Senizergues, G.: L(A)=L(B)? decidability results from complete formal systems. Theo-
ret. Comput. Sci. 251(1-2), 1-166 (2001)
Search WWH ::
Custom Search