An Introduction to Decidability of DPDA Equivalence
The DPDA equivalence problem was posed in 1966 : is there an effective procedure for deciding whether two configurations of a deterministic pushdown automaton (a DPDA) accept the same language? The problem is whether language equivalence is decidable for deterministic context-free languages. Despite intensive work throughout the late 1960s and 1970s, the problem remained unsolved until 1997 when Sénizergues announced a positive solution . It seems that the notation of pushdown configurations, although simple, is not rich enough to sustain a proof. Deeper algebraic structure needs to be exposed. The full proof by Sénizergues, in journal form, appeared earlier this year . It exposes structure within a DPDA by representing configurations as boolean rational series, and he develops an algebraic theory of their linear combinations. Equivalence between configurations is captured within a deduction system. The equations within the proof system have associated weights. Higher level strategies (transformations) are defined which guide proof. A novel feature is that these strategies depend upon differences between weights of their associated equations. Decidability is achieved by showing that two configurations are equivalent if, and only if, there is a finite proof of this fact.
Unable to display preview. Download preview PDF.
- 1.Burkart, O., Caucal, D., Moller, F., and Steffen, B. (2001). Verification on infinite structures. In Handbook of Process Algebra, edited Bergstra, J., Ponse, A., and Smolka, S. 545–623, North Holland.Google Scholar
- 2.Christensen, S., Hirshfeld, Y. and Moller, F. (1993). Bisimulation equivalence is decidable for all basic parallel processes. Lecture Notes in Computer Science, 715, 143–157.Google Scholar
- 4.Ginsberg, S., and Greibach, S. (1966). Deterministic context-free languages. Information and Control, 620–648.Google Scholar
- 5.Harrison, M. (1978). Introduction to Formal Language Theory, Addison-Wesley.Google Scholar
- 8.Hüttel, H., and Stirling, C. (1991). Actions speak louder than words: proving bisimilarity for context free processes. Proceedings 6th Annual Symposium on Logic in Computer Science, IEEE Computer Science Press, 376–386.Google Scholar
- 9.Korenjak, A and Hopcroft, J. (1966). Simple deterministic languages. Procs. 7th Annual IEEE Symposium on Switching and Automata Theory, 36–46.Google Scholar
- 11.Sénizergues, G. (1997). The equivalence problem for deterministic pushdown automata is decidable. Lecture Notes in Computer Science, 1256, 671–681.Google Scholar