On Synchronized Multitape and Multihead Automata

Motivated by applications to verification problems in string manipulating programs, we look at the problem of whether the heads in a multitape 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 (

x

1

, …,

x

n

) (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 (

x

1

, …,

x

n

) 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 multihead automata and investigate similar problems.