These two talks will continue the study of the equivalence problem of deterministic pushdown automata (DPDA).

The main focus of these talks will be on the computational complexity of this problem. We will give a proof of Stirling’s result that DPDA equivalence is primitive recursive.

More precisely, we will present a recent paper by Jancar that shows that in case two DPDAs are inequivalent they can be distinguished by a word whose length is bounded by a tower of exponentials of elementary height.

As in Arnaud’s talk we will view DPDA equivalence in terms of trace equivalence of deterministic first-order grammars.

This talk aims at going hand-in-hand with Arnaud’s talk but is intended to be self-contained as well.

These talks will be completely self-contained and require no background knowledge.