Decidability of halting problem for DPDAs with $\epsilon$-transitions?

Question

For LBAs it's rather easy to prove the decidability of the halting problem, as there can only be a finite number of different configurations when using limited space.

But what about PDAs with $\epsilon$-transitions? Is the halting problem decidable for deterministic PDA's with $\epsilon$-transitions? Given such a DPDA $P$ and an input $x$, can we decide whether $P$ will halt on input $x$?

The stack may be infinitely large, so it seems like it might be much harder here to see if the PDA is in an infinite loop or not.

I don't think it's as easy as answered here for non-$\epsilon$ PDAs:

[For] DFAs or PDAs, the halting problem is decidable: the machine always halts because it halts when it reaches the end of its input, the input is finite and the machine consumes one character of input at every step.

Is the halting problem specific to Turing machines?)

The answer to my earlier question (Is a PDA's stack size linear bounded in input size?) also seems to point in a direction of a higher difficulty of proving this.

Answer 1

Let $L_1$ be the language of all $(M, p, y)$ such that if we start $M$ (a DPDA with $\epsilon$ transitions) in state $p$ with a stack consisting of only $y$ (which is either a single symbol or nothing), then reading an empty string as input would cause $M$ to eventually return to state $p$, with a $y$ on top of its stack if $y$ was a symbol rather than nothing (if $y$ was originally nothing, we don't care about what's on the top of stack after $M$ returns to $p$; anything is fine).

claim: $L_1$ is decidable.

proof: modify $M$ as follows: make a copy $p_0$ of $p$ with the same outgoing transitions but no incoming transitions, and start the DPDA in $p_0$ with a symbol $y$ (or empty) in its stack. If $y$ is empty, then make $p$ the only accept state. Otherwise if $y$ is a symbol, then after creating $p_0$, modify the outgoing transition of $p$ with $y$ on the top of its stack to instantly go to a state $w$ that is now the only accept state (see note 1). Now use the standard CFL emptiness decider on this modified DPDA and we are done.

Note 1: If there is no such transition to modify due to determinism of $M$, i.e. $p$ only has one outgoing $\epsilon$ transition that either does nothing or pushes some symbol onto the stack, then do the following instead: delete the transition, add one that pops $y$ and goes to $w$ and also add trivial no-op transition that pops then immediately pushes back all other symbols that are not $y$.

Next, let $L_2$ be the language of all $(N, q, x)$ such that if we start the DPDA $N$ in state $q$ with a stack having only a single symbol $x$ (or empty), then with an empty input string, it will run forever without ever attempting to pop an empty stack. Note Sipser calls $(q, x)$ a "looping situation".

claim: $L_2$ is decidable (Sipser third edition problem 4.32 asks to prove this)

proof: take $N$ and delete all its input-reading transitions (leaving only $\epsilon$ transitions). Then, start $N$ in state $q$ with an $x$ on its stack, and for every state $p$ it enters, take its stack top $y$ and run the decider for $L_1$ on $(N, p, y)$. This procedure is guaranteed to terminate in either an accept for $L_1$ for some $p$ and $y$, or $N$ itself will terminate (either by attempting to pop an empty stack or by running out of $\epsilon$ transitions to follow). (Why? Suppose $N$ runs forever. Consider all of the pairs $(p,y)$ that it encounters at each step during execution. Since there are only finitely many states and symbols, by the pigeonhole principle, there must be some pair $(p,y)$ that is encountered infinitely often during execution; consider all the time points where we encounter $(p,y)$. Since the size of the stack cannot decrease forever, there must be some adjacent pair of such time points where the stack is larger at the second than at the first. Now consider the execution between between those two times, and find the time in that range when the stack is smallest. Let $p'$ be the state of the DPDA and $y'$ the value on the top of its stack. Then starting the DPDA at state $p'$ and just $y'$ on the stack and running forward will eventually return to state $p'$ with $y'$ on the top of the stack. Why? Well, we start $(p',y')$, then reach a point with state $p$ and $y$ on the top of the stack, then continues on to a point with state $p'$ and $y'$ on the top of the stack, and we never pop off the initial $y'$. Basically, we've decomposed the trajectory $(p,y) \leadsto (p',y') \leadsto (p,y)$ into its second part $(p',y') \leadsto (p,y)$ followed by its first part $(p,y) \leadsto (p',y')$, but with things chosen so that we can start with just the symbol $y'$ on the stack and nothing more, and it will never get popped off. It follows that $(N,p',y')$ is accepted by $L_1$, i.e., if $N$ runs forever, it will visit a pair that is accepted by $L_1$.)

Finally, we get to the problem in the main question: define $L_3$ as the language of $(M, x)$ where $x$ is some input string such that the DPDA $M$ halts on input $x$.

claim: $L_3$ is decidable.

proof: run $M$ on input $x$, and after every input symbol read, run the decider for $L_2$ on the current state and stack top: either $M$ itself will halt or the $L_2$ decider will return an acceptance. (Why? Suppose $M$ never halts normally. Then consider the configuration $(q,s)$ where $s$ is the shortest stack among all configurations, resolving ties arbitrarily. Since $s$ is among the shortest stacks, it will never pop below the element on top of $s$. Consequently, $(q,y)$ is accepted by the decider for $L_2$, where $y$ is the top of $s$.)

Note 2: it's probably not necessary to run $L_2$ decider to prove decidability of $L_3$: we can just run the $L_1$ decider instead.

Answer 2

Suppose we have a DPDA with $\epsilon$ transitions, $M$. Define a configuration of $M$ to be a pair $\langle p,s \rangle$ where $p$ is a state and $s$ is a stack; and define the silhouette of $\langle p,s \rangle$ to be the pair $(p,y)$ where $y=\textrm{top}(s)$ is the symbol at the top of the stack $s$.

Define a subroutine called SimpleLoop as follows: when provided a silhouette $(p,y)$, it checks whether, if you start in configuration $\langle p,y \rangle$ (i.e., in state $p$ and with a stack containing only $y$), running $M$ on an empty input will return to the same silhouette and in this way enter an infinite loop. This can be tested using the decider for $L_1$ from xdavidliu's answer. Note that if SimpleLoop returns yes on a silhouette $(p,y)$, then any configuration with that silhouette will lead to an infinite loop (if we process the empty input), but the reverse does not hold.

Now to test whether $M$ halts on input $x$, we'll use the following algorithm. Simulate running $M$ on input $x$. At each configuration reached, we invoke the SimpleLoops subroutine on the current silhouette $(p,y)$; if SimpleLoops returns yes, then we terminate and output that $M$ never halts. If $M$ halts, we terminate and output that $M$ halts.

---

Now we need to prove that the above algorithm is correct. Clearly, if the algorithm terminates, its output is correct. We need to show that the algorithm will always terminate. If $M$ halts on input $x$, then the algorithm terminates, so now assume $M$ never halts on input $x$.

In this case, it must enter a non-terminating computation after consuming some prefix of $x$, say $x_{1..k}$; the non-termination happens among the $\epsilon$-transitions after reading $x_{1..k}$. We'll ignore everything before those $\epsilon$-transitions. Consider the sequence of silhouettes that are traversed during these $\epsilon$-transitions.

You can classify each silhouette according to whether it is traversed finitely many times (bad) or infinitely many times (call this a good silhouette). Since this is an infinite sequence, by the pigeonhole principle, there must be some point in time after which all silhouettes visited are good. So, discard the part of the sequence before that, and focus only on the sequence of silhouettes/configurations after that point in time.

Now of all configurations reached after that point that have a good silhouette, take the configuration $\langle p,s \rangle$ whose stack is shortest. Let $y$ be the symbol on the top of $s$, so its silhouette is $(p,y)$. Since the silhouette $(p,y)$ is good, i.e., is visited infinitely many times, there must be a subsequent configuration $\langle p,s' \rangle$ with the same silhouette. Moreover, the part of the execution $\langle p,s \rangle \leadsto \langle p,s' \rangle$ never pops off any element under the top of $s$ (since $s$ was one of the configurations with the shortest stack), so $s$ must have the form $y:t$ and $s'$ must have the form $y:t':t$, where $y$ is the symbol on the top of $s$ and $t$ is the rest of $s$. Consequently it follows that $\langle p,y \rangle \leadsto \langle p,y:t' \rangle$ on an empty input, and thus the SimpleLoop subroutine will return yes on the silhouette $(p,y)$.

So we have shown that if $M$ never halts on input $x$, the algorithm will eventually reach a silhouette where SimpleLoop returns yes, and the algorithm will terminate in finitely many steps. Alternatively, if $M$ halts on input $x$, the algorithm will also terminate after finitely many steps. So the algorithm always terminates, and always yields the correct answer.