On synchronized multi-tape and multi-head automata

Motivated by applications to verification problems in string manipulating programs, we look at the problem of whether the heads in a multi-tape automaton are synchronized. Given an n-tape pushdown automaton M with a one-way read-only head per tape and a right end marker $ on each tape, and an integer k≥0, we say that M is k-synchronized if at any time during any computation of M on any input n-tuple (x1,…,xn) (whether or not it is accepted), no pair of input heads that are not on $ are more than k cells apart. This requirement is automatically satisfied if one of the heads has reached $. Note that an n-tuple (x1,…,xn) is accepted if M reaches the configuration where all n heads are on $ and M is in an accepting state. The automaton can be deterministic (DPDA) or nondeterministic (NPDA) and, in the special case, may not have a pushdown stack (DFA, NFA). We obtain decidability and undecidability results for these devices for both one-way and two-way versions. We also consider the notion of k-synchronized one-way and two-way multi-head automata and investigate similar problems.