Halting Stack Automata
Jeffrey David Ullman · Journal of the ACM · 1969
It is shown that every two-way (deterministic) stack automaton language is accepted by a two-way (deterministic) stack automaton which for each input has a bound on the length of a valid computation. As a consequence, two-way deterministic stack languages are closed under complementation.