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 136

The Equivalence Checking Algorithm
Check whether N ( p , α ) = 0 or not for each configuration ( p , α ) ∈ Q 1 × Γ 1 with
1 ≤| α |≤| Q 1 | . Similarly, check whether N ( p , β ) = 0 or not for each configuration
( p , β ) ∈ Q 2 × Γ 2 with 1 ≤| β |≤| Q 2 | .
Let the comparison tree consist of only a root labeled ( q 01 , Z 01 ) ≡ ( q 02 , Z 02 ) in
unchecked status.
while the comparison tree contains an unchecked or a skipping node do
if the comparison tree contains an unchecked node then
let P be the smallest unchecked node
else let P be the smallest skipping node fi
suppose P is labeled ( p , α ) ≡ h ( p , β ) ;
if stack reduction is applicable to P then
apply the stack reduction to P ;
turn the status of P to be checked , while its newly added son is in unchecked ;
turn the status of all s-checked nodes to be skipping
else
if FIRST live ( p , α )= FIRST live ( p , β )= { ε } and both ( p , α ) and ( p , β ) are
not in ε-mode then
if h = ε then turn P to checked
else conclude that “ T 1 ≡ T 2 ”; halt fi
else if

( p , α ) ≡ h (

p , β )( h = h )

appears as the label of another internal

node then
conclude that “ T 1 ≡

T 2 ”; halt

else
if ( p , α ) ≡ h ( p , β ) appears as the label of another internal node then
turn P to checked
else
if the prerequisite for skipping to P is satisfied then
if skipping to P is applicable then
apply the skipping to P ;
if either any skipping-end has been newly added to P as its son,
or any label of an edge from P has been changed by
the above skipping then
turn the status of P to be skipping , while its newly added sons
are in unchecked ;
turn the status of all s-checked nodes to be skipping
else turn the status of P to be s-checked fi
else conclude that “ T 1 ≡ T 2 ”; halt fi
else if output branch checking is successful for P then
apply the branching to P ;
turn the status of P to be checked , while its newly added sons
are in unchecked ;
turn the status of all s-checked nodes to be skipping
else conclude that “ T 1 ≡ T 2 ”; haltfifififififiod
Conclude that “ T 1 ≡ T 2 ”; halt

Fig. 1 The Equivalence Checking Algorithm