Proof emptiness for PDA is $\mathcal{O}(n^3)$

It is well known that the emptiness problem vor PDAs is in $$\mathcal{O}(n^3)$$. I couldn't find a good paper proving this theorem. Furthermore a proof for VPAs would be fine for me as well if that is easier.

Do you maybe have a book or paper I should investigate?

EDIT: This looks interesting but a formal proof from a book or paper would be great!

Start with an arbitrary PDA. Convert it to a PDA which pushes at most two symbols to the stack at each step — this only incurs a linear blow-up. Convert the PDA to a CFG using the standard construction, described in this answer. Since the PDA pushed at most two symbols at each step, the CFG has size $$O(n^3)$$ (for each transition $$p \stackrel {a,\gamma} \to q$$, where $$a$$ is a letter and $$\gamma$$ is a word in the stack alphabet, we have to enumerate over $$|\gamma| \leq 2$$ states, hence the number of transitions is at most the original number of transitions times $$|Q|^2$$). Convert the CFG to Chomsky normal form with linear blow-up. Then use the linear time algorithm described in this answer to check whether the CFG generates an empty language or not.

Summarizing:

• Convert the PDA to one in which at most two symbols are pushed to the stack at each move (linear blow-up).
• Convert the new PDA to a CFG (cubic blow-up).
• Convert the CFG to Chomsky normal form (linear blow-up).
• Check emptiness of the CFG in Chomsky normal form (linear time).

You can probably skip the step in which you convert the CFG to Chomsky normal form by modifying slightly the algorithm described in the second answer.