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

Question

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.

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.