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.

  • $\begingroup$ On a specific input. Isn't that the "standard" halting problem? $\endgroup$ Commented Jun 27, 2016 at 20:52
  • $\begingroup$ no, that's not the "standard" halting problem, because this is about deciding whether a DPDA halts, not deciding whether a TM halts. $\endgroup$
    – xdavidliu
    Commented Sep 17, 2020 at 2:39

2 Answers 2


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.

  • $\begingroup$ Looks okay to me. Also, what do you think about skipping $L_2$ and just directly using $L_1$ for the proof of $L_3$? Or is $L_2$ actually necessary? $\endgroup$
    – xdavidliu
    Commented Sep 19, 2020 at 4:58
  • $\begingroup$ That's an interesting idea, but how would the proof go? If $(q,s)$ is a configuration that has the shortest stack, with $y$ on top of the stack, then there's no reason to think it will ever return to state $q$ with $y$ on top. So some additional argument would be needed. Perhaps out of all pairs $(p,y)$ that are visited infinitely often, we can consider the shortest stack among such visits? $\endgroup$
    – D.W.
    Commented Sep 19, 2020 at 8:41
  • $\begingroup$ I wrote an answer that attempts to prove it, using $L_1$ directly and skipping $L_2$: cs.stackexchange.com/a/130303/755. Would you be interested in checking my reasoning? $\endgroup$
    – D.W.
    Commented Sep 19, 2020 at 9:17

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.

  • $\begingroup$ SimpleLoop should be tested using $L_2$, not $L_1$: It need not return to $p$ in order to run infinitely; while $L_1$ explicitly says it must return to $p$. $\endgroup$
    – xdavidliu
    Commented Sep 21, 2020 at 0:52
  • $\begingroup$ @xdavidliu, I think $L_1$ suffices. I think I've taken care of that by considering only the good silhouettes. If it doesn't return to $p$, then $p$ won't recur infinitely many times, so it'll be excluded, since I'm focusing only on good silhouettes/configurations. $\endgroup$
    – D.W.
    Commented Sep 21, 2020 at 1:40
  • $\begingroup$ For the way you have defined SimpleLoop, being accepted by $L_1$ is sufficient, but not necessary: even if it never returns to $p$, it can still loop infinitely. In comparison, $L_2$ is both necessary and sufficient for SimpleLoop. $\endgroup$
    – xdavidliu
    Commented Sep 21, 2020 at 3:41
  • $\begingroup$ @xdavidliu, I wonder if we are miscommunicating. I don't see how any of that is relevant. My proof demonstrates that if $M$ runs forever, then it visits a state that will be accepted by $L_1$. Sure, it might also visit a state $p$ of the form you describe, but if so, there will also exist another state $p'$ that is accepted by $L_1$. I'm not claiming that if $M$ loops every state will be accepted by $L_1$; all I'm claiming is that there will be one state. So saying "well you could have a state that isn't accepted by $L_1$" does not contradict anything in my proof. $\endgroup$
    – D.W.
    Commented Sep 21, 2020 at 3:53
  • $\begingroup$ Is there some line of my proof that you think does not follow or is not convincing? Is there some way I could make the argument clearer? Is it the name SimpleLoop -- is that name misleading or confusing? My proof has a different structure than yours but I think it is still valid. $\endgroup$
    – D.W.
    Commented Sep 21, 2020 at 3:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.