# Does a DPDA halt on all inputs?

Given a deterministic DPA, is it possible to tell whether it halts on all possible inputs? Is this problem decidable?

The standard halting problem is "Given a DPDA and an input $x$, determine whether it halts on input $x$", and that problem is decidable. But what about the variant above?

Yes, this problem is decidable. It can be answered in polynomial time. We can check whether there exists any input $x$ that causes it to enter an infinite loop, by characterizing the states from which it could enter an infinite loop.

First, let me establish some terminology. Let $Q$ denote the set of states of the DPDA, and $\Gamma$ the stack alphabet. A configuration is a pair $(q,t)$ with $q \in Q$, $t \in \Gamma^*$, where $q$ represents the state of the automaton and $t$ the contents of its stack. Define the status of the automaton at any point to be a pair $(q,\gamma)$ where $q \in Q$ represents the state of the automaton and $\gamma \in \Gamma$ the symbol at the top of the stack. Thus, the status gives only partial information about the configuration of the automaton.

Now, the strategy is going to be twofold:

1. We will determine, for each possible status $(q,\gamma)$, whether that status is reachable (i.e., whether there is some input $x$ that takes the automaton to a point where it is in that status).

2. We will also determine, for each possible status $(q,\gamma)$, whether the automaton enters a particular kind of infinite loop if the automaton starts in the configuration $(q,\gamma)$ and then reads the input $\epsilon$ (the empty word). In particular, if it starts in configuration $(q,\gamma)$ and reads the input $\epsilon$, we'll test whether it transitions to any configuration $(q,t)$ where $t$ has the form $\cdots \gamma$ (i.e., $\gamma$ at the top of the stack, with some other stuff below it in the stack) in the process of reading the empty word.

Putting these two together, if there is a status $(q,\gamma)$ for which the answer to both questions is yes, then we will learn that the input $x$ causes the automaton to enter an infinite loop. We will show a polynomial-time algorithm for each. Since there are only finitely (in fact, polynomially) many possibilities for the status, this gives a polynomial-time algorithm for the original problem. So, on to the details of how to check each of these things.

First, reachability is easy and can be tested using standard methods. (For instance, construct a new automaton that halts when it enters the status $(q,\gamma)$ and otherwise doesn't halt, then check whether that automaton accepts the empty language or not; there is a standard algorithm for that.)

Second, it's easy to find all statuses $(q,\gamma)$ where an automaton that starts in configuration $(q,\gamma)$ and reads the empty word will enter an infinite loop of the particular kind mentioned above. (One way is to reduce this to reachability; construct a new automaton that starts in configuration $(q,\gamma)$ and halt if it reaches any configuration of the form $(q,\dots \gamma)$ apart from the initial state, discarding all non-$\epsilon$ transitions from the original automaton and keeping only the $\epsilon$ transitions. Then, check whether this new automaton accepts a non-empty language.)

This yields an algorithm for the original problem. Why is it correct?

Well, if this algorithm outputs "yes", then it is correct -- there exists an input $x$ that causes the automaton to halt. In particular, we know there exists an input $x$ that causes the automaton to transition to status $(q,\gamma)$, i.e., to some configuration of the form $(q,t_0 \gamma)$. Suppose reading the empty word causes the automaton to transition from configuration $(q,\gamma)$ to $(q,t_1 \gamma)$; then it follows it will subsequently transition to $(q,t_1 t_1 \gamma)$ and even later to $(q,t_1 t_1 t_1 \gamma)$ and so on, entering an infinite loop. Thus, reading the empty word will cause the automaton to transition from the configuration $(q,t_0 \gamma)$ to the configurations $(q, t_0 t_1 \gamma)$ and $(q, t_0 t_1 t_1 \gamma)$ and so on, thus entering an infinite loop. Since the input $x$ takes us to that configuration $(q,t_0 \gamma)$, we have found an input $x$ that causes the DPDA to enter an infinite loop. So if the algorithm says "yes", it is correct.

What about the converse? Let's suppose there exists some input $x$ that causes the DPDA to enter an infinite loop. It follows that the infinite loop must happen during the $\epsilon$-transitions that follow some finite prefix of $x$, say $x'$. Let $(q',t')$ denote the configuration of the automaton immediately after reading the last letter of $x'$ (but before following any of the subsequent $\epsilon$-transitions). Let's consider the sequence of configurations that the DPDA visits after that point, by following the $\epsilon$-transitions. By assumption, this is an infinite sequence. Consider the corresponding sequence of statuses. Since that is infinite sequence, and there are only finitely many statuses, there must be at least one status that appears infinitely many times. Discard a large enough prefix of the sequence so that you remove all the statuses that occur only finitely many times, so that now we have a sequence where all statuses recur infinitely many times; such a prefix must exist. Among all configurations in the resulting sequence, pick the configuration where the height of the stack is minimal. Call this configuration $(q,t)$ where $t=t_0 \gamma$. By the choice of $(q,t)$, it follows that in all subsequent configurations the stack is at least as tall, so the original symbols $t_0$ are never popped, i.e., all subsequent configurations are of the form $(q',t_0 u)$ for some $q' \in Q$, $u \in \Gamma^+$. Also since the status $(q,\gamma)$ recurs infinitely often in the sequence and since $(q,t_0 \gamma)$ was the one of minimal height, there must be some subsequent configuration of the form $(q, t_0 t_1 \gamma)$ (i.e., some subsequent configuration with the same status, but stack at least as high). And since we got from $(q, t_0 \gamma)$ to $(q, t_0 t_1 \gamma)$ by $\epsilon$-transitions, without ever popping off the $t_0$ part, this means we'll enter an infinite sequence $(q, t_0 \gamma) \leadsto (q, t_0 t_1 \gamma) \leadsto (q, t_0 t_1 t_1 \gamma) \leadsto (q, t_0 t_1 t_1 t_1 \gamma) \leadsto \cdots$. Since the $t_0 \gamma$ was never popped off, that also means that if we had started in the configuration $(q, \gamma)$, we would also have entered an infinite sequence $(q, \gamma) \leadsto (q, t_1 \gamma) \leadsto (q, t_1 t_1 \gamma) \leadsto \cdots$, and this would have been detected in step 2 of the algorithm. Also, by assumption, since the configuration $(q, t_0 \gamma)$ is reachable on input $x'$, the status $(q,\gamma)$ is reachable and this would be detected in step 1 of the algorithm. In summary, if there exists an input $x$ that causes the DPDA to enter an infinite loop, there exists a status $(q,\gamma)$ that is reachable and that triggers an infinite loop of the specific kind detected in step 2 of the algorithm, so the algorithm will output "yes".