Revisiting the Equivalence Problem for Finite Multitape Automata

TL;DR

This paper presents an alternative proof for the decidability of equivalence in deterministic multitape automata, introducing a polynomial-time randomized algorithm based on matrix algebra that efficiently determines automata equivalence.

Contribution

It offers a new proof replacing group theory with matrix algebra results and introduces a polynomial-time randomized algorithm for automata equivalence checking.

Findings

Decidability of automata equivalence confirmed with a new proof.

Introduces a polynomial-time randomized algorithm for equivalence checking.

Algorithm outputs a distinguishing word if automata are inequivalent.

Abstract

The decidability of determining equivalence of deterministic multitape automata (or transducers) was a longstanding open problem until it was resolved by Harju and Karhum\"{a}ki in the early 1990s. Their proof of decidability yields a co_NP upper bound, but apparently not much more is known about the complexity of the problem. In this paper we give an alternative proof of decidability, which follows the basic strategy of Harju and Karhumaki but replaces their use of group theory with results on matrix algebras. From our proof we obtain a simple randomised algorithm for deciding language equivalence of deterministic multitape automata and, more generally, multiplicity equivalence of nondeterministic multitape automata. The algorithm involves only matrix exponentiation and runs in polynomial time for each fixed number of tapes. If the two input automata are inequivalent then the algorithm outputs a word on which they differ.