How to prove that ε-loops are not necessary in PDAs? 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?
The removal of $\varepsilon$-transitions has been studied for the more
general model of valence automata by Zetzsche [1]. 
Valence automata are essentially finite automata with a monoid for storage.

Among other things, Zetzsche shows that for monoids $M$ from a rich class $\mathcal{C}$ of monoids
(which contains (partially) blind counters, stacks, and combinations thereof), 
$\varepsilon$-free $M$-automata accept the same class of languages as $M$-automata.

Since PDAs with a $k$-symbol stack alphabet correspond to valence automata over
monoid $\mathbb{B}^{(k)} \in \mathcal{C}$ ($\mathbb{B}$ is the 
bicyclic monoid),
the result from Theorem 1 (resp. 7.1 in the preprint) applies here. 

The proof is long and technical; the proofs of lemmas 8 and 10 (resp. 7.6 and 7.9) 
contain the relevant constructions. Note that while they do not use grammar models
(as required in the question) they do use valence transducers.




Silent Transitions in Automata with Storage by G. Zetzsche (2013) [more elaborate preprint on arXiv]