4pm Tuesday 5th February 2002
Room 2511, JCMB, King's Buildings
Despite intensive work throughout the 1960s and 1970s, the equivalence problem for determinisitic pushown automata, DPDA, whether language equivalence is decidable for deterministic context-free languages, remained unsolved until 1997 when Senizergues announced a positive solution. The full proof, in journal form, appeared last year in TCS. I produced a different proof of decidability using ideas from concurrency and language theory that is essentially a simplification of Senizergues's proof (that also appeared last year in TCS). It views the problem as a bisimulation equivalence problem for a process calculus whose expressions generate infinite-state transition graphs.
These proofs of decidability are very complex because they rely on subtle mechanisms for ``decomposition'' (to show termination) that introduce nondeterminism into the decision procedures. A consequence is that decidability is achieved through two semi-decision procedures that do not give a complexity upper bound: this is also true of proofs of decidability in restricted cases, such as for DPDA without epsilon transitions that was shown in 1980.
In the talk, I review the problem and its background and describe a much simpler decision procedure that is determinisitic. It avoids decomposition mechanisms: instead, there is an analysis of termination, using a new combinatorial result, "the extension theorem". One consequence is a primitive recursive upper bound on the complexity of the decision procedure.