In this series of talks, we will present a proof of the decidability of the equivalence problem for deterministic pushdown automata. Namely given two deterministic pushdown automata, it is decidable if they accept the same language. This result was first proved by Géraud Sénizergues in 1997. His proof consists in two semi-decision procedures and hence while establishing decidability does not give an upper-bound on the complexity of the problem. In 2002, Colin Stirling gave a primitive recursive algorithm to decide the problem.

The aim of the talk is to present what seems to be the simplest self-contained proof of this result. We will present a proof based on the recent work of Petr Jancar which uses first-order grammars instead of deterministic pushdown automata. To keep the proof as simple as possible, we will present the proof giving two semi-decision procedures.