A decision procedure is described for equivalence of deterministic two-tape (oneway) automata.
l. INTRODUCTION
The notion of an n-tape (one-way, deterministic) automaton was introduced by Rabin and Scott [2]. Although the properties of these devices have been studied extensively, no answer has been forthcoming to the question: for any n >/2, is there an effective procedure for deciding if two n-tape automata are equivalent ? The present paper shows that, in the case of two-tape automata, such a procedure exists.
We concentrate on a simplified form of two-tape automaton called a "scheme." A scheme may be thought of as a two-tape automaton with, instead of a set of final states, a single final state (the "exit") from which no transitions are permitted. It is shown that there exists a decision procedure for equivalence of schemes (Sections 2-5), and that the equivalence problem for two-tape automata reduces to the equivalence problem for schemes (Section 6).
The decision procedure is based on the notion of a "closed diagram." Informally, this is a nondeterministic scheme (without an "entry node") with a certain property which guarantees deterministic behavior. It is shown that two schemes are equivalent if and only if they can be mapped in a certain manner into a closed diagram. Given two schemes the procedure attempts to construct a closed diagram related to them in this way.
DEFINITIONS
Before giving a formal definition of "schemes," we define two generalizations ("semidiagrams" and "diagrams") which arise during the execution of the decision procedure. We also define a type of mapping ("morphism") between these objects in terms of which many of their properties may be expressed conveniently.