In the context of our investigation of heap automata, I would like to prove that a particular variant can not accept non-context-sensitive languages. As we have no equivalent grammar model, I need a proof that uses only automata; therefore, I have to show that heap automata can be simulated by LBAs (or an equivalent model).
I expect the proof to work similarly to showing that pushdown automata accept a subset the context-sensitive languages. However, all proofs I know work by
- using grammars -- here the fact is obvious by definition -- or
- are unconvinvingly vague (e.g. here).
My problem is that a PDA (resp. HA) can contain cycles of $\varepsilon$-transitions that may write symbols to the stack (resp. heap). An LBA can not simulate arbitrary iterations of such loops. From the Chomsky hierarchy obtained with grammars, we know that
- every context-free language has an $\varepsilon$-cycle-free PDA or
- the simulating LBA can prevent iterating $\varepsilon$-cycles too often.
Intuitively, this is clear: such cycles write symbols independently of the input, therefore the stack (heap) content does only hold an amount of information linear in the length of the cycle (disregarding overlapping cycles for now). Also, you don't have a way to get rid of the stuff again (if you need to) other than using another $\varepsilon$-cycle. In essence, such cycles do not contribute to dealing with the input if iterated multiple times, so they are not necessary.
How can this argument be put rigorously/formally, especially considering overlapping $\varepsilon$-cycles?