L(A)=L(B)? decidability results from complete formal systems

AbstractThe equivalence problem for deterministic pushdown automata is shown to be decidable. We exhibit a complete formal system for deducing equivalent pairs of deterministic rational boolean series on the alphabet associated with a dpda M. We then extend the result to deterministic pushdown transducers from a free monoid into an abelian group. A general algebraic and logical framework, inspired by Harrison et al. (Theoret. Comput. Sci. 9 (1979) 173–205), Conrcelle (Theoret. Comput. Sci. 6 (1978) 255–279) and Meitus (Kybernetika 5 (1989) 14–25 (in Russian)) is developed