Equivalent DPDA that always halts for every DPDA with empty stack language

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?

Edit

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.

• This is a standard proof contained in many textbooks that cover PDAs. Where have you looked, what have you read? – Raphael Dec 19 '16 at 18:40
• @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. – Karo Dec 27 '16 at 13:03
• For the look ahead method, see for instance the Chapter on PDA liacs.leidenuniv.nl/~hoogeboomhj/praatjes/pda.pdf (Lemma 14, Section 1.5) – Hendrik Jan Dec 27 '16 at 19:46

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.