A Polynomial-Time Algorithm for Checking the Equivalence of Deterministic Restricted One-Counter Transducers Which Accept by Final State - Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing - page 132

w 1
=== ⇒
T 1

w /

, α ) (ii) If we have, in addition to (i), another pair of derivations ( q 01 , Z 01 ) ( p

w 2
=== ⇒
T 2

w /

, β ) , α ) = , β ) = 0 for some w ∈ Σ ∗ ,

with L ( p 0 and ( q 02 , Z 02 ) ( p with L ( p

w 1 , w 2 ∈ Δ ∗ such that w 1 h = w 2 for some h ∈ Δ ±∗ , α ∈ Γ 1 , β ∈ Γ 2 , and hence

, α ) ≡ h ( , β ) h .

( p p ,thenh =

Proof. These properties can be easily derived from Definitions 5, 6, and 8, and
Lemma 1 (ii).

∈ Δ ±∗ in eq.(3) and eq.(4) is to compensate the difference between
the two outputs, and is called an output compensating part . From Proposition 1 (ii),
the output compensating part is unique for each equivalence equation as eq.(4) when
T 1 ≡

The above h

T 2 .

4 The Equivalence Checking Algorithm

The equivalence checking is carried out by developing step by step the so-called
comparison tree as in Refs. [5]-[7].
At the initial stage, the comparison tree contains only the root labeled ( q 01 , Z 01 ) ≡

( whichissaidtobein unchecked status. In each step, the algorithm con-

siders a node labeled

q 02 , Z 02 )

( p , α ) ≡ h ( p , β ) such that eq.(1) and eq.(2) with eq.(3) for

w 2 ∈ Δ ∗ , and tries to prove or disprove this equivalence. In the
case where FIRST live (

∈ Σ ∗ , w 1 ,

some w

p , α )= FIRST live ( p , β )= { ε } and both ( p , α ) and ( p , β ) are

not in ε -mode, if h = ε then we turn the node to be in checked status. Otherwise,

i.e. h T 2 ”. Also, if another internal node with the same

label has appeared elsewhere in the tree, then we turn the above node to be checked .
From Proposition 1 (ii), if another internal node labeled

= ε , conclude that “ T 1 ≡

, α ) ≡ h ( , β )

( p p such that

h = T 2 ”. Otherwise,

we expand it by branching , skipping ,or stack reduction , which will be described
below.

h has appeared elsewhere in the tree, then conclude that “ T 1 ≡

4.1 Branching

Branching is a basic step of developing the comparison tree. The following branch-
ing step is almost the same as in [10] but some extensions.

Lemma 3. The equivalence equation eq.(4) holds iff the following conditions (i), (ii)
and (iii) hold.
(i) FIRST live ( p , α )= FIRST live ( p , β ) .

(ii) (a) In case both ( p , α ) and ( p , β ) are in reading mode, for each a i ∈

FIRST live ( p , α ) −{ ε } = { a 1 , a 2 ,..., a l }⊆ Σ (i = 1 , 2 ,..., l), let

z i
−−−→
T 1

a i / z i

−−−→
T 2

a i /

( p , α ) ( p i , α i ) and ( p , β ) ( p i , β i )