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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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. 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. 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. 4.
    Ginsberg, S., and Greibach, S. (1966). Deterministic context-free languages. Information and Control, 620–648.Google Scholar
  5. 5.
    Harrison, M. (1978). Introduction to Formal Language Theory, Addison-Wesley.Google Scholar
  6. 6.
    Harrison, M., and Havel, I. (1973). Strict deterministic grammars. Journal of Computer and System Sciences, 7, 237–277.zbMATHMathSciNetGoogle Scholar
  7. 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. 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. 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. 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. 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. 12.
    Sénizergues, G. (2001). L(A) = L(B)? decidability results from complete formal systems. Theoretical Computer Science, 251, 1–166.zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Stirling, C. (1998). Decidability of bisimulation equivalence for normed pushdown processes. Theoretical Computer Science, 195, 113–131.zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Stirling, C. (2001). Decidability of DPDA equivalence. Theoretical Computer Science, 255, 1–31.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Colin Stirling
    • 1
  1. 1.Division of InformaticsUniversity of EdinburghUK

Personalised recommendations