Store Languages of Turing Machines and Counter Machines

The store language of an automaton is the set of store configurations (state and store contents, but not the input) that can appear as an intermediate step in an accepting computation. A one-way nondeterministic finite-visit Turing machine (fvNTM) is a Turing machine with a one-way read-only input tape, and a single worktape, where there is some number $k$ such that in every accepting computation, each worktape cell is visited at most $k$ times. We show that the store language of every fvNTM is a regular language. Furthermore, we show that the store language of every fvNTM augmented by reversal-bounded counters can be accepted by a machine with only reversal-bounded counters and no worktape. Several applications are given to problems in the areas of verification and fault tolerance, and to the study of right quotients. We also continue the investigation of the store languages of one-way and two-way machine models where we present some conditions under which their store languages are recursive or non-recursive.