I want to show that for every deterministic pushdown automaton with the language of the empty stack there is a deterministic pushdown automaton that always halts. my transition function of $P$ is

$\delta: \Gamma \times Q \times \Sigma_\lambda \to \Gamma^* \times Q$

I tried to use look ahead pushdown method. I think I should create a $DFA$ for every $q \in Q$ that recognize if $P$ is in the lambda-cycle starting from $q$ with input string reversing of containing the stack of $P$. I define NFA with states of set $\Gamma \times Q$ and it has transition from $(\alpha,p)$ to $(\alpha',p')$ reading $\beta$ if there is $(\beta\alpha',p') \in \delta(\alpha,p,\lambda)$ and start state is $(Z_0,q)$ and I think every state should be final state. then reverse $NFA$ and convert it to $DFA$. I don't know this works or not. I after that I can create $DPDA$ named $P'$ such that its stack simulate all $DFAs$ and also original stack of $P$ and after that I can decide if $P$ will be in the loop in future so in $P'$ it halts.

how can I edit creating $DFA$ that works well?


I changed the way using above automata, first of all, I design $DFA$ to check if in future there is a sequence of lambda-transitions that empties stack? if there is so I should let process continues because it will stop in future. $NFA$ is like above example with final states in $(\lambda,q)$ for each $q\in Q$ and simply we can convert $NFA$ to $DFA$, if there is not such sequence I ask another question, is it possible that we have some non-lambda transition? checking this is also simple we create exactly same $NFA$ as above $NFA$ and after that, if in a state we have non-lambda transition we go to a special final state. if there is no such transition it means we will stock on loop in future.

  • $\begingroup$ This is a standard proof contained in many textbooks that cover PDAs. Where have you looked, what have you read? $\endgroup$
    – Raphael
    Commented Dec 19, 2016 at 18:40
  • $\begingroup$ @Raphael books such as Sipser have a different definition of PDA and DPDA. and I also looked at books like Linz and some other books but none of them used look ahead pushdown to proof this theorem. is there any textbook that explains this method? I also change my proof I thinks it's correct right now. $\endgroup$
    – Karo
    Commented Dec 27, 2016 at 13:03
  • 1
    $\begingroup$ For the look ahead method, see for instance the Chapter on PDA liacs.leidenuniv.nl/~hoogeboomhj/praatjes/pda.pdf (Lemma 14, Section 1.5) $\endgroup$ Commented Dec 27, 2016 at 19:46

1 Answer 1


The look-ahead property for pushdown automata is that a PDA $Z$ can answer certain questions of the form "how would PDA $X$ behave when given my stack", and then make moves based on that information. In particular, also deterministic PDA $Z$ can use this even when $X$ is nondeterministic.

You know, as I understand from the formulation of your question, this is possible because the property "when started on stack $\alpha$ PDA $X$ empties its stack" defines a regular set of stacks. The PDA look-ahead test can then be build in the original PDA.

So, to solve your problem, you have to formulate which PDA tests you would like to perform on the stack in order to avoid infinite computations.

I do not know whether it is necessary to actually construct the regular language of stacks that gives a positive answer.


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.