# An Introduction to Decidability of DPDA Equivalence

## Abstract

The DPDA equivalence problem was posed in 1966 [4]: 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 [11]. 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 [12]. 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.

## Preview

Unable to display preview. Download preview PDF.

## References

- 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 - 3.Christensen, S., Hüttel, H., and Stirling, C. (1995). Bisimulation equivalence is decidable for all context-free processes.
*Information and Computation*,**121**, 143–148.zbMATHCrossRefMathSciNetGoogle 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 - 6.Harrison, M., and Havel, I. (1973). Strict deterministic grammars.
*Journal of Computer and System Sciences*,**7**, 237–277.zbMATHMathSciNetGoogle Scholar - 7.Harrison, M., Havel, I., and Yehudai, A. (1979). On equivalence of grammars through transformation trees.
*Theoretical Computer Science*,**9**, 173–205.zbMATHCrossRefMathSciNetGoogle 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 - 10.Oyamaguchi, M., Honda, N., and Inagaki, Y. (1980). The equivalence problem for real-time strict deterministic languages.
*Information and Control*,**45**, 90–115.zbMATHCrossRefMathSciNetGoogle 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 - 12.Sénizergues, G. (2001). L(A) = L(B)? decidability results from complete formal systems.
*Theoretical Computer Science*,**251**, 1–166.zbMATHCrossRefMathSciNetGoogle Scholar - 13.Stirling, C. (1998). Decidability of bisimulation equivalence for normed pushdown processes.
*Theoretical Computer Science*,**195**, 113–131.zbMATHCrossRefMathSciNetGoogle Scholar - 14.Stirling, C. (2001). Decidability of DPDA equivalence.
*Theoretical Computer Science*,**255**, 1–31.zbMATHCrossRefMathSciNetGoogle Scholar