When does a PDA halt? In DFA/NFA the automaton halts when it finishes reading the string.

In a PDA there's the string and the stack. When the string is finished and there are symbols on the stack does it ignore them? Or does it have to pop them?

Or maybe does the behavior depend on whether the PDA is deterministic or not?



Here's an example to demonstrate where the ambiguity is.

It's a dumb example and it can be done with a DFA but just for demonstration.



This PDA should accept anything but the string aa.

It starts by inserting a $ to mark the bottom of the stack. Then it inserts 2 as. Then when it receives an a it pops one from a stack. It can do that twice.

Now at this point suppose that the input string was indeed aa, and that the machine reached state x and popped the two as. Now the stack has only $ in it.


Does it have to go to the next state (y) because there's a $ on top of the stack?
Or by non-determinism can it be either in x or in y?


If the latter is true then this is a wrong PDA for this language. It would accept everything.
The setup places $aa\$$ on the stack and puts the machine in state $x$. We then have this sequence of moves on input $aa$:


Consume the first $a$ and pop the stack. We're then still in state $x$ with stack contents $a\$$. No other move is possible.
Consume the next $a$ and pop the stack. We're then still in state $x$ with stack contents $\$$. No other move is possible.
Seeing a $\$$ on the stack, the only possible move is to pop the $\$$ and pass to state $y$.
In state $y$ with no further input, there are no possible moves, so the machine halts, in a non-accepting state.


Notice that there's no nondeterminism here: perhaps you were mistaken in your first bullet point: indeed there is a $\$$ in the stack at move (1), but it's not on the top of the stack.

The deeper question is exactly what model of a PDA is being used here: some people allow multiple accept states and say that the PDA accepts a string if it is in an accept state when the input has been completely consumed, others require that the stack be empty when the input has been consumed; some require a single accept state, some don't. All these models are equivalent, but you need to look closely at the definition you are using.